Definition of the conversion

The conversion introduces new variables named "k", "v1" and "v2". It is crucial that these variables do not conflict with variables coming from the source program. To ensure this, the conversion renames those variables by prepending them with an "x".

Definition rename (v: var): var := String.append "x" v.

This is Plotkin's CPS conversion.

Fixpoint cps (a: term): term :=
  match a with
  | Var x =>
      Fun "k" (App (Var "k") (Var (rename x)))
  | Const n =>
      Fun "k" (App (Var "k") (Const n))
  | Fun x a =>
      Fun "k" (App (Var "k") (Fun (rename x) (cps a)))
  | App a b =>
      Fun "k" (App (cps a)
        (Fun "v1" (App (cps b)
           (Fun "v2" (App (App (Var "v1") (Var "v2")) (Var "k"))))))
  end.

The CPS conversion of a value has a specific shape.

Definition cps_value (a: term): term :=
  match a with
  | Const n => Const n
  | Fun x a => Fun (rename x) (cps a)
  | _ => Const 0 (* never happens *)
  end.

Lemma cps_of_value:
  forall v, isvalue v -> cps v = Fun "k" (App (Var "k") (cps_value v)).

Proof.

destruct 1; auto.
Qed.

Lemma cps_value_is_value:
forall a, isvalue (cps_value a).

Proof.

intros. destruct a; constructor.
Qed.

Hint Resolve cps_value_is_value: sem.

Reasoning about free variables

notfree v a holds if variable v does not occur free in term a.

Fixpoint notfree (v: var) (a: term) : Prop :=
  match a with
  | Var x => x <> v
  | Const n => True
  | Fun x a => x = v \/ notfree v a
  | App a b => notfree v a /\ notfree v b
  end.

Substituting a non-free variable leaves a term unchanged.

Lemma dec_eq_true:
forall (A B: Type) (eq: forall (x y: A), {x=y} + {x<>y}) x (a b: B),
(if eq x x then a else b) = a.

Proof.

intros. destruct (eq x x); congruence.
Qed.

Lemma dec_eq_false:
forall (A B: Type) (eq: forall (x y: A), {x=y} + {x<>y}) x y (a b: B),
x <> y -> (if eq x y then a else b) = b.

Proof.

intros. destruct (eq x y); congruence.
Qed.

Lemma notfree_subst:
forall b v a, notfree v a -> subst v b a = a.

Proof.

induction a; simpl; intros.
- apply dec_eq_false; auto.
- auto.
- destruct (var_eq v v0); auto. f_equal. apply IHa. intuition congruence.
- destruct H. f_equal; auto.
Qed.

The temporary variables "k", "v1" and "v2" are never free in CPS-converted terms.

Definition no_temp_free (a: term): Prop :=
notfree "k" a /\ notfree "v1" a /\ notfree "v2" a.

Lemma cps_no_temp_free:
forall a, no_temp_free (cps a).

Proof.

unfold no_temp_free; induction a; simpl; unfold rename; simpl; intuition congruence.
Qed.

Hint Resolve cps_no_temp_free: cps.

CPS conversion preserves semantics

Commutation between substitution and CPS conversion.

Lemma subst_k: forall a b, no_temp_free a -> subst "k" b a = a.

Proof.

intros a b (P & Q & R). apply notfree_subst; auto.
Qed.

Lemma subst_v1: forall a b, no_temp_free a -> subst "v1" b a = a.

Proof.

intros a b (P & Q & R). apply notfree_subst; auto.
Qed.

Lemma subst_v2: forall a b, no_temp_free a -> subst "v2" b a = a.

Proof.

intros a b (P & Q & R). apply notfree_subst; auto.
Qed.

Lemma cps_subst:
forall x v, isvalue v ->
forall a, cps (subst x v a) = subst (rename x) (cps_value v) (cps a).

Proof.

Local Opaque var_eq.
  induction a; simpl.
- unfold rename, String.append. symmetry.
  repeat rewrite dec_eq_false by congruence.
  destruct (var_eq x v0).
  subst v0. rewrite dec_eq_true. symmetry. apply cps_of_value; auto.
  rewrite dec_eq_false by congruence. auto.
- unfold rename, String.append. repeat rewrite dec_eq_false by congruence. auto.
- symmetry. unfold rename, String.append.
  repeat rewrite dec_eq_false by congruence.
  destruct (var_eq x v0).
  subst v0. rewrite dec_eq_true. auto.
  rewrite dec_eq_false by congruence. rewrite IHa. auto.
- unfold rename, String.append. repeat rewrite dec_eq_false by congruence.
  rewrite IHa1, IHa2. auto.
Qed.

The application of cps a to a continuation k evaluates like evaluating a to a value v, then applying k to cps_value v.

Theorem eval_cps:
  forall a v, eval a v ->
  forall k r, isvalue k -> no_temp_free k ->
  eval (App k (cps_value v)) r -> eval (App (cps a) k) r.

Proof.

Local Transparent var_eq.
  induction 1; intros k r VK TK EK; simpl in *.
- (* constant *)
  eauto with sem.
- (* function *)
  econstructor; eauto with sem. simpl. rewrite subst_k by auto with cps. auto.
- (* application *)
  econstructor; eauto with sem. simpl.
  rewrite subst_k by auto with cps.
  apply IHeval1; auto with sem.
  unfold no_temp_free; simpl. rewrite subst_k by auto with cps.
  destruct (cps_no_temp_free b) as (P & Q & R).
  destruct TK as (X & Y & Z).
  intuition (try congruence).
  econstructor; eauto with sem. simpl.
  rewrite subst_k by auto with cps.
  rewrite subst_v1 by auto with cps.
  apply IHeval2; auto with sem.
  unfold no_temp_free; simpl. rewrite subst_v1 by auto with cps.
  destruct (cps_no_temp_free c) as (P & Q & R).
  destruct TK as (X & Y & Z).
  intuition (try congruence).
  econstructor; eauto with sem.
  simpl. rewrite subst_v1 by auto. rewrite ! subst_v2 by auto with cps.
  assert (E: eval (App (cps (subst x vb c)) k) r) by auto.
  rewrite cps_subst in E by eauto with sem. inversion E; subst.
  eauto with sem.
Qed.

As a corollary, we obtain that applying cps a to the initial continuation evaluates to cps_value v, where v is the value of a.

Corollary eval_cps_program:
forall a v, eval a v -> eval (App (cps a) (Fun "v" (Var "v"))) (cps_value v).

Proof.

  intros. apply eval_cps with v; auto with sem.
  red; simpl; intuition congruence.
  eauto with sem.
Qed.

Module CPS

Definition of the conversion

Reasoning about free variables

CPS conversion preserves semantics