Compilation to the Modern SECD abstract machine and its proof of correctness.

Require Omega.
Require Import List.
Require Import Sequences.

Source language

Syntax with de Bruijn indices.

Big-step semantics with environments and closures.

A value is either an integer or a closure of a term by an environment.

Inductive value: Type :=
| Int: const -> value
| Clos: term -> list value -> value.

An environment is a list of values. Element number N of the list is the value of variable having de Bruijn index N.

Definition env := list value.

Looking up the N-th element of an environment.

Fixpoint lookup {A: Type} (n: nat) (l: list A) {struct l}: option A :=
  match l, n with
  | nil, _ => None
  | x :: l', O => Some x
  | x :: l', S n' => lookup n' l'
  end.

eval e a v means "in environment e, term a evaluates to value v".

Inductive eval: env -> term -> value -> Prop :=
  | eval_Var: forall e n v,
      lookup n e = Some v ->
      eval e (Var n) v
  | eval_Const: forall e i,
      eval e (Const i) (Int i)
  | eval_Fun: forall e a,
      eval e (Fun a) (Clos a e)
  | eval_Let: forall e a b va vb,
      eval e a va -> eval (va :: e) b vb ->
      eval e (Let a b) vb
  | eval_App: forall e a b ca ea vb v,
      eval e a (Clos ca ea) ->
      eval e b vb ->
      eval (vb :: ea) ca v ->
      eval e (App a b) v.

evalinf e a v means "in environment e, term a diverges".

CoInductive evalinf: env -> term -> Prop :=
  | evalinf_Let_l: forall e a b,
      evalinf e a ->
      evalinf e (Let a b)
  | evalinf_Let_r: forall e a b va,
      eval e a va -> evalinf (va :: e) b ->
      evalinf e (Let a b)
  | evalinf_App_l: forall e a b,
      evalinf e a ->
      evalinf e (App a b)
  | evalinf_App_r: forall e a b v,
      eval e a v ->
      evalinf e b ->
      evalinf e (App a b)
  | evalinf_App_f: forall e a b ca ea vb,
      eval e a (Clos ca ea) ->
      eval e b vb ->
      evalinf (vb :: ea) ca ->
      evalinf e (App a b).

Abstract machine: the Modern SECD

Instruction set.

Machine values and environments.

Inductive mvalue: Type :=
| MInt: const -> mvalue
| MClos: code -> list mvalue -> mvalue.

Definition menv := list mvalue.

Stacks.

Inductive slot: Type :=
| Value: mvalue -> slot (* a value on the stack *)
| Return: code -> menv -> slot. (* a return frame *)

Definition stack := list slot.

A state of the machine is a triple of a piece of code, a machine environment, and a stack.

Definition state : Type := (code * menv * stack)%type.

One transition of the machine.

Inductive transition: state -> state -> Prop :=
  | trans_IAccess: forall n k e s v,
      lookup n e = Some v ->
      transition (IAccess n :: k, e, s)
                 (k, e, Value v :: s)
  | trans_IConst: forall n k e s,
      transition (IConst n :: k, e, s)
                 (k, e, Value (MInt n) :: s)
  | trans_IClosure: forall c k e s,
      transition (IClosure c :: k, e, s)
                 (k, e, Value (MClos c e) :: s)
  | trans_IApp: forall k e v k' e' s,
      transition (IApp :: k, e, Value v :: Value (MClos k' e') :: s)
                 (k', v :: e', Return k e :: s)
  | trans_ITailApp: forall k e v k' e' s,
      transition (ITailApp :: k, e, Value v :: Value (MClos k' e') :: s)
                 (k', v :: e', s)
  | trans_ILet: forall k e v s,
      transition (ILet :: k, e, Value v :: s)
                 (k, v :: e, s)
  | trans_IEndLet: forall k e v s,
      transition (IEndLet :: k, v :: e, s)
                 (k, e, s)
  | trans_IReturn: forall k e v k' e' s,
      transition (IReturn :: k, e, Value v :: Return k' e' :: s)
                 (k', e', Value v :: s).

Executing code with the machine.

Definition mach_terminates (k: code) (v: mvalue) : Prop :=
star transition (k, nil, nil) (nil, nil, Value v :: nil).

Definition mach_diverges (k: code) : Prop :=
infseq transition (k, nil, nil).

Compilation and its correctness.

The compilation scheme. compile a k prepends the code for term a to the code k. The code for a evaluates a and deposits its value on top of the stack.

Fixpoint compile (a: term) (k: code) : code :=
  match a with
  | Var n => IAccess n :: k
  | Const i => IConst i :: k
  | Fun b => IClosure (compile b (IReturn :: nil)) :: k
  | Let b c => compile b (ILet :: compile c (IEndLet :: k))
  | App b c => compile b (compile c (IApp :: k))
  end.

