POPL Tutorial/Big step, small step

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

In this exercise, we explore the relationship between big-step evaluation and small-step transition semantics for the MinML language we worked with before. The theroem we want to establish is that an expression e evaluates to a value v in many little steps if and only if it evaluates to v in one big step.

There are five tasks:

  • Complete a compatibility lemma that if , then
  • Prove the backward direction (big-step evaluation implies small-step evaluation)
  • Prove three cases of the expansion lemma.
  • Prove the forward direction (small-step evaluation implies big-step evaluation) for a "convienent" definition of multi-step.
  • Prove the forward direction for the original definition of multi-step.

The solution is here.



tp : type.				%name tp T.
nat : tp.
arr : tp -> tp -> tp.


exp : type.				%name exp E.
fn : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
z : exp.
s : exp -> exp.
ifz : exp -> exp -> (exp -> exp) -> exp.

Small-step dynamic semantics

value : exp -> type.			%name value Dval.
%mode value +E.

value/z : value z.
value/s : value (s E) 
	   <- value E.
value/fn : value (fn _ _).

step : exp -> exp -> type.		%name step Dstep.
%mode step +E1 -E2.

step/app/fn : step (app E1 E2) (app E1' E2)
	       <- step E1 E1'.
step/app/arg : step (app E1 E2) (app E1 E2')
		<- value E1 <- step E2 E2'.
step/app/beta : step (app (fn _ ([x] E x)) E2) (E E2)
		 <- value E2.
step/s : step (s E) (s E') 
	  <- step E E'.
step/ifz/arg : step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))
		<- step E E'.
step/ifz/z : step (ifz z E1 ([x] E2 x)) E1.
step/ifz/s : step (ifz (s E) E1 ([x] E2 x)) (E2 E)
	      <- value E.


step* : exp -> exp -> type.             %name step* Dstep*.

step*/step : step* E E'
              <- step E E'.
step*/refl : step* E E.
step*/trans : step* E E''
               <- step* E' E''
               <- step* E E'.

We can define D1 @ D2 to be an abbreviation for step*/trans D1 D2. This is convenient for chaining together several derivations using transitivity.

%abbrev @ : step* E E' -> step* E' E'' -> step* E E''
          = [d1] [d2] step*/trans d1 d2.

%infix right 10 @.

Big-step dynamic semantics

eval : exp -> exp -> type.              %name eval Deval.

eval/z : eval z z.
eval/s : eval (s E) (s V)
          <- eval E V.
eval/ifz/z : eval (ifz E E0 ([x] E1 x)) V0
              <- eval E z
              <- eval E0 V0.
eval/ifz/s : eval (ifz E E0 ([x] E1 x)) V1
              <- eval E (s V)
              <- eval (E1 V) V1.
eval/fn : eval (fn T1 ([x] E x)) (fn T1 ([x] E x)).

eval/app : eval (app E1 E2) V
            <- eval E1 (fn T1 ([x] E x))
            <- eval E2 V2
            <- eval (E V2) V.


There are two easy lemmas we'll need later that relate evaluation to the value judgement from above.

Evaluation returns a value

eval-val : eval E V -> value V -> type.
%mode eval-val +D1 -D2.

- : eval-val eval/z value/z.
- : eval-val (eval/s D) (value/s Dval)
     <- eval-val D Dval.
- : eval-val (eval/ifz/z (D0 : eval E0 V0)
                         (Dz : eval E z))
     <- eval-val D0 (Dval0 : value V0).
- : eval-val (eval/ifz/s (D1 : eval (E1 V) V1)
                         (Ds : eval E (s V))
                : eval (ifz E E0 [x] E1 x) V1)
     <- eval-val D1 (Dval1 : value V1).
- : eval-val eval/fn value/fn.
- : eval-val (eval/app (Dsub : eval (E V2) V)
                       (D2 : eval E2 V2)
                       (D1 : eval E1 (fn T1 ([x] E x))))
     <- eval-val Dsub (DvalV : value V).

%worlds () (eval-val _ _).
%total D (eval-val D _).

Values evaluate to themselves

val-eval : value V -> eval V V -> type.
%mode val-eval +Dval -Dev.

- : val-eval value/z eval/z.
- : val-eval (value/s Dval) (eval/s Dev)
     <- val-eval Dval Dev.
- : val-eval value/fn eval/fn.

%worlds () (val-eval _ _).
%total D (val-eval D _).

Big-step implies multi-step

Our first main theorem is to show that big-step evaluation implies multi-step evaluation, i.e. that if eval E V then step* E V.

Compatibility lemmas

To prove this, we'll need some compatibility lemmas for multi-step transition which say that multi-step transitions in a sub-term of a term can be bubbled up to the term itself.

Each argument proceeds by induction on the derivation that step* E E'.

step*/s : step* E E' -> step* (s E) (s E') -> type.
%mode step*/s +D* -D*s.

