POPL Tutorial/MinML Answer

Syntax

%sort tp %.
%name tp %.
%term num tp %.
%term arr %pi tp %-> tp %-> tp %.
%% you can world-check syntax if you want
%worlds () (tp) %.
%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 %.

Exercise: constant for ifz

%term ifz %pi exp %-> exp %-> (%pi exp %-> exp) %-> exp %.
%% you can world-check syntax if you want
%block exp_block {x exp}%.
%worlds (exp_block) (exp) %.

Static semantics

%sort of {_ exp} {_ tp} %.
%name of %.
%term of/z of z num %.
%term of/app %pi (of (app E1 E2) T) %<- (of E1 (arr T' T)) %<- (of E2 T') %.
%term of/fn
  %pi (of (fn T1 ([x] E x)) (arr T1 T2))
  %<- ({x exp} %pi (of x T1) %-> (of (E x) T2)) %.

Exercise: typing rules for s and ifz

%term of/s %pi (of (s E) num) %<- (of E num) %.
%term of/ifz
  %pi (of (ifz E E0 ([x] E1 x)) T)
  %<- (of E num)
  %<- (of E0 T)
  %<- ({x exp} %pi (of x num) %-> (of (E1 x) T)) %.
%block of_block [T tp] {x exp} {dx of x T}%.
%worlds (of_block) (of _ _) %.

Dynamic semantics

value judgement

%sort value {_ exp} %.
%name value %.
%term value/fn value (fn T ([x] E x)) %.

Exercise: value rules for z and s

%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.

step judgement

%sort step {_ exp} {_ exp} %.
%name step %.
%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 T ([x] E x)) E2) (E E2)) %<- (value E2) %.

Exercise: step rules for s and ifz

%term step/s %pi (step (s E) (s E')) %<- (step E E') %.
%term step/ifz/arg %pi (step (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))) %<- (step E E') %.
%term step/ifz/z step (ifz z E0 ([x] E1 x)) E0 %.
%term step/ifz/s %pi (step (ifz (s E) E0 ([x] E1 x)) (E1 E)) %<- (value E) %.

Progress theorem

Sum type for the result

%sort val-or-step {_ exp} %.
%name val-or-step %.
%term vos/value %pi (val-or-step E) %<- (value E) %.
%term vos/step %pi (val-or-step E) %<- (step E E') %.

Lemmas

%sort prog/app {_ of E1 (arr T' T)} {_ val-or-step E1} {_ val-or-step E2} {_ val-or-step (app E1 E2)} %.
%mode prog/app %in %in %in %out %.
%term _ prog/app _ (vos/step (%the (step E1 E1') Dstep1)) _ (vos/step (step/app/fn Dstep1)) %.
%term _ prog/app _ (vos/value (%the (value E1) Dval1)) (vos/step (%the (step E2 E2') Dstep2)) (vos/step (step/app/arg Dstep2 Dval1)) %.
%term _ prog/app (%the (of (fn T ([x] E' x)) (arr T T')) (of/fn _)) (vos/value (%the (value (fn T ([x] E' x))) Dval1)) (vos/value (%the (value E2) Dval2)) (vos/step (step/app/beta Dval2)) %.
%worlds () (prog/app _ _ _ _) %.
%total {} (prog/app _ _ _ _) %.

Exercise: lemma for s

%sort prog/s {_ val-or-step E} {_ val-or-step (s E)} %.
%mode prog/s %in %out %.
%term _ prog/s (vos/step (%the (step E E') Dstep)) (vos/step (step/s Dstep)) %.
%term _ prog/s (vos/value (%the (value E) Dval)) (vos/value (value/s Dval)) %.
%worlds () (prog/s _ _) %.
%total {} (prog/s _ _) %.

Exercise: lemma for ifz

%sort prog/ifz {_ of E num} {E0 exp} {E1 %pi exp %-> exp} {_ val-or-step E} {_ step (ifz E E0 ([x] E1 x)) E'} %.
%mode prog/ifz %in %in %in %in %out %.
%mode prog/ifz %in %in %in %in %out %.
%term _ prog/ifz _ _ _ (vos/step Dstep) (step/ifz/arg Dstep) %.
%term _ prog/ifz _ _ _ (vos/value value/z) step/ifz/z %.
%term _ prog/ifz _ _ _ (vos/value (value/s Dval)) (step/ifz/s Dval) %.
%worlds () (prog/ifz _ _ _ _ _) %.
%total {} (prog/ifz _ _ _ _ _) %.

Main theorem

%sort prog {_ of E T} {_ val-or-step E} %.
%mode prog %in %out %.
%term _ prog (%the (of z num) of/z) (vos/value (%the (value z) value/z)) %.
%term _ prog (of/fn _) (vos/value value/fn) %.
%term _
  %pi (prog (of/app (%the (of E2 T') D2) (%the (of E1 (arr T' T)) D1)) DvosApp)
  %<- (prog D1 (%the (val-or-step E1) Dvos1))
  %<- (prog D2 (%the (val-or-step E2) Dvos2))
  %<- (prog/app D1 Dvos1 Dvos2 DvosApp) %.

Exercise: cases for s and ifz

%term _
  %pi (prog (of/s (%the (of E num) D)) DvosS)
  %<- (prog D (%the (val-or-step E) Dvos))
  %<- (prog/s Dvos DvosS) %.
%term _
  %pi (prog (of/ifz ([x] [dx of x num] %the (of (E1 x) T) (D1 x dx)) (%the (of E0 T) D0) (%the (of E num) D)) (vos/step DstepIfz))
  %<- (prog D (%the (val-or-step E) Dvos))
  %<- (prog/ifz D E0 ([x] E1 x) Dvos DstepIfz) %.
%worlds () (prog _ _) %.
%total Dof (prog Dof _) %.