Extension to values and environments

Fixpoint compile_value (v: value) : mvalue :=
  match v with
  | Int n => MInt n
  | Clos a e =>
      let fix compenv (e: env) : menv :=
        match e with
        | nil => nil
        | v :: e' => compile_value v :: compenv e'
        end in
      MClos (compile a (IReturn :: nil)) (compenv e)
  end.

Fixpoint compile_env (e: env) : menv :=
   match e with
   | nil => nil
   | v :: e' => compile_value v :: compile_env e'
   end.

Lemma lookup_compile:
  forall e n v,
  lookup n e = Some v ->
  lookup n (compile_env e) = Some (compile_value v).

Proof.

induction e; destruct n; simpl; intros; auto; congruence.
Qed.

Compiler correctness for terminating programs.

Lemma compile_eval:
  forall e a v,
  eval e a v ->
  forall k s,
  plus transition (compile a k, compile_env e, s)
                  (k, compile_env e, Value (compile_value v) :: s).

Proof.

  induction 1; simpl; intros.
- (* Var *)
  apply plus_one. constructor. apply lookup_compile; auto.
- (* Const *)
  apply plus_one. constructor.
- (* Closure *)
  apply plus_one. constructor.
- (* Let *)
  eapply plus_trans; eauto.
  eapply plus_left. constructor.
  eapply star_trans. apply plus_star. eauto.
  apply star_one. constructor.
- (* App *)
  eapply plus_trans; eauto.
  eapply plus_trans; eauto.
  eapply plus_left.
    change (compile_value (Clos ca ea))
      with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
    constructor.
  eapply star_trans. apply plus_star. eauto.
  apply star_one. constructor.
Qed.

Theorem compile_terminates:
forall a v,
eval nil a v -> mach_terminates (compile a nil) (compile_value v).

Proof.

intros. red. apply plus_star. apply compile_eval with (e := nil). auto.
Qed.

Compiler correctness for diverging programs.

Inductive diverging_state : state -> Prop :=
  | diverging_state_intro: forall e a k s,
      evalinf e a ->
      diverging_state (compile a k, compile_env e, s).

Lemma diverging_states_productive:
  forall S,
  diverging_state S ->
  exists S', plus transition S S' /\ diverging_state S'.

Proof.

  intros. inversion H; subst. clear H. revert a e k s H0.
  induction a; intros e k s EVALINF; inversion EVALINF; subst; simpl.
- (* divergence left of a Let *)
  apply IHa1. auto.
- (* divergence right of a Let *)
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_intro with (e := va :: e). auto.
- (* divergence left of an App *)
  apply IHa1. auto.
- (* divergence right of an App *)
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
- (* divergence after beta reduction *)
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
  constructor.
  apply diverging_state_intro with (e := vb :: ea). auto.
Qed.

Theorem compile_diverges:
forall a, evalinf nil a -> mach_diverges (compile a nil).

Proof.

  intros; red.
  apply infseq_coinduction_principle_2 with (X := diverging_state).
  exact diverging_states_productive.
  apply diverging_state_intro with (e := nil). auto.
Qed.

Adding tail call optimization

Module WithTailCalls.

The revised compilation scheme.

compile a k prepends the code for term a to the code k. The code for a evaluates a and deposits its value on top of the stack.
tailcompile a produces code that evaluates a and returns the value of a to the caller.

Note mutual recursion: tailcompile uses compile for sub-terms that are not in tail position; compile uses tailcompile for the bodies of Fun abstractions.

Fixpoint compile (a: term) (k: code) : code :=
  match a with
  | Var n => IAccess n :: k
  | Const i => IConst i :: k
  | Fun b => IClosure (tailcompile b) :: k
  | Let b c => compile b (ILet :: compile c (IEndLet :: k))
  | App b c => compile b (compile c (IApp :: k))
  end

with tailcompile (a: term) : code :=
  match a with
  | Var n => IAccess n :: IReturn :: nil
  | Const i => IConst i :: IReturn :: nil
  | Fun b => IClosure (tailcompile b) :: IReturn :: nil
  | Let b c => compile b (ILet :: tailcompile c)
  | App b c => compile b (compile c (ITailApp :: nil))
  end.

Extension to values and environments.

Fixpoint compile_value (v: value) : mvalue :=
  match v with
  | Int n => MInt n
  | Clos a e =>
      let fix compenv (e: env) : menv :=
        match e with
        | nil => nil
        | v :: e' => compile_value v :: compenv e'
        end in
      MClos (tailcompile a) (compenv e)
  end.