- : step*/s (step*/step (D : step E E')) (step*/step (step/s D)).
- : step*/s (step*/refl : step* E E) (step*/refl : step* (s E) (s E)).
- : step*/s (step*/trans (D* : step* E E') (D*' : step* E' E''))
            (step*/trans D*s D*'s)
     <- step*/s D* (D*s : step* (s E) (s E'))
     <- step*/s D*' (D*'s : step* (s E') (s E'')).

%worlds () (step*/s _ _).
%total D (step*/s D _).

step*/ifz/arg : step* E E' -> step* (ifz E E0 [x] E1 x) (ifz E' E0 [x] E1 x)
                 -> type.
%mode +{E:exp} +{E':exp} +{E0:exp} +{E1:exp -> exp} +{D:step* E E'}
   -{Difz:step* (ifz E E0 ([x:exp] E1 x)) (ifz E' E0 ([x:exp] E1 x))}
   (step*/ifz/arg D Difz).

- : step*/ifz/arg (step*/step (D : step E E')) (step*/step (step/ifz/arg D)).
- : step*/ifz/arg step*/refl step*/refl.
- : step*/ifz/arg (step*/trans D* D*') (step*/trans D*ifz D*'ifz)
     <- step*/ifz/arg D* D*ifz
     <- step*/ifz/arg D*' D*'ifz.

%worlds () (step*/ifz/arg _ _).
%total D (step*/ifz/arg D _).

step*/app/fn : step* E1 E1' -> step* (app E1 E2) (app E1' E2) -> type.
%mode +{E1:exp} +{E1':exp} +{E2:exp} +{D1:step* E1 E1'}
    -{Dapp:step* (app E1 E2) (app E1' E2)}
    (step*/app/fn D1 Dapp).

- : step*/app/fn (step*/step (D1 : step E1 E1'))
                  (step*/step (step/app/fn D1)).
- : step*/app/fn step*/refl step*/refl.
- : step*/app/fn (step*/trans D* D*') (step*/trans D*app D*'app)
     <- step*/app/fn D* D*app
     <- step*/app/fn D*' D*'app.

%worlds () (step*/app/fn _ _).
%total D (step*/app/fn D _).

TASK 1: Fill in the cases of the unfinished compatibility proof

step*/app/arg : step* E2 E2' -> value V1 -> step* (app V1 E2) (app V1 E2')
                 -> type.
%mode step*/app/arg +D2 +DvalV1 -Dapp.

%%% fill in here.

%worlds () (step*/app/arg _ _ _).
%total D (step*/app/arg D _ _).

Main theorem

Now we can prove our first main theorem by induction on the derivation of eval E V using the multi-step compatibility lemmas above.

TASK 2: Fill in the missing cases of the theorem

eval-multi : eval E V -> step* E V -> type.
%mode eval-multi +D -D*.

- : eval-multi (eval/z : eval z z) step*/refl.

- : eval-multi (eval/s D : eval (s E) (s V)) D*s
     <- eval-multi D (D* : step* E V)
     <- step*/s D* (D*s : step* (s E) (s V)).

- : eval-multi (eval/ifz/z (D0 : eval E0 V0) (Dz : eval E z))
        (Difz* @ step*/step step/ifz/z @ D0*)
     <- eval-multi Dz (Dz* : step* E z)
     <- eval-multi D0 (D0* : step* E0 V0)
     <- step*/ifz/arg Dz* (Difz* : step* (ifz E E0 [x] E1 x)
                                         (ifz z E0 [x] E1 x)).

- : eval-multi (eval/ifz/s (D1 : eval (E1 V) V1) (Ds : eval E (s V)))
        (Difz* @ step*/step (step/ifz/s DvalV) @ D1*)
     <- eval-multi Ds (Ds* : step* E (s V))
     <- eval-multi D1 (D1* : step* (E1 V) V1)
     <- step*/ifz/arg Ds* (Difz* : step* (ifz E E0 [x] E1 x)
                                         (ifz (s V) E0 [x] E1 x))
     <- eval-val Ds (value/s (DvalV : value V)).

- : eval-multi 
     XXX. %%% fill in here.

- : eval-multi 
     (eval/app (Dsub : eval (E (fn T1 T2 [f] [x] E f x) V2) V)
        (D2 : eval E2 V2)
        (D1 : eval E1 (fn T1 T2 [f] [x] E f x)))
     XXX. %%% fill in here.

%worlds () (eval-multi _ _). 
%total D (eval-multi D _).

Multi-step implies big step

Left-linearized multi-step

For the reverse direction, it turns out we'd rather have the inductive definition of the multi-step relation be a little bit different. We call the more convienent direction "left-linearlized multi-step" and prove it equivlaent to the previous definition of multi-step.

step** : exp -> exp -> type.            %name step** Dstep**.

step**/refl : step** E E.
step**/cons : step** E E''
               <- step** E' E''
               <- step E E'.

Lemma: Multi-step implies linearized multi-step. This is tantamount to showing that transitivity is admissible for linearized derivations.

step**/trans : step** E E' -> step** E' E'' -> step** E E'' -> type.
%mode step**/trans +D1 +D2 -D3.

- : step**/trans step**/refl (Dstep** : step** E E'') Dstep**.
- : step**/trans (step**/cons (Dstep1 : step E E1)
                              (Dstep**1 : step** E1 E'))
                 (Dstep**2 : step** E' E'')
        (step**/cons Dstep1 Dstep**)
     <- step**/trans Dstep**1 Dstep**2 (Dstep** : step** E1 E'').

%worlds () (step**/trans _ _ _).
%total D (step**/trans D _ _).

Lemma: Multi-step implies linearized multi-step. This is tantamount to showing that transitivity is admissible for linearized derivations.

multi-step** : step* E E' -> step** E E' -> type.
%mode multi-step** +D* -D**.

- : multi-step** (step*/step Dstep) (step**/cons Dstep step**/refl).
- : multi-step** step*/refl step**/refl.
- : multi-step** (step*/trans (D1 : step* E E') (D2 : step* E' E'')) D**
     <- multi-step** D1 (D1** : step** E E')
     <- multi-step** D2 (D2** : step** E' E'')
     <- step**/trans D1** D2** (D** : step** E E'').

%worlds () (multi-step** _ _).
%total D (multi-step** D _).

Expansion lemma

The main lemma is that evaluation is closed under single-step expansion. This is a key lemma in the proof that evaluation in the small-step semantics implies evaluation in the big-step evaluation.

We proceed by induction on the second derivation, the derivation that step E E'.

TASK 3: Prove the three missing cases of the expansion lemma

expansion : eval E' V -> step E E' -> eval E V -> type.
%mode expansion +D1 +D2 -D3.

Case step/s:

- : expansion (eval/s (Deval' : eval E' V) : eval (s E') (s V))
              (step/s (Dstep  : step E E') : step (s E) (s E'))
              (eval/s (Deval  : eval E V)  : eval (s E) (s V))
     <- expansion Deval' Dstep (Deval : eval E V).

Case step/ifz/arg:

%% By inversion, either eval E' V by eval/ifz/z or by eval/ifz/s.
- : expansion (eval/ifz/z (D0 : eval E0 V0) (Dz' : eval E' z)
                  : eval (ifz E' E0 [x] E1 x) V0)
              (step/ifz/arg (Dstep : step E E')
                  : step (ifz E E0 [x] E1 x) (ifz E' E0 [x] E1 x))
              (eval/ifz/z D0 Dz
                  : eval (ifz E E0 [x] E1 x) V0)
     <- expansion Dz' Dstep (Dz : eval E z).

- : expansion 
     XXX %%% fill in here.
     (step/ifz/arg (Dstep : step E E')
        : step (ifz E E0 [x] E1 x) (ifz E' E0 [x] E1 x))
     YYY. %%% fill in here.

Case step/ifz/z:

- : expansion (Deval' : eval E0 V0)
              (step/ifz/z : step (ifz z E0 [x] E1 x) E0)
              (eval/ifz/z Deval' eval/z).

Case step/ifz/s:

- : expansion (Deval' : eval (E1 V) V1)
              (step/ifz/s (Dval : value V)
                  : step (ifz (s V) E0 ([x] E1 x)) (E1 V))
              (eval/ifz/s Deval' (eval/s DevalV))
     <- val-eval Dval (DevalV : eval V V).

Case step/app/fn:

- : expansion (eval/app (Dsub : eval (E V2) V)
                        (D2 : eval E2 V2)
                        (D1' : eval E1' (fn T1 ([x] E x)))
                  : eval (app E1' E2) V)
              (step/app/fn (Dstep1 : step E1 E1')
                  : step (app E1 E2) (app E1' E2))
              (eval/app Dsub D2 D1)
     <- expansion D1' Dstep1 (D1 : eval E1 (fn T1 ([x] E x))).

Case step/app/arg:

- : expansion 
     XXX %%% fill in here.
     (step/app/arg (Dstep2 : step E2 E2') (Dval1 : value V1)
        : step (app V1 E2) (app V1 E2'))
     YYY. %%% fill in here.

Case step/app/beta-v:

- : expansion 
     XXX %%% fill in here.
     (step/app/beta-v (Dval2 : value V2)
        : step (app (fn T1 T2 [f] [x] E f x) V2)
           (E (fn T1 T2 [f] [x] E f x) V2))
     YYY. %%% fill in here.

%worlds () (expansion _ _ _).
%total D (expansion _ D _).

Main theorem

Now we will use our "more convienent" left-linearized multi-step definition and induct over it in order to prove the forward direction of our primary theorem, that small step evaluation implies big step evaluation.

The proof is by induction on the derivation that step** E V, using closure under single-step expansion. There are only two cases due to the simple definition of step**.

TASK 4: Prove main theorem in the forward direction

multi**-eval : step** E V -> value V -> eval E V -> type.
%mode multi**-eval +D1 +D2 -D3.

%%% fill in here.

%worlds () (multi**-eval _ _ _).
%total D (multi**-eval D _ _).


Using one of the theorems we proved about left-linearized multi-step, we can easly show the final result; our proof needs to have only one case and does not use induction.

TASK 5: Complete proof by composing previous lemmas

multi-eval : step* E V -> value V -> eval E V -> type.
%mode multi-eval +D1 +D2 -D3.

%%% fill in here.

%worlds () (multi-eval _ _ _).
%total {} (multi-eval _ _ _).