POPL Tutorial/MinML Preservation Theorem

This is Literate Twelf Code: here Status: %% ABORT %% Output: here.

In this exercise, we prove the preservation theorem for the MinML langauge we worked with before.

There is one task:

• Complete the cases of the preservation theorem

The solution is here.

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.

Static semantics

of : exp -> tp -> type.			%name of Dof.
%mode of +E -T.

of/z : of z nat.
of/fn : of (fn T1 ([x] E x)) (arr T1 T2)
	 <- ({x:exp} of x T1 -> of (E x) T2).
of/app : of (app E1 E2) T
      <- of E1 (arr T2 T)
      <- of E2 T2.
of/s : of (s E) nat 
	<- of E nat.
of/ifz : of (ifz E E1 ([x] E2 x)) T
	  <- of E nat
	  <- of E1 T
	  <- ({x:exp} of x nat -> of (E2 x) T).

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.

Preservation

TASK 1: Fill in missing cases

pres : step E E' -> of E T -> of E' T -> type. %name pres Dpres.
%mode pres +Dstep +Dof -Dof.

% fill in here.

%worlds () (pres Dstep Dof Dof').
%total Dstep (pres Dstep _ _).