Fixpoint compile_env (e: env) : menv :=
   match e with
   | nil => nil
   | v :: e' => compile_value v :: compile_env e'
   end.

Lemma lookup_compile:
  forall e n v,
  lookup n e = Some v ->
  lookup n (compile_env e) = Some (compile_value v).

Proof.

induction e; destruct n; simpl; intros; auto; congruence.
Qed.

Compiler correctness for terminating programs.

Lemma compile_eval_gen:
  forall e a v,
  eval e a v ->
  (forall k s,
   plus transition (compile a k, compile_env e, s)
                   (k, compile_env e, Value (compile_value v) :: s))
  /\
  (forall s k e',
   plus transition (tailcompile a, compile_env e, Return k e' :: s)
                   (k, e', Value (compile_value v) :: s)).

Proof.

  induction 1; split; simpl; intros.
- (* Var, non-tail *)
  apply plus_one. constructor. apply lookup_compile; auto.
- (* Var, tail *)
  eapply plus_left. constructor. apply lookup_compile; eauto.
  apply star_one. constructor.
- (* Const, non-tail *)
  apply plus_one. constructor.
- (* Const, tail *)
  eapply plus_left. constructor.
  apply star_one. constructor.
- (* Closure, non-tail *)
  apply plus_one. constructor.
- (* Const, tail *)
  eapply plus_left. constructor.
  apply star_one. constructor.
- (* Let, non-tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_left. constructor.
  eapply star_trans. apply plus_star. eapply IHeval2.
  apply star_one. constructor.
- (* Let, tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_left. constructor.
  apply plus_star. eapply IHeval2.
- (* App, non-tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_trans. eapply IHeval2.
  eapply plus_left.
  change (compile_value (Clos ca ea))
    with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply plus_star. apply IHeval3.
- (* App, tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_trans. eapply IHeval2.
  eapply plus_left.
  change (compile_value (Clos ca ea))
    with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply plus_star. apply IHeval3.
Qed.

Lemma compile_eval:
  forall e a v k s,
  eval e a v ->
  plus transition (compile a k, compile_env e, s)
                  (k, compile_env e, Value (compile_value v) :: s).

Proof.

intros. apply (proj1 (compile_eval_gen _ _ _ H)).
Qed.

Lemma tailcompile_eval:
  forall e a v s k e',
  eval e a v ->
  plus transition (tailcompile a, compile_env e, Return k e' :: s)
                  (k, e', Value (compile_value v) :: s).

Proof.

intros. apply (proj2 (compile_eval_gen _ _ _ H)).
Qed.

Theorem compile_terminates:
forall a v,
eval nil a v -> mach_terminates (compile a nil) (compile_value v).

Proof.

intros. red. apply plus_star. apply compile_eval with (e := nil). auto.
Qed.

Compiler correctness for diverging programs.

Inductive diverging_state : state -> Prop :=
  | diverging_state_nontail: forall e a k s,
      evalinf e a ->
      diverging_state (compile a k, compile_env e, s)
  | diverging_state_tail: forall e a s,
      evalinf e a ->
      diverging_state (tailcompile a, compile_env e, s).

Lemma diverging_states_productive:
  forall S,
  diverging_state S ->
  exists S', plus transition S S' /\ diverging_state S'.

Proof.

  assert (NONTAIL: forall a e s k,
    evalinf e a ->
      exists S', plus transition (compile a k, compile_env e, s) S' /\ diverging_state S').
  induction a; intros e s k EVALINF; inversion EVALINF; subst; simpl.
  apply IHa1. auto.
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_nontail with (e := va :: e). auto.
  apply IHa1. auto.
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply diverging_state_tail with (e := vb :: ea). auto.

  assert (TAIL: forall a e s,
    evalinf e a ->
      exists S', plus transition (tailcompile a, compile_env e, s) S' /\ diverging_state S').
  intros. inversion H; subst; clear H; simpl.
  apply NONTAIL. auto.
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_tail with (e := va :: e). auto.
  apply NONTAIL. auto.
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply diverging_state_tail with (e := vb :: ea). auto.

  intros. inversion H; subst; auto.
Qed.

Theorem compile_diverges:
forall a, evalinf nil a -> mach_diverges (compile a nil).

Proof.

  intros; red.
  apply infseq_coinduction_principle_2 with (X := diverging_state).
  exact diverging_states_productive.
  apply diverging_state_nontail with (e := nil). auto.
Qed.

End WithTailCalls.

Module Compiler

Source language

Big-step semantics with environments and closures.

Abstract machine: the Modern SECD

Compilation and its correctness.

Adding tail call optimization