Require Import Coq.Program.Equality.
Require Import Imp.
Require Import Sequences.

In this chapter: various styles of semantics for the Imp language from "Software Foundations", and equivalence results between these semantics.

1. Big-step semantics for termination.

The starting point is the big-step semantics defined in file sf/Imp.v, recalled here for reference.

Inductive ceval : state -> com -> state -> Prop :=
  | E_Skip : forall st,
      SKIP / st ==> st
  | E_Ass  : forall st a1 n l,
      aeval st a1 = n ->
      (l ::= a1) / st ==> (update st l n)
  | E_Seq : forall c1 c2 st st' st'',
      c1 / st  ==> st' ->
      c2 / st' ==> st'' ->
      (c1 ; c2) / st ==> st''
  | E_IfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      c1 / st ==> st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / st ==> st'
  | E_IfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      c2 / st ==> st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / st ==> st'
  | E_WhileEnd : forall b1 st c1,
      beval st b1 = false ->
      (WHILE b1 DO c1 END) / st ==> st
  | E_WhileLoop : forall st st' st'' b1 c1,
      beval st b1 = true ->
      c1 / st ==> st' ->
      (WHILE b1 DO c1 END) / st' ==> st'' ->
      (WHILE b1 DO c1 END) / st ==> st''

  where "c1 '/' st '==>' st'" := (ceval st c1 st').

c / st ==> st' means "executed in initial state st, command c terminates in final state st'".

2. Small-step semantics.

Reserved Notation " c '/' st '-->' c' '/' st' " (at level 40, st at level 39, c' at level 39).

In small-step style, the semantics is presented as a one-step reduction relation c / st --> c' / st' , meaning that the command c, executed in initial state st', performs one elementary step of computation. st' is the updated state after this step. c' is the residual command, capturing all the computations that remain to be done. A small-step semantics for Imp was given in file sf/Imp.v, where not only the execution of commands is broken in individual steps, but also the evaluation of arithmetic and boolean expressions. We depart from this semantics by still treating the evaluation of arithmetic and boolean expressions as one atomic "big-step" (cf. rules CS_Ass, CS_IfTrue and CS_IfFalse below. Non-atomic evaluation of expressions makes a difference in the case of parallel (interleaved) execution of several commands. In a purely sequential setting, it is equivalent (and much simpler) to evaluate expressions in one atomic step, since their evaluations always terminate. In summary, we have:

Three "computational" rules: CS_Ass, CS_IfTrue and CS_IfFalse that actually perform a significant computation.
Two "refocusing" rules: CS_SeqFinish and CS_While that just shift the focus of reduction to the next redex.
One "context" rule: CS_SeqStep that lets us reduce "under" a sequence.

Inductive cstep : (com * state) -> (com * state) -> Prop :=
  | CS_Ass : forall st i a n,
      aeval st a = n ->
      (i ::= a) / st --> SKIP / (update st i n)
  | CS_SeqStep : forall st c1 c1' st' c2,
      c1 / st --> c1' / st' ->
      (c1 ; c2) / st --> (c1' ; c2) / st'
  | CS_SeqFinish : forall st c2,
      (SKIP ; c2) / st --> c2 / st
  | CS_IfTrue : forall st b c1 c2,
      beval st b = true ->
      IFB b THEN c1 ELSE c2 FI / st --> c1 / st
  | CS_IfFalse : forall st b c1 c2,
      beval st b = false ->
      IFB b THEN c1 ELSE c2 FI / st --> c2 / st
  | CS_While : forall st b c1,
      (WHILE b DO c1 END) / st
       --> (IFB b THEN (c1; (WHILE b DO c1 END)) ELSE SKIP FI) / st

  where " c '/' st '-->' c' '/' st' " := (cstep (c,st) (c',st')).

Lemma cstep_deterministic:
  forall cs cs1, cstep cs cs1 -> forall cs2, cstep cs cs2 -> cs1 = cs2.

Proof.

In small-step style, the semantics of a command c in a state st is determined by forming sequences of reductions starting from c, st.

Finite sequences: zero, one or several reductions (reflexive transitive closure)
Infinite sequences: infinitely many reductions.

These sequences are defined using the generic star and infseq operators over binary relations, which are defined in module Sequences, along with useful lemmas.

Notation " c '/' st '-->*' c' '/' st' " := (star cstep (c, st) (c', st'))
(at level 40, st at level 39, c' at level 39).

Notation " c '/' st '-->' '∞' " := (infseq cstep (c, st))
(at level 40, st at level 39).

Definition terminates (c: com) (st: state) (st': state) : Prop :=
  c / st -->* SKIP / st'.

Definition diverges (c: com) (st: state) : Prop :=
  c / st --> ∞.

Definition goes_wrong (c: com) (st: state) : Prop :=
  exists c', exists st',
  c / st --> c' / st' /\ irred cstep (c', st') /\ c' <> SKIP.

Exercise (2 stars)

Show that Imp programs cannot go wrong.

Lemma not_goes_wrong:
forall c st, ~(goes_wrong c st).

Proof.

Sequences of reductions can go under a sequence context, generalizing rule CS_SeqStep.

Lemma star_CS_SeqStep:
  forall c2 st c st' c',
  c / st -->* c' / st' ->
  (c;c2) / st -->* (c';c2) / st'.

Proof.

We now recall the equivalence result between

termination according to the big-step semantics
existence of a finite sequence of reductions to SKIP according to the small-step semantics.

We start with the implication big-step ==> small-step, which is a straightforward induction on the big-step evaluation derivation.

Theorem ceval_to_csteps:
  forall c st st',
  c / st ==> st' ->
  c / st -->* SKIP / st'.

Proof.

The reverse implication, from small-step to big-step, is more subtle. The key lemma is the following, showing that one step of reduction followed by a big-step evaluation to a final state can be collapsed into a single big-step evaluation to that final state.

Lemma cstep_append_ceval:
  forall c1 st1 c2 st2,
  c1 / st1 --> c2 / st2 ->
  forall st3,
  c2 / st2 ==> st3 ->
  c1 / st1 ==> st3.

Proof.

As a consequence, a term that reduces to SKIP evaluates in big-step with the same final state.

Theorem csteps_to_ceval:
  forall st c st',
  c / st -->* SKIP / st' ->
  c / st ==> st'.

Proof.

3. Coinductive big-step semantics for divergence

We now define a predicate c / st ==> ∞ that characterizes diverging evaluations in big-step style, that is, by following the structure of the command c. The only commands that can diverge are:

c1;c2 if either c1 diverges, or c1 terminates and c2 diverges.
IFB b THEN c1 ELSE c2 FI if either b is true and c1 diverges, or b is false and c2 diverges.
WHILE b DO c END if either c diverges at the first iteration or the loop diverges at later iterations.

Reserved Notation " c '/' st '==>' '∞' " (at level 40, st at level 39).

CoInductive cevalinf: com -> state -> Prop :=
  | Einf_Seq_1: forall c1 c2 st,
      c1 / st ==> ∞ ->
      (c1; c2) / st ==> ∞
  | Einf_Seq_2: forall c1 c2 st1 st2,
      c1 / st1 ==> st2 -> c2 / st2 ==> ∞ ->
      (c1; c2) / st1 ==> ∞
  | Einf_IfTrue: forall b c1 c2 st,
      beval st b = true ->
      c1 / st ==> ∞ ->
      (IFB b THEN c1 ELSE c2 FI) / st ==> ∞
  | Einf_IfFalse: forall b c1 c2 st,
      beval st b = false ->
      c2 / st ==> ∞ ->
      (IFB b THEN c1 ELSE c2 FI) / st ==> ∞
  | Einf_WhileBody: forall b c1 st,
      beval st b = true ->
      c1 / st ==> ∞ ->
      (WHILE b DO c1 END) / st ==> ∞
  | Einf_WhileLoop: forall b c1 st st',
      beval st b = true ->
      c1 / st ==> st' -> (WHILE b DO c1 END) / st' ==> ∞ ->
      (WHILE b DO c1 END) / st ==> ∞

where " c '/' st '==>' '∞' " := (cevalinf c st).

The c / st ==> ∞ predicate is declared as coinductive, meaning that we are interested in finite or infinite derivations. If it were declared inductive, only finite derivations would be accepted, and the predicate would always be false, since there are no axioms to start a finite derivation.

To show that c / st ==> ∞ holds for some c and st, we must use proofs by coinduction. A proof by coinduction shows the existence of a derivation by assuming the result (as coinduction hypothesis), then constructing the bottom steps of the derivation, using one or several constructors of the coinductive predicate, then possibly using the coinduction hypothesis as argument to some of those constructors. For example, here is a proof that WHILE BTrue DO SKIP END always diverges.

Remark while_true_skip_diverges:
forall st, (WHILE BTrue DO SKIP END) / st ==> ∞.

Proof.

Of course, we must be careful not to use the coinduction hypothesis immediately, but only as argument to a constructor. Otherwise, Coq will refuse the proof.

Remark while_true_skip_diverges_wrong_proof:
forall st, (WHILE BTrue DO SKIP END) / st ==> ∞.

Proof.

Exercise (1 star)

Show that the program WHILE 1 <= x DO x ::= x + 1 END diverges if started in a state st such that st x >= 1:

Notation vx := (Id 0).

Remark counting_program_diverges:
  forall st,
  st vx >= 1 ->
  WHILE BLe (ANum 1) (AId vx) DO vx ::= APlus (AId vx) (ANum 1) END / st ==> ∞.

Proof.

To make sure that the coinductive big-step notion of divergence is correct, we show that it is equivalent to the existence of infinite reduction sequences. We start with the implication coinductive big-step => infinite reductions. The crucial lemma is that a command that diverges according to the big-step definition can always reduce, and its reduct still diverges.

Lemma cevalinf_can_progress:
forall c st,
c / st ==> ∞ -> exists c', exists st', c / st --> c' / st' /\ c' / st' ==> ∞.

Proof.

By iterating the lemma above "infinitely often", we can build an infinite sequence of reductions. The actual proof is a coinductive argument, of course.

Lemma cevalinf_diverges:
forall c st,
c / st ==> ∞ -> c / st --> ∞.

Proof.

Reverse implication: from infinite reduction sequences to coinductive big-step divergence. We start with a number of inversion lemmas to decompose infinite reduction sequences c / st --> ∞ into sub-sequences according to the shape of the command c considered.

Lemma diverges_skip_impossible:
forall st, ~(SKIP / st --> ∞).

Proof.

Lemma diverges_assign_impossible:
forall v a st, ~((v ::= a) / st --> ∞).

Proof.

Ltac inv H := inversion H; subst; clear H.

The following inversion lemma for sequences uses the fact that a reduction sequence is either infinite or finite, terminating on an irreducible state. This is intuitively obvious, but not provable in core Coq because only constructive proofs are accepted. We need to use classical logic, namely the axiom of excluded middle, to obtain this proof. See file Sequences, theorem infseq_or_finseq.

Lemma diverges_seq_inversion:
  forall st c1 c2,
  (c1;c2) / st --> ∞ ->
  c1 / st --> ∞ \/ (exists st', c1 / st -->* SKIP / st' /\ c2 / st' --> ∞).

Proof.

Lemma diverges_ifthenelse_inversion:
  forall b c1 c2 st,
  (IFB b THEN c1 ELSE c2 FI) / st --> ∞ ->
  (beval st b = true /\ c1 / st --> ∞) \/ (beval st b = false /\ c2 / st --> ∞).

Proof.

Lemma diverges_while_inversion:
  forall b c st,
  (WHILE b DO c END) / st --> ∞ ->
  beval st b = true /\
  (c / st --> ∞ \/ (exists st', c / st -->* SKIP / st' /\ (WHILE b DO c END) / st' --> ∞)).

Proof.

Lemma diverges_to_cevalinf:
forall c st, c / st --> ∞ -> c / st ==> ∞.

Proof.

4. Definitional interpreter

Yet another way to define the semantics of commands is via an interpreter: a function that computes the final state st' for a command c started in initial state st. As explained in the "Software Foundations" course, such a function must be parameterized by an integer i bounding the number of recursive calls of the interpreter. We recall the definition of the ceval_step interpreter given in file Imp of "Software Foundations":

Fixpoint ceval_step (st : state) (c : com) (i : nat) 
                    : option state :=
  match i with 
  | O => None
  | S i' =>
    match c with 
      | SKIP => 
          Some st
      | l ::= a1 => 
          Some (update st l (aeval st a1))
      | c1 ; c2 => 
          bind_option 
            (ceval_step st c1 i')
            (fun st' => ceval_step st' c2 i')
      | IFB b THEN c1 ELSE c2 FI => 
          if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i'
      | WHILE b1 DO c1 END => 
          if (beval st b1)           
          then bind_option 
                 (ceval_step st c1 i')
                 (fun st' => ceval_step st' c i')
          else Some st
    end
  end.

In file Imp, it is shown that the definitional interpreter is equivalent to the big-step semantics for termination, in the following sense:

Theorem ceval_step__ceval: forall c st st',
(exists i, ceval_step st c i = Some st') ->
c / st ==> st'.

Proof.

Theorem ceval__ceval_step: forall c st st',
c / st ==> st' ->
exists i, ceval_step st c i = Some st'.

Proof.

We now show a similar result for the coinductive big-step semantics for divergence.

Remark ceval__ceval_step_either:
forall n c st st', c / st ==> st' -> ceval_step st c n = None \/ ceval_step st c n = Some st'.

Proof.

If c in st diverges according to the big-step rules, then the definitional interpreter returns None no matter how many recursive steps it is allowed to take.

Theorem cevalinf__ceval_step_bottom:
forall n c st, c / st ==> ∞ -> ceval_step st c n = None.

Proof.

For the converse result, we again need a bit of classical logic (the axiom of excluded middle) to show that the sequence n => ceval_step st c n has a limit: it stabilizes to a fixed result when n is big enough.

Require Import Classical.
Require Import Max.

Lemma ceval_step_limit:
forall st c,
exists res, exists m, forall n, m <= n -> ceval_step st c n = res.

Proof.

From this lemma, it follows that a command for which the interpreter always returns None no matter how big the step limit is does diverge according to the big-step semantics.

Theorem ceval_step_bottom__cevalinf:
  forall c st m,
  (forall n, m <= n -> ceval_step st c n = None) ->
  c / st ==> ∞.

Proof.

5. From a definitional interpreter to a denotational semantics

Using yet another bit of logic (an axiom of description -- a variant of the axiom of choice), we can show the existence of a function denot st c which is the limit of the sequence n => ceval_step st c n as n goes to infinity. The result of this function is to be interpreted as the denotation of command c in state st:

denot st c = None (or "bottom") means that c diverges
denot st c = Some st' means that c terminates with final state st'.

Require Import ClassicalDescription.

Definition interp_limit_dep (st: state) (c: com) :
{ res: option state | exists m, forall n, m <= n -> ceval_step st c n = res}.

Proof.

Definition denot (st: state) (c: com) : option state :=
  proj1_sig (interp_limit_dep st c).

Lemma denot_limit:
  forall st c,
  exists m, forall n, m <= n -> ceval_step st c n = denot st c.

Proof.

Lemma denot_charact:
  forall st c m res,
  (forall n, m <= n -> ceval_step st c n = res) ->
  denot st c = res.

Proof.

Lemma denot_terminates:
forall st c n st', ceval_step st c n = Some st' -> denot st c = Some st'.

Proof.

We can then show that this denot function satisfies the equations of denotational semantics for the Imp language.

Lemma denot_skip:
forall st, denot st SKIP = Some st.

Proof.

Lemma denot_assign:
forall v a st, denot st (v ::= a) = Some (update st v (aeval st a)).

Proof.

Lemma denot_seq:
forall c1 c2 st,
denot st (c1;c2) = bind_option (denot st c1) (fun st' => denot st' c2).

Proof.

Lemma denot_ifthenelse:
  forall b c1 c2 st,
  denot st (IFB b THEN c1 ELSE c2 FI) =
  if beval st b then denot st c1 else denot st c2.

Proof.

Lemma denot_while:
  forall b c st,
  denot st (WHILE b DO c END) =
  if beval st b
  then bind_option (denot st c) (fun st' => denot st' (WHILE b DO c END))
  else Some st.

Proof.

Moreover, denot st (WHILE b DO c END) is the least fixpoint of the equation above.

Definition result_less_defined (r1 r2: option state) : Prop :=
  r1 = None \/ r1 = r2.

Lemma denot_while_least_fixpoint:
  forall b c (f: state -> option state),
  (forall st,
   f st = if beval st b then bind_option (denot st c) f else Some st) ->
  (forall st,
   result_less_defined (denot st (WHILE b DO c END)) (f st)).

Proof.

Exercise (2 stars).

Show that the denotational semantics for loops is compositional:

Lemma denot_while_compositional:
  forall b c1 c2,
  (forall st, denot st c1 = denot st c2) ->
  (forall st, denot st (WHILE b DO c1 END) = denot st (WHILE b DO c2 END)).

Proof.

Composing the various results so far, we obtain the following equivalences between the denotational semantics and the big-step semantics.

Lemma denot_ceval:
forall c st st',
c / st ==> st' <-> denot st c = Some st'.

Proof.

Lemma denot_cevalinf:
forall c st,
c / st ==> ∞ <-> denot st c = None.

Proof.

Module Semantics

1. Big-step semantics for termination.

2. Small-step semantics.

Exercise (2 stars)

3. Coinductive big-step semantics for divergence

Exercise (1 star)

4. Definitional interpreter

5. From a definitional interpreter to a denotational semantics

Exercise (2 stars).