POPL Tutorial/MinML Preservation Theorem
From The Twelf Project
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.
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.
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 _ _).