Module Semantics

Mechanization of operational semantics.

Require Import String.
Require Import List.
Require Import Sequences.

Open Scope string_scope.
Open Scope list_scope.

Abstract syntax of the language


Definition var: Type := string.

Definition var_eq: forall (v1 v2: var), {v1=v2} + {v1<>v2} := string_dec.

Definition const: Type := nat.

Inductive term: Type :=
  | Var: var -> term (* variable *)
  | Const: const -> term (* constant *)
  | Fun: var -> term -> term (* function abstraction *)
  | App: term -> term -> term. (* function application *)

subst x b a replaces x by b in a. Warning: not capture-avoiding! b must be closed.

Fixpoint subst (x: var) (b: term) (a: term) {struct a}: term :=
  match a with
  | Var y => if var_eq x y then b else Var y
  | Const n => Const n
  | Fun y a1 => Fun y (if var_eq x y then a1 else subst x b a1)
  | App a1 a2 => App (subst x b a1) (subst x b a2)
  end.

Values are either constants or functions.

Inductive isvalue: term -> Prop :=
  | isvalue_const: forall c,
      isvalue (Const c)
  | isvalue_fun: forall x a,
      isvalue (Fun x a).

Hint Constructors isvalue: sem.

Operational semantics


Reduction semantics (small-step)


One step of reduction, in SOS style.

Inductive red: term -> term -> Prop :=
  | red_beta: forall x a v, (* beta-v reduction at top of term *)
      isvalue v ->
      red (App (Fun x a) v) (subst x v a)
  | red_app_l: forall a1 a2 b, (* reduction to the left of an application *)
      red a1 a2 ->
      red (App a1 b) (App a2 b)
  | red_app_r: forall v b1 b2, (* reduction to the right of an application *)
      isvalue v ->
      red b1 b2 ->
      red (App v b1) (App v b2).

Hint Constructors red: sem.

Values do not reduce.

Lemma value_irred:
  forall a, isvalue a -> irred red a.
Proof.
  destruct 1; unfold irred; intros; red; intros; inversion H.
Qed.

Determinism of one-step reduction.

Lemma red_deterministic:
  forall a b c, red a b -> red a c -> b = c.
Proof.
  intros a b c R. revert a b R c.
  induction 1; intros c R'; inversion R'; subst.
  auto.
  inversion H3.
  elim (value_irred v H b2 H4).
  inversion R.
  f_equal; auto.
  elim (value_irred a1 H1 a2 R).
  elim (value_irred b1 H3 b2 R).
  elim (value_irred v H a2 H3).
  f_equal; auto.
Qed.

The three possible outcomes of an execution.

Definition terminates (a: term) (v: term) : Prop :=
  star red a v /\ isvalue v.

Definition diverges (a: term) : Prop :=
  infseq red a.

Definition goes_wrong (a: term) : Prop :=
  exists b, star red a b /\ irred red b /\ ~isvalue b.

Natural semantics (big-step)


For termination.

Inductive eval: term -> term -> Prop :=
  | eval_const: forall c,
      eval (Const c) (Const c)
  | eval_fun: forall x a,
      eval (Fun x a) (Fun x a)
  | eval_app: forall a b x c vb v,
      eval a (Fun x c) ->
      eval b vb ->
      eval (subst x vb c) v ->
      eval (App a b) v.

Lemma eval_isvalue:
  forall a b, eval a b -> isvalue b.
Proof.
  induction 1; auto with sem.
Qed.

For divergence.

CoInductive evalinf: term -> Prop :=
  | evalinf_app_l: forall a b,
      evalinf a ->
      evalinf (App a b)
  | evalinf_app_r: forall a b va,
      eval a va ->
      evalinf b ->
      evalinf (App a b)
  | evalinf_app_f: forall a b x c vb,
      eval a (Fun x c) ->
      eval b vb ->
      evalinf (subst x vb c) ->
      evalinf (App a b).

An example of a term that diverges.

Definition delta := Fun "x" (App (Var "x") (Var "x")).
Definition omega := App delta delta.

Lemma evalinf_omega: evalinf omega.
Proof.
  cofix COINDHYP. unfold omega. eapply evalinf_app_f.
  unfold delta. apply eval_fun.
  unfold delta. apply eval_fun.
  simpl. fold delta. fold omega. apply COINDHYP.
Qed.

Hint Constructors eval evalinf: sem.
Hint Resolve eval_isvalue: sem.

Equivalence small-step / big-step


Context lemmas for reduction sequences.

Lemma star_red_app_l:
  forall a1 a2 b,
  star red a1 a2 -> star red (App a1 b) (App a2 b).
Proof.
  induction 1; intros; eauto with sem sequences.
Qed.

Lemma star_red_app_r:
  forall v a1 a2,
  isvalue v -> star red a1 a2 -> star red (App v a1) (App v a2).
Proof.
  induction 2; intros; eauto with sem sequences.
Qed.

If a evaluates to v, there exists a finite reduction sequence from a to v.

Lemma eval_star_red:
  forall a v, eval a v -> star red a v.
Proof.
  induction 1.
