Master Thesis, Page 10 This file contains operational semantics, context semantics and bigstep semantics as well as the definition of normal forms, normality and evaluation

Set Implicit Arguments.
Require Import Omega Logic List Classes.Morphisms.
Import List Notations.

Require Export CBPV.Terms CBPV.Base CBPV.AbstractReductionSystems.
Import CommaNotation.

Semantics

Reserved Notation "A '≽' B" (at level 80).
Reserved Notation "A '⇝' B" (at level 80).

Primitive Reduction

Inductive pstep {n: nat}: comp n -> comp n -> Prop :=
| pstepForce (c: comp n):
    <{c }>! ≽ c
| pstepApp (c: comp (S n)) (c': comp n) v:
    c [v..] = c' -> (lambda c) v ≽ c'
| pstepProj (b: bool) (c c1 c2: comp n) :
    (c = if b then c1 else c2 ) -> proj b (tuple c1 c2) ≽ c
| pstepLetin (c: comp (S n)) c' v:
    c [v..] = c' -> $ <- (ret v ); c ≽ c'
| pstepCaseS v (b: bool) c (c1 c2: comp (S n)):
    (if b then c1 else c2 )[v..] = c -> caseS (inj b v) c1 c2 ≽ c
| pstepCaseP v1 v2 (c: comp (S (S n))) c':
    c [v2 ,v1..] = c' -> caseP (pair v1 v2) c ≽ c'
where "A '≽' B" := (pstep A B).

Operational Semantics

Inductive step {n: nat}: comp n -> comp n -> Prop :=
| stepPrimitive (c c': comp n) : c ≽ c' -> c > c'
| stepApp (c c': comp n) v: c > c' -> c v > c' v
| stepProj (c c': comp n) b: c > c' -> proj b c > proj b c'
| stepLetin (c1 c1': comp n) c2: c1 > c1' -> $ <- c1 ; c2 > $ <- c1'; c2
where "A > B" := (step A B).

Hint Constructors pstep step.

Notation "A >* B" := (star step A B) (at level 60).
Notation "A >+ B" := (plus step A B) (at level 60).

Context Semantics

Evaluation context

Inductive ectx {n: nat}: Type :=
| ectxHole : ectx
| ectxApp : ectx -> value n -> ectx
| ectxProj : bool -> ectx -> ectx
| ectxLetin : ectx -> comp (S n) -> ectx.

Context filling

Fixpoint fill {n: nat} (K: ectx) (c: comp n) :=
  match K with
  | ectxHole => c
  | ectxApp K v => (fill K c) v
  | ectxProj b K => proj b (fill K c)
  | ectxLetin K c' => letin (fill K c) c'
  end.

Context Semantics

Inductive cstep {n: nat}: comp n -> comp n -> Prop :=
| contextStep C c c' (c'' c''': comp n):
c ≽ c' -> fill C c = c'' -> fill C c' = c''' -> c'' ⇝ c'''
where "A '⇝' B" := (cstep A B).

Bigstep Semantics

Reserved Notation "A ▷ B" (at level 80).

Inductive bigstep {n: nat}: comp n -> comp n -> Prop :=
| bigstepCu: @cu n ▷ cu
| bigstepReturn (v: value n) : ret v ▷ ret v
| bigstepLambda (c: comp (S n)) : lambda c ▷ lambda c
| bigstepTuple (c1 c2: comp n): tuple c1 c2 ▷ tuple c1 c2
| bigstepForce (c c': comp n): c ▷ c' -> <{c }>! ▷ c'
| bigstepApp (c c'': comp n) c' v: c ▷ lambda c' -> c'[v..] ▷ c'' -> c v ▷ c''
| bigstepProj c c' (c1 c2: comp n) (b: bool):
    c ▷ tuple c1 c2 -> (if b then c1 else c2 ) ▷ c' -> proj b c ▷ c'
| bigstepLetin c1 (v: value n) c2 c: c1 ▷ ret v -> c2 [v..] ▷ c -> $ <- c1 ; c2 ▷ c
| bigstepCaseS c c1 c2 (b: bool) (v: value n):
    (if b then c1 else c2 )[v..] ▷ c -> caseS (inj b v) c1 c2 ▷ c
| bigstepCaseP c c' (v1 v2: value n):
    c [v2 ,v1..] ▷ c' -> caseP (pair v1 v2) c ▷ c'
where "A ▷ B" := (bigstep A B).

Hint Constructors bigstep.

Normal Form

Inductive nf {n: nat}: comp n -> Prop :=
| nfCu: nf cu
| nfLam c: nf (lambda c)
| nfTup c1 c2: nf (tuple c1 c2)
| nfRet v: nf (ret v).

Hint Constructors nf.

Evaluation

Definition eval {n: nat} (c c': comp n) := c >* c' /\ nf c'.
Hint Transparent eval.

Properties

Instance proper_letin {n: nat}: Proper (star step ++> eq ++> star step) (@letin n).
Proof.
  intros c1 c1' H ? c2 ->.
  induction H; eauto.
Qed.

Instance proper_app {n: nat}: Proper (star step ++> eq ++> star step) (@app n).
Proof.
  intros c1 c1' H ? c2 ->.
  induction H; eauto.
Qed.

Instance proper_proj {n: nat}: Proper (eq ++> star step ++> star step) (@proj n).
Proof.
  intros ? i -> c c' H.
  induction H; eauto.
Qed.

Hint Resolve proper_letin proper_app proper_proj.

Reduction tactic for beta reduction step

Ltac reduce := econstructor 2; [ solve [eauto] | cbn ].

Substitution Primitive Step

Lemma pstep_subst m n (C1 C2: comp m) (f: fin m -> value n):
C1 ≽ C2 -> C1 [f ] ≽ C2 [f ].
Proof.
intros H; inv H; cbn; constructor; try destruct b; asimpl; reflexivity.
Qed.

The operational semantic we defined is functional

Lemma step_functional {n: nat} (c1 c2 c2': comp n) : c1 > c2 -> c1 > c2' -> c2 = c2'.
Proof.
  induction 1 in c2' |-*; intros H1; inv H1.
  1: inv H; inv H0; reflexivity.
  all: try (inv H; inv H0; inv H).
  all: try (inv H0; inv H; inv H0).
  all: firstorder congruence.
Qed.

Lemma confluence_steps (n: nat):
  confluent (@step n).
Proof.
  apply confluent_semi.
  intros x y z H1 H2.
  destruct H2.
  - exists y; eauto.
  - exists y0; eauto. specialize (step_functional H1 H) as ->; eauto.
Qed.

Hint Resolve confluence_steps.

The operational semantic and the context semantic agree

Lemma step_equiv {n: nat} (c c': comp n): c > c' <-> c ⇝ c'.
Proof.
  split.
  - induction 1.
    + eapply (contextStep ectxHole); eauto.
    + inv IHstep; eapply (contextStep (ectxApp C v)); eauto.
    + inv IHstep; eapply (contextStep (ectxProj b C)); eauto.
    + inv IHstep; eapply (contextStep (ectxLetin C c2)); eauto.
  - destruct 1; subst c''; subst c'''.
    induction C in c, c', H |-*; cbn; eauto.
Qed.

The bigstep semantic is sound w.r.t the operational semantic

Lemma bigstep_soundness {n: nat} (c c': comp n): c ▷ c' -> c >* c'.
Proof.
  induction 1; eauto.
  - rewrite IHbigstep1; reduce; rewrite IHbigstep2; reflexivity.
  - rewrite IHbigstep1; reduce; assumption.
  - rewrite IHbigstep1; reduce; rewrite IHbigstep2; reflexivity.
Qed.

The bigstep semantic is closed under expasion by the operational semantics

Lemma bigstep_primitive_cons {n: nat} (c c' c'': comp n): c ≽ c' -> c' ▷ c'' -> c ▷ c''.
Proof.
  intros H; inv H; intros H; econstructor; eauto.
Qed.

Lemma bigstep_cons {n: nat} (c c' c'': comp n): c > c' -> c' ▷ c'' -> c ▷ c''.
Proof.
  induction 1 in c'' |-*.
  1: now apply bigstep_primitive_cons.
  all: intros H1; inv H1; eauto.
Qed.

Lemma bigstep_prepend {n: nat} (c c' c'': comp n): c >* c' -> c' ▷ c'' -> c ▷ c''.
Proof.
  induction 1 in c'' |-*; intros; eauto using bigstep_cons.
Qed.

Hint Resolve bigstep_cons bigstep_prepend.

The bigstep semantic is functional

Lemma bigstep_functional {n: nat} (c1 c2 c2': comp n) : c1 ▷ c2 -> c1 ▷ c2' -> c2 = c2'.
Proof.
induction 1 in c2' |-*; intros H1; inv H1; eauto.
all: specialize (IHbigstep1 _ H4); injection IHbigstep1; repeat intros ->; apply IHbigstep2; eauto.
Qed.

Normal forms are normal

Lemma nf_normal {n: nat} (c: comp n) : nf c -> Normal step c.
Proof. intros [] c' H; inv H; inv H0. Qed.

Terms bigstep evaluate to normal forms

Lemma bigstep_normal {n: nat} (c c': comp n): c ▷ c' -> nf c'.
Proof.
induction 1; eauto.
Qed.

Normal forms bigstep evaluate

Lemma normal_bigstep {n: nat} (c: comp n): nf c -> c ▷ c.
Proof.
intros []; eauto.
Qed.

Bigstep evaluation is evaluation

Lemma eval_bigstep {n: nat} (c c': comp n): eval c c' <-> c ▷ c'.
Proof.
  split.
  - intros [H1 H2]; induction H1; eauto using normal_bigstep, bigstep_cons.
  - intros H; split; eauto using bigstep_normal, bigstep_soundness.
Qed.

Lemma ectx_decompose {n: nat} (K : @ectx n) c c':
  fill K c ▷ c' -> exists c'', c ▷ c'' /\ fill K c'' ▷ c'.
Proof.
  induction K in c, c' |-*; cbn; intros H.
  1: eexists; intuition; eauto; induction H; eauto.
  all: inv H; edestruct IHK; eauto; intuition.
  all: eexists; intuition; eauto.
Qed.

Lemma ectx_compose {n: nat} (K : @ectx n) c c' c'':
  c ▷ c' -> fill K c' ▷ c'' -> fill K c ▷ c''.
Proof.
  intros H1 H2.
  eapply eval_bigstep in H1.
  eapply eval_bigstep in H2.
  eapply eval_bigstep.
  unfold eval in *; intuition.
  rewrite <-H1.
  clear H0 H3 H1; induction K; cbn in *; eauto;
    now rewrite IHK.
Qed.

Lemma eval_evaluates n (c c': comp n):
  evaluates step c c' -> nf c' -> eval c c'.
Proof.
  split; eauto. destruct H; eauto.
Qed.

Lemma steps_nf_eval n (c c': comp n):
    c >* c' -> nf c' -> eval c c'.
Proof.
  split; eauto.
Qed.

Lemma steps_bigstep n (c c': comp n):
    c >* c' -> nf c' -> c ▷ c'.
Proof.
  intros; eapply eval_bigstep, steps_nf_eval; eauto.
Qed.

Star Steps are functional if the term steps to a term in normal form

Lemma starstep_functional_nf {n: nat} (c c1 c2: comp n):
c >* c1 -> c >* c2 -> nf c1 -> nf c2 -> c1 = c2.
Proof.
intros; eapply bigstep_functional; eapply eval_bigstep; unfold eval; split; eauto.
Qed.

Strong Normaliation is closed under expansion

Lemma normalizing_extension {n: nat} (c c': comp n):
  c >* c' -> SN step c' -> SN step c.
Proof.
  induction 1.
  - now intros.
  - intros H1 % IHstar. constructor. intros x'' H2.
    enough (x' = x'') as -> by assumption.
    eapply step_functional; eassumption.
Qed.

Bigstep Semantics implies termination

Lemma bigstep_sn' {n: nat} (c c': comp n) : c ▷ c' -> SN step c'.
Proof.
  intros H % eval_bigstep; destruct H; now apply Normal_SN, nf_normal.
Qed.

Lemma bigstep_sn {n: nat} (c c': comp n) : c ▷ c' -> SN step c.
Proof.
  intros H; eapply normalizing_extension; [| eapply bigstep_sn'; eassumption].
  enough (eval c c') by firstorder. now apply eval_bigstep.
Qed.