POPL Tutorial/MinML Preservation Theorem: Solution

This is the solution to this exercise.

Type safety for MinML

|hidden = true

%% Syntax %%
%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 %.
%% Static semantics %%
%sort of {_ exp} {_ tp} %.
%name of %.
%mode of %in %out %.
%term of/z of z nat %.
%term of/fn
  %pi (of (fn T1 ([x] E x)) (arr T1 T2))
  %<- ({x exp} %pi (of x T1) %-> (of (E x) T2)) %.
%term of/app %pi (of (app E1 E2) T) %<- (of E1 (arr T2 T)) %<- (of E2 T2) %.
%term of/s %pi (of (s E) nat) %<- (of E nat) %.
%term of/ifz
  %pi (of (ifz E E1 ([x] E2 x)) T)
  %<- (of E nat)
  %<- (of E1 T)
  %<- ({x exp} %pi (of x nat) %-> (of (E2 x) T)) %.
%% 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) %.

Preservation

%sort pres {_ step E E'} {_ of E T} {_ of E' T} %.
%name pres %.
%mode pres %in %in %out %.
%term _ %pi (pres (step/s Dstep) (of/s Dof) (of/s Dof')) %<- (pres Dstep Dof Dof') %.
%term _
  %pi (pres (step/ifz/arg Dstep) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof'))
  %<- (pres Dstep Dof Dof') %.
%term _ pres step/ifz/z (of/ifz _ Dof1 _) Dof1 %.
%term _ pres (step/ifz/s (%the (value E) _)) (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof)) (Dof2 E Dof) %.
%term _
  %pi (pres (step/app/fn Dstep1) (of/app Dof2 Dof1) (of/app Dof2 Dof1'))
  %<- (pres Dstep1 Dof1 Dof1') %.
%term _
  %pi (pres (step/app/arg Dstep2 _) (of/app Dof2 Dof1) (of/app Dof2' Dof1))
  %<- (pres Dstep2 Dof2 Dof2') %.
%term _ pres (step/app/beta _) (of/app Dof2 (of/fn ([x] [dx] Dof1 x dx))) (Dof1 _ Dof2) %.
%worlds () (pres Dstep Dof Dof') %.
%total Dstep (pres Dstep _ _) %.