- constructor.
- constructor.
- eapply star_trans. apply star_red_app_l; eauto.
  eapply star_trans. apply star_red_app_r; eauto. constructor.
  eapply star_step. apply red_beta. eapply eval_isvalue; eauto.
  assumption.
Qed.

If a reduces to v in zero, one or several steps, then a evaluates to v.

Lemma eval_value:
  forall v, isvalue v -> eval v v.
Proof.
  induction 1; intros; constructor.
Qed.

Hint Resolve eval_value: sem.

Lemma red_eval:
  forall a b, red a b -> forall v, eval b v -> eval a v.
Proof.
  induction 1; intros.
- eauto with sem.
- inversion H0. eauto with sem.
- inversion H1. eauto with sem.
Qed.

Lemma star_red_eval:
  forall a v, star red a v -> isvalue v -> eval a v.
Proof.
  induction 1; intros.
  apply eval_value. assumption.
  eapply red_eval; eauto.
Qed.

Hint Resolve star_red_eval: sem.

Corollary: equivalence between eval and small-step termination.

Theorem eval_terminates:
  forall a v, terminates a v <-> eval a v.
Proof.
  intros; split; intros.
  destruct H. apply star_red_eval; auto.
  split. apply eval_star_red; auto. eapply eval_isvalue; eauto.
Qed.

If a diverges according to evalinf, it can make one step of reduction to a term that still diverges according to evalinf.

Lemma evalinf_red:
  forall a, evalinf a -> exists b, red a b /\ evalinf b.
Proof.
  induction a; intros; inversion H; subst.
- (* function part evaluates infinitely *)
  destruct (IHa1 H1) as [a1' [R E]].
  exists (App a1' a2); eauto with sem.
- (* function part evaluates finitely, argument evaluates infinitely *)
  destruct (IHa2 H3) as [a2' [R E]].
  assert (S: star red a1 va) by (apply eval_star_red; auto).
  inversion S; subst.
  + (* function part was already a value *)
    exists (App va a2'); eauto with sem.
  + (* function part evaluates *)
    exists (App b a2); eauto 6 with sem.
- (* function and argument parts evaluate finitely, beta-redex evaluates infinitely *)
  assert (S1: star red a1 (Fun x c)) by (apply eval_star_red; auto).
  assert (S2: star red a2 vb) by (apply eval_star_red; auto).
  inversion S1; subst; [inversion S2; subst|idtac].
  + (* function part and argument part were already values *)
    exists (subst x vb c); eauto with sem.
  + (* function part was already a value, argument part reduces *)
    exists (App (Fun x c) b); eauto 6 with sem.
  + (* function part reduces *)
    exists (App b a2); eauto with sem.
Qed.

As a consequence, if a diverges according to evalinf, there exists an infinite sequence of reductions starting with a.

Lemma evalinf_infseq_red:
  forall a, evalinf a -> infseq red a.
Proof.
  cofix COINDHYP. intros.
  destruct (evalinf_red _ H) as [b [R E]].
  apply infseq_step with b. auto. apply COINDHYP. auto.
Qed.

Conversely, if there exists an infinite sequence of reductions starting with a, then a diverges according to evalinf.

Lemma infseq_red_evalinf:
  forall a, infseq red a -> evalinf a.
Proof.
  cofix COINDHYP.
  intros.
  destruct a; try (inversion H; inversion H0; fail).
  elim (infseq_or_finseq red a1).
- (* a1 evaluates infinitely *)
  intro REDINF1. apply evalinf_app_l. apply COINDHYP. assumption.
- (* a1 evaluates finitely *)
  intros [n1 [REDM1 NOTRED1]].
  assert (REDINF1: infseq red (App n1 a2)).
    eapply infseq_star_inv; eauto. exact red_deterministic. apply star_red_app_l; auto.
  assert (ISVAL1: isvalue n1).
    inversion REDINF1. inversion H0.
    constructor.
    elim (NOTRED1 _ H6).
    assumption.
  elim (infseq_or_finseq red a2).
+ (* a2 evaluates infinitely *)
  intro REDINF2. apply evalinf_app_r with n1.
    apply star_red_eval; assumption.
    apply COINDHYP. assumption.
+ (* a2 evaluates finitely as well *)
  intros [n2 [REDM2 NOTRED2]].
  assert (REDINF2: infseq red (App n1 n2)).
    eapply infseq_star_inv; eauto. exact red_deterministic. apply star_red_app_r; auto.
  assert (NEXTRED: exists x, exists c,
            n1 = Fun x c /\ isvalue n2 /\ infseq red (subst x n2 c)).
    inversion REDINF2. inversion H0.
    subst b. exists x; exists a0. tauto.
    elim (NOTRED1 _ H6).
    elim (NOTRED2 _ H7).
  destruct NEXTRED as [x [c [A [B C]]]]. subst n1.
  apply evalinf_app_f with x c n2.
    apply star_red_eval; assumption.
    apply star_red_eval; assumption.
    apply COINDHYP. assumption.
Qed.

Corollary: equivalence between evalinf and small-step divergence.

Theorem evalinf_diverges:
  forall a, diverges a <-> evalinf a.
Proof.
  intros; split; intros. apply infseq_red_evalinf; auto. apply evalinf_infseq_red; auto.
Qed.