Commit 9a1309c5 authored by POTTIER Francois's avatar POTTIER Francois

A Coq solution for part 1 of the mid-term exam.

parent 6055421b
...@@ -173,31 +173,32 @@ Although the course has changed, you may still have a look at previous exams ...@@ -173,31 +173,32 @@ Although the course has changed, you may still have a look at previous exams
available with solutions: available with solutions:
- mid-term exam 2017-2018: - mid-term exam 2017-2018:
[Call-by-name. Extensible records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2017-2018.pdf) [Encoding call-by-name into call-by-value; extensible records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2017-2018.pdf)
([Coq solution of part 1](coq/LambdaCalculusEncodingCBNIntoCBV.v)).
- mid-term exam 2016-2017: - mid-term exam 2016-2017:
[Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf) [Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf).
- mid-term exam 2015-2016: - mid-term exam 2015-2016:
[Type containment](http://gallium.inria.fr/~remy/mpri/exams/partiel-2015-2016.pdf) [Type containment](http://gallium.inria.fr/~remy/mpri/exams/partiel-2015-2016.pdf).
- final exam 2014-2015: [Copatterns](http://gallium.inria.fr/~remy/mpri/exams/final-2014-2015.pdf) - final exam 2014-2015:
[Copatterns](http://gallium.inria.fr/~remy/mpri/exams/final-2014-2015.pdf).
- mid-term exam 2014-2015: - mid-term exam 2014-2015:
[Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf) [Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf).
- final exam 2013-2014: - final exam 2013-2014:
[Operation on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf) [Operations on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf).
- mid-term exam 2013-2014: - mid-term exam 2013-2014:
[Typechecking Effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf) [Typechecking effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf).
- final exam 2012-2013: - final exam 2012-2013:
[Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf) [Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf).
- mid-term exam 2012-2013: - mid-term exam 2012-2013:
[Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf) [Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf).
- final exam 2011-2012: - final exam 2011-2012:
[Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf) [Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf).
- mid-term exam 2011-2012: - mid-term exam 2011-2012:
[Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf) [Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf).
- final exam 2010-2011: - final exam 2010-2011:
[Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf) [Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf).
- mid-term exam 2010-2011: - mid-term exam 2010-2011:
[Compilation [Compilation of polymorphic records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2010-2011.pdf).
of polymorphic records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2010-2011.pdf)
## Recommended software ## Recommended software
......
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusFreeVars.
Require Import LambdaCalculusReduction.
(* This file defines an encoding of call-by-name into call-by-value. This is a
simple encoding, based on two combinators [delay] and [force]. [delay] is
implemented as a function which ignores its argument, and [force] as a
function call with a dummy actual argument. The proof of semantic
preservation involves parallel call-by-value reduction. *)
(* -------------------------------------------------------------------------- *)
(* To delay the evaluation of [t], we wrap it in a function which ignores its
argument. *)
Definition delay t :=
Lam (lift 1 t).
(* To force the evaluation of a thunk (a delayed computation), we apply it to
a dummy actual argument. *)
Definition dummy :=
Lam (Var 0).
Definition force t :=
App t dummy.
(* The key property that is expected of [force] and [delay] is of course that
[force (delay t)] reduces to [t] under call-by-value reduction. *)
Lemma force_delay:
forall t,
cbv (force (delay t)) t.
Proof.
intros. unfold force, delay. econstructor; obvious. autosubst.
Qed.
(* Obviously, [delay] and [force] commute with substitutions. *)
Lemma delay_subst:
forall t sigma,
(delay t).[sigma] = delay t.[sigma].
Proof.
unfold delay. intros. autosubst.
Qed.
Lemma force_subst:
forall t sigma,
(force t).[sigma] = force t.[sigma].
Proof.
unfold force. intros. autosubst.
Qed.
(* Finally, although ordinary reduction under [delay is not permitted,
parallel reduction under [delay] is permitted. *)
Lemma pcbv_delay:
forall t1 t2,
pcbv t1 t2 ->
pcbv (delay t1) (delay t2).
Proof.
unfold delay. intros. econstructor; eauto using red_subst with obvious.
Qed.
Local Hint Resolve pcbv_delay : obvious.
(* That is all we need to know about [force] and [delay]. We now make them
opaque, so as to prevent their unfolding during the proofs that follow. *)
Opaque force delay.
(* -------------------------------------------------------------------------- *)
(* This is the encoding of call-by-name into call-by-value. It is simple:
in short, in every application, the actual argument is wrapped in a
[delay]; accordingly, every use of a variable involves a [force]. *)
Fixpoint encode (t : term) :=
match t with
| Var x =>
force (Var x)
| Lam t =>
Lam (encode t)
| App t1 t2 =>
App (encode t1) (delay (encode t2))
| Let t1 t2 =>
Let (delay (encode t1)) (encode t2)
end.
(* -------------------------------------------------------------------------- *)
(* A naive attempt at a simulation diagram, which (if it were true) would
imply semantic preservation. *)
Lemma encode_simulation:
forall t1 t2,
cbn t1 t2 ->
cbv (encode t1) (encode t2).
Proof.
induction 1; intros; subst; simpl; try solve [ tauto ].
(* Beta *)
{ econstructor; eauto.
(* This fails because [encode] does not quite commute with
substitution. The intuition is, it almost commutes, but
this introduces [force/delay] pairs. *)
Abort.
(* -------------------------------------------------------------------------- *)
(* [encode] commutes with renamings. *)
Lemma encode_renaming:
forall t sigma,
is_ren sigma ->
(encode t).[sigma] = encode t.[sigma].
Proof.
induction t; intros; asimpl;
repeat rewrite delay_subst;
repeat f_equal; obvious.
(* Var *)
{ pick is_ren invert. reflexivity. }
Qed.
Lemma encode_lift:
forall t k,
lift k (encode t) = encode (lift k t).
Proof.
eauto using encode_renaming with obvious.
Qed.
(* -------------------------------------------------------------------------- *)
(* In order to express the fact that [encode] commutes with substitutions, we
define the following relation between substitutions. *)
(* [sigma1] is a target-level substitution, intended to be applied after
[encode], whereas [sigma2] is a source-level substitution, intended to be
applied before [encode]. *)
(* Because [sigma1] typically maps variables to terms that have a [delay] at
the root, we allow [force (sigma1 x)] to reduce to [encode (sigma2 x)].
We use parallel reduction [pcbv], even though we could perhaps use a
slightly more precise relation at this point (such as "at most one step
of [cbv]") because it is convenient and [pcbv] must be used in the
conclusion of the lemma [encode_subst] anyway. *)
Local Definition related (sigma1 sigma2 : var -> term) :=
forall x, pcbv (force (sigma1 x)) (encode (sigma2 x)).
(* This relation is preserved by [up]. *)
Local Lemma up_related:
forall sigma1 sigma2,
related sigma1 sigma2 ->
related (up sigma1) (up sigma2).
Proof.
unfold related. intros. destruct x as [|x]; asimpl.
(* Variable 0. This case goes through because [pcbv] is reflexive. *)
{ eapply red_refl; obvious. }
(* Variables above 0. This case goes through because [force], [encode]
and [pcbv] are compatible with [lift 1]. *)
{ rewrite <- force_subst.
rewrite <- encode_lift.
eapply red_subst; obvious. }
Qed.
Local Hint Resolve up_related : obvious.
(* [encode] commutes with substitutions in the following sense. *)
Local Lemma encode_subst:
forall t sigma1 sigma2,
related sigma1 sigma2 ->
pcbv
(encode t).[sigma1]
(encode t.[sigma2]).
Proof.
induction t; simpl; intros; subst;
repeat rewrite force_subst;
repeat rewrite delay_subst;
eauto 6 with obvious.
Qed.
(* We obtain the following corollary for singleton substitutions. *)
Local Lemma encode_subst_singleton:
forall t1 t2,
pcbv
(encode t1).[delay (encode t2)/]
(encode t1.[t2/]).
Proof.
intros.
eapply encode_subst.
intros [|x]; asimpl.
(* Variable 0. This case goes through by [force_delay]. *)
{ eauto using cbv_subset_pcbv, force_delay. }
(* Variables above 0. This case goes through because [pcbv] is reflexive. *)
{ eapply red_refl; obvious. }
Qed.
(* -------------------------------------------------------------------------- *)
(* Equipped with the previous substitution lemma, it is straightforward to
establish the following simulation diagram: if [t1] steps to [t2] under
call-by-name reduction, then [encode t1] steps to [encode t2] in at
least one step of parallel call-by-value reduction. *)
Lemma encode_simulation:
forall t1 t2,
cbn t1 t2 ->
plus pcbv (encode t1) (encode t2).
Proof.
induction 1; simpl; intros; subst; try solve [ tauto ].
(* Beta. Two steps of reduction are required. *)
{ econstructor. { eauto using cbv_subset_pcbv with obvious. }
econstructor. { eauto using encode_subst_singleton. }
finished. eauto. }
(* Let. Two steps of reduction are required. *)
{ econstructor. { eauto using cbv_subset_pcbv with obvious. }
econstructor. { eauto using encode_subst_singleton. }
finished. eauto. }
(* AppL. Just perform reduction under a context. *)
{ obvious. }
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment