POPL Tutorial/Big step, small step
From The Twelf Project
| 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.
Contents |
Syntax
Types:
tp : type. %name tp T. nat : tp. arr : tp -> tp -> tp.
Expressions
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.
Multi-step
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.
Lemmas
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)) Dval0 <- 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) Dval1 <- 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)))) DvalV <- 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 eval/fn 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 _ _).
Corollary
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 _ _ _).
