POPL Tutorial/Big step, small step

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 $e \mapsto^* e'$, then $v~e \mapsto^* v~e'$
• 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.

Syntax

Types:

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.

Expressions

%sort exp %.
%name exp %.
%term fn %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%term z exp %.
%term s %pi exp %-> exp %.
%term ifz %pi exp %-> exp %-> (%pi exp %-> exp) %-> exp %.

Small-step dynamic semantics

%sort value {_ exp} %.
%name value %.
%mode value %in %.
%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.
%term value/fn value (fn _ _) %.
%sort step {_ exp} {_ exp} %.
%name step %.
%mode step %in %out %.
%term step/app/fn %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step/app/beta %pi (step (app (fn _ ([x] E x)) E2) (E E2)) %<- (value E2) %.
%term step/s %pi (step (s E) (s E')) %<- (step E E') %.
%term step/ifz/arg %pi (step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))) %<- (step E E') %.
%term step/ifz/z step (ifz z E1 ([x] E2 x)) E1 %.
%term step/ifz/s %pi (step (ifz (s E) E1 ([x] E2 x)) (E2 E)) %<- (value E) %.

Multi-step

%sort step* {_ exp} {_ exp} %.
%name step* %.
%term step*/step %pi (step* E E') %<- (step E E') %.
%term step*/refl step* E E %.
%term step*/trans %pi (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.

%inline @ (%pi (step* E E') %-> (step* E' E'') %-> (step* E E'')) [d1] [d2] step*/trans d1 d2 %.
%prec %right 10 @ %.

Big-step dynamic semantics

%sort eval {_ exp} {_ exp} %.
%name eval %.
%term eval/z eval z z %.
%term eval/s %pi (eval (s E) (s V)) %<- (eval E V) %.
%term eval/ifz/z %pi (eval (ifz E E0 ([x] E1 x)) V0) %<- (eval E z) %<- (eval E0 V0) %.
%term eval/ifz/s %pi (eval (ifz E E0 ([x] E1 x)) V1) %<- (eval E (s V)) %<- (eval (E1 V) V1) %.
%term eval/fn eval (fn T1 ([x] E x)) (fn T1 ([x] E x)) %.
%term eval/app
  %pi (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

%sort eval-val {_ eval E V} {_ value V} %.
%mode eval-val %in %out %.
%term _ eval-val eval/z value/z %.
%term _ %pi (eval-val (eval/s D) (value/s Dval)) %<- (eval-val D Dval) %.
%term _
  %pi (eval-val (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E z) Dz)) Dval0)
  %<- (eval-val D0 (%the (value V0) Dval0)) %.
%term _
  %pi (eval-val (%the (eval (ifz E E0 ([x] E1 x)) V1) (eval/ifz/s (%the (eval (E1 V) V1) D1) (%the (eval E (s V)) Ds))) Dval1)
  %<- (eval-val D1 (%the (value V1) Dval1)) %.
%term _ eval-val eval/fn value/fn %.
%term _
  %pi (eval-val (eval/app (%the (eval (E V2) V) Dsub) (%the (eval E2 V2) D2) (%the (eval E1 (fn T1 ([x] E x))) D1)) DvalV)
  %<- (eval-val Dsub (%the (value V) DvalV)) %.
%worlds () (eval-val _ _) %.
%total D (eval-val D _) %.

Values evaluate to themselves

%sort val-eval {_ value V} {_ eval V V} %.
%mode val-eval %in %out %.
%term _ val-eval value/z eval/z %.
%term _ %pi (val-eval (value/s Dval) (eval/s Dev)) %<- (val-eval Dval Dev) %.
%term _ 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'.

%sort step*/s {_ step* E E'} {_ step* (s E) (s E')} %.
%mode step*/s %in %out %.
%term _ step*/s (step*/step (%the (step E E') D)) (step*/step (step/s D)) %.
%term _ step*/s (%the (step* E E) step*/refl) (%the (step* (s E) (s E)) step*/refl) %.
%term _
  %pi (step*/s (step*/trans (%the (step* E E') D*) (%the (step* E' E'') D*')) (step*/trans D*s D*'s))
  %<- (step*/s D* (%the (step* (s E) (s E')) D*s))
  %<- (step*/s D*' (%the (step* (s E') (s E'')) D*'s)) %.
%worlds () (step*/s _ _) %.
%total D (step*/s D _) %.
%sort step*/ifz/arg {_ step* E E'} {_ step* (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))} %.
%mode {%in E exp} {%in E' exp} {%in E0 exp} {%in E1 %pi exp %-> exp} {%in D step* E E'} {%out Difz step* (ifz E E0 ([x exp] E1 x)) (ifz E' E0 ([x exp] E1 x))} step*/ifz/arg D Difz %.
%term _ step*/ifz/arg (step*/step (%the (step E E') D)) (step*/step (step/ifz/arg D)) %.
%term _ step*/ifz/arg step*/refl step*/refl %.
%term _
  %pi (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 _) %.
%sort step*/app/fn {_ step* E1 E1'} {_ step* (app E1 E2) (app E1' E2)} %.
%mode {%in E1 exp} {%in E1' exp} {%in E2 exp} {%in D1 step* E1 E1'} {%out Dapp step* (app E1 E2) (app E1' E2)} step*/app/fn D1 Dapp %.
%term _ step*/app/fn (step*/step (%the (step E1 E1') D1)) (step*/step (step/app/fn D1)) %.
%term _ step*/app/fn step*/refl step*/refl %.
%term _
  %pi (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

%sort step*/app/arg {_ step* E2 E2'} {_ value V1} {_ step* (app V1 E2) (app V1 E2')} %.
%mode step*/app/arg %in %in %out %.
%%% 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

%sort eval-multi {_ eval E V} {_ step* E V} %.
%mode eval-multi %in %out %.
%term _ eval-multi (%the (eval z z) eval/z) step*/refl %.
%term _
  %pi (eval-multi (%the (eval (s E) (s V)) (eval/s D)) D*s)
  %<- (eval-multi D (%the (step* E V) D*))
  %<- (step*/s D* (%the (step* (s E) (s V)) D*s)) %.
%term _
  %pi (eval-multi (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E z) Dz)) (Difz* @ step*/step step/ifz/z @ D0*))
  %<- (eval-multi Dz (%the (step* E z) Dz*))
  %<- (eval-multi D0 (%the (step* E0 V0) D0*))
  %<- (step*/ifz/arg Dz* (%the (step* (ifz E E0 ([x] E1 x)) (ifz z E0 ([x] E1 x))) Difz*)) %.
%term _
  %pi (eval-multi (eval/ifz/s (%the (eval (E1 V) V1) D1) (%the (eval E (s V)) Ds)) (Difz* @ step*/step (step/ifz/s DvalV) @ D1*))
  %<- (eval-multi Ds (%the (step* E (s V)) Ds*))
  %<- (eval-multi D1 (%the (step* (E1 V) V1) D1*))
  %<- (step*/ifz/arg Ds* (%the (step* (ifz E E0 ([x] E1 x)) (ifz (s V) E0 ([x] E1 x))) Difz*))
  %<- (eval-val Ds (value/s (%the (value V) DvalV))) %.
%term _ eval-multi eval/fn XXX %.
%%% fill in here.
%term _ eval-multi (eval/app (%the (eval (E (fn T1 T2 ([f] [x] E f x)) V2) V) Dsub) (%the (eval E2 V2) D2) (%the (eval E1 (fn T1 T2 ([f] [x] E f x))) D1)) 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.

%sort step** {_ exp} {_ exp} %.
%name step** %.
%term step**/refl step** E E %.
%term step**/cons %pi (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.

%sort step**/trans {_ step** E E'} {_ step** E' E''} {_ step** E E''} %.
%mode step**/trans %in %in %out %.
%term _ step**/trans step**/refl (%the (step** E E'') Dstep**) Dstep** %.
%term _
  %pi (step**/trans (step**/cons (%the (step E E1) Dstep1) (%the (step** E1 E') Dstep**1)) (%the (step** E' E'') Dstep**2) (step**/cons Dstep1 Dstep**))
  %<- (step**/trans Dstep**1 Dstep**2 (%the (step** E1 E'') Dstep**)) %.
%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.

%sort multi-step** {_ step* E E'} {_ step** E E'} %.
%mode multi-step** %in %out %.
%term _ multi-step** (step*/step Dstep) (step**/cons Dstep step**/refl) %.
%term _ multi-step** step*/refl step**/refl %.
%term _
  %pi (multi-step** (step*/trans (%the (step* E E') D1) (%the (step* E' E'') D2)) D**)
  %<- (multi-step** D1 (%the (step** E E') D1**))
  %<- (multi-step** D2 (%the (step** E' E'') D2**))
  %<- (step**/trans D1** D2** (%the (step** E E'') D**)) %.
%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

%sort expansion {_ eval E' V} {_ step E E'} {_ eval E V} %.
%mode expansion %in %in %out %.

Case step/s:

%term _
  %pi (expansion (%the (eval (s E') (s V)) (eval/s (%the (eval E' V) Deval'))) (%the (step (s E) (s E')) (step/s (%the (step E E') Dstep))) (%the (eval (s E) (s V)) (eval/s (%the (eval E V) Deval))))
  %<- (expansion Deval' Dstep (%the (eval E V) Deval)) %.

Case step/ifz/arg:

%% By inversion, either eval E' V by eval/ifz/z or by eval/ifz/s.
%term _
  %pi (expansion (%the (eval (ifz E' E0 ([x] E1 x)) V0) (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E' z) Dz'))) (%the (step (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))) (step/ifz/arg (%the (step E E') Dstep))) (%the (eval (ifz E E0 ([x] E1 x)) V0) (eval/ifz/z D0 Dz)))
  %<- (expansion Dz' Dstep (%the (eval E z) Dz)) %.
%term _ expansion XXX (%the (step (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))) (step/ifz/arg (%the (step E E') Dstep))) YYY %.
%%% fill in here.

Case step/ifz/z:

%term _ expansion (%the (eval E0 V0) Deval') (%the (step (ifz z E0 ([x] E1 x)) E0) step/ifz/z) (eval/ifz/z Deval' eval/z) %.

Case step/ifz/s:

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

Case step/app/fn:

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

Case step/app/arg:

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

Case step/app/beta-v:

%term _ expansion XXX (%the (step (app (fn T1 T2 ([f] [x] E f x)) V2) (E (fn T1 T2 ([f] [x] E f x)) V2)) (step/app/beta-v (%the (value V2) Dval2))) 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

%sort multi**-eval {_ step** E V} {_ value V} {_ eval E V} %.
%mode multi**-eval %in %in %out %.
%%% 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

%sort multi-eval {_ step* E V} {_ value V} {_ eval E V} %.
%mode multi-eval %in %in %out %.
%%% fill in here.
%worlds () (multi-eval _ _ _) %.
%total {} (multi-eval _ _ _) %.