Summer school 2008:Type safety for MinML (extrinsic encoding)
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
| Summer school 2008 |
| Previous: Type safety for MinML (intrinsic encoding) |
| Next: Exercises 3 |
Type safety for MinML: call-by-value, with recursive functions, in extrinsic form
Syntax
Types:
tp : type. %name tp T. nat : tp. arr : tp -> tp -> tp.
Raw expressions, which admit ill-typed terms
exp : type. %name exp E. z : exp. s : exp -> exp. ifz : exp -> exp -> (exp -> exp) -> exp. fun : tp -> tp -> (exp -> exp -> exp) -> exp. app : exp -> exp -> exp.
Static semantics
A judgement picking out the well-typed terms:
of : exp -> tp -> type. %name of Dof.
%mode of +E -T.
of/z
: of z nat.
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).
of/fun
: of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2)
<- ({f:exp} of f (arr T1 T2) -> {x:exp} of x T1 -> of (E f x) T2).
of/app
: of (app E1 E2) T
<- of E1 (arr T2 T)
<- of E2 T2.
Dynamic semantics
value : exp -> type. %name value Dval.
%mode value +E.
value/z : value z.
value/s : value (s E) <- value E.
value/fun : value (fun _ _ _).
step : exp -> exp -> type. %name step Dstep.
%mode step +E1 -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.
step/app/fun
: 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-v
: step
(app (fun T1 T2 ([f] [x] E f x)) E2)
(E (fun T1 T2 ([f] [x] E f x)) E2)
<- value E2.
Preservation
With this encoding, we have to prove preservation explicitly, as the type of step doesn't guarantee it.
pres : step E E' -> of E T -> of E' T -> type. %name pres Dpres.
%mode pres +Dstep +Dof -Dof.
- : pres
(step/s Dstep)
(of/s Dof)
(of/s Dof')
<- pres Dstep Dof Dof'.
- : 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'.
- : pres
step/ifz/z
(of/ifz _ Dof1 _)
Dof1.
- : pres
(step/ifz/s (_ : value E))
(of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof))
(Dof2 E Dof).
- : pres
(step/app/fun Dstep1)
(of/app Dof2 Dof1)
(of/app Dof2 Dof1')
<- pres Dstep1 Dof1 Dof1'.
- : pres
(step/app/arg Dstep2 _)
(of/app Dof2 Dof1)
(of/app Dof2' Dof1)
<- pres Dstep2 Dof2 Dof2'.
- : pres
(step/app/beta-v _)
(of/app
Dof2
(of/fun [f] [df] [x] [dx] (Dof1 f df x dx)))
(Dof1
_
(of/fun [f] [df] [x] [dx] (Dof1 f df x dx))
_
Dof2).
%worlds () (pres Dstep Dof Dof').
%total Dstep (pres Dstep _ _).
Progress
val-or-step : exp -> type. %name val-or-step Dvos. vos/val : val-or-step E <- value E. vos/step : val-or-step E <- step E _.
Factoring lemmas
prog/s
: val-or-step E -> val-or-step (s E) -> type.
%mode prog/s +Dvos1 -Dvos2.
- : prog/s
(vos/step Dstep)
(vos/step (step/s Dstep)).
- : prog/s
(vos/val Dval)
(vos/val (value/s Dval)).
%worlds () (prog/s _ _).
%total {} (prog/s _ _).
prog/ifz
: of E nat
-> val-or-step E
-> {E1} {E2} (step (ifz E E1 ([x] E2 x)) E')
-> type.
%mode prog/ifz +Dof +Dvos +E1 +E2 -Dstep.
- : prog/ifz _ (vos/step Dstep) _ _ (step/ifz/arg Dstep).
- : prog/ifz _ (vos/val value/z) _ _ step/ifz/z.
- : prog/ifz _ (vos/val (value/s Dval)) _ _ (step/ifz/s Dval).
%worlds () (prog/ifz _ _ _ _ _).
%total {} (prog/ifz _ _ _ _ _).
prog/app
: of E1 (arr T2 T)
-> val-or-step E1
-> val-or-step E2
-> step (app E1 E2) E'
-> type.
%mode prog/app +Dof +Dvos1 +Dvos2 -Dstep.
- : prog/app
_
(vos/step Dstep1)
_
(step/app/fun Dstep1).
- : prog/app
_
(vos/val Dval1)
(vos/step Dstep2)
(step/app/arg Dstep2 Dval1).
- : prog/app
_
(vos/val Dval1)
(vos/val Dval2)
(step/app/beta-v Dval2).
%worlds () (prog/app _ _ _ _).
%total {} (prog/app _ _ _ _).
Main theorem
prog : of E T -> val-or-step E -> type. %name prog Dprog.
%mode prog +Dof -Dvos.
- : prog of/z (vos/val value/z).
- : prog (of/s Dof) Dvos'
<- prog Dof Dvos
<- prog/s Dvos Dvos'.
- : prog (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) (vos/step Dstep)
<- prog Dof Dvos
<- prog/ifz Dof Dvos _ _ Dstep.
- : prog (of/fun _) (vos/val value/fun).
- : prog (of/app Dof2 Dof1) (vos/step Dstep)
<- prog Dof1 Dvos1
<- prog Dof2 Dvos2
<- prog/app Dof1 Dvos1 Dvos2 Dstep.
%worlds () (prog _ _).
%total Dof (prog Dof _).
And thus we have proved type safety for minml!
Examples
%abbrev plus : exp =
fun nat (arr nat nat)
([plus] [x] ifz x
(fun nat nat ([_] [y] y))
([predx] (fun nat nat ([_] [y] s (app (app plus predx) y))))).
%solve D : of plus T.
%abbrev mult : exp =
fun nat (arr nat nat)
([mult] [x] (fun nat nat
[_] [y]
ifz y
z
([predy] app (app plus x) (app (app mult x) predy)))).
%solve Dmult : of mult T.
%abbrev fact : exp =
fun nat nat ([fact] [x]
ifz x
(s z)
([predx] (app (app mult x) (app fact predx)))).
%solve Dfact : of fact T.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%solve of (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) T. OK Dfact : of (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ( [e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (arr nat nat) = of/fun ([f:exp] [dof:of f (arr nat nat)] [x:exp] [dof1:of x nat] of/ifz ([x3:exp] [dof2:of x3 nat] of/app (of/app dof2 dof) (of/app dof1 (of/fun ([f1:exp] [dof3:of f1 (arr nat (arr nat nat))] [x4:exp] [dof4:of x4 nat] of/fun ([f2:exp] [dof5:of f2 (arr nat nat)] [x5:exp] [dof6:of x5 nat] of/ifz ([x6:exp] [dof7:of x6 nat] of/app (of/app dof7 (of/app dof4 dof3)) (of/app dof4 (of/fun ([f3:exp] [dof8:of f3 (arr nat (arr nat nat))] [x7:exp] [dof9:of x7 nat] of/ifz ([x9:exp] [dof10:of x9 nat] of/fun ([f5:exp] [dof11:of f5 (arr nat nat)] [x10:exp] [dof12:of x10 nat] of/s (of/app dof12 (of/app dof10 dof8)))) (of/fun ([f4:exp] [dof10:of f4 (arr nat nat)] [x8:exp] [dof11:of x8 nat] dof11)) dof9)))) of/z dof6))))) (of/s of/z) dof1).
%% OK %%
stepv : exp -> exp -> type. stepv/v : stepv E E <- value E. stepv/s : stepv E E'' <- step E E' <- stepv E' E''. %solve D : stepv (app (app plus (s (s z))) (s (s z))) E. %solve D : stepv (app (app mult (s (s (s z)))) (s (s z))) E.
%solve D : stepv (app fact (s (s (s z)))) E.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%solve stepv (app (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (s (s (s z)))) E. OK D : stepv (app (fun nat nat ([fact1:exp] [x:exp] ifz x (s z) ([predx:exp] app (app (fun nat (arr nat nat) ([mult1:exp] [x1:exp] fun nat nat ([e:exp] [y:exp] ifz y z ([predy:exp] app (app (fun nat (arr nat nat) ([plus1:exp] [x2:exp] ifz x2 (fun nat nat ([e1:exp] [y1:exp] y1)) ([predx1:exp] fun nat nat ([e1:exp] [y2:exp] s (app (app plus1 predx1) y2))))) x1) (app (app mult1 x1) predy))))) x) (app fact1 predx)))) (s (s (s z)))) (s (s (s (s (s (s z)))))) = stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/s (stepv/v (value/s (value/s (value/s (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))))) (step/s (step/s (step/s (step/app/fun step/ifz/z))))) (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z)))))) (step/s (step/s (step/app/beta-v (value/s (value/s (value/s value/z))))))) (step/s (step/s (step/app/fun (step/ifz/s value/z))))) (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z)))))) (step/s (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/s (step/app/fun (step/ifz/s (value/s value/z))))) (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z)))))) (step/app/beta-v (value/s (value/s (value/s value/z))))) (step/app/arg (step/s (step/s (step/s (step/app/beta-v value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun step/ifz/z)))) value/fun)) (step/app/arg (step/s (step/s (step/s (step/app/fun (step/app/beta-v value/z))))) value/fun)) (step/app/arg (step/s (step/s (step/app/beta-v value/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/ifz/s value/z)))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/app/beta-v (value/s value/z))))) value/fun)) (step/app/arg (step/s (step/app/beta-v value/z)) value/fun)) (step/app/arg (step/s (step/app/fun (step/ifz/s (value/s value/z)))) value/fun)) (step/app/arg (step/s (step/app/fun (step/app/beta-v (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/app/beta-v value/z) value/fun)) (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun) value/fun)) (step/app/arg (step/app/fun (step/ifz/s (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/arg (step/ifz/s value/z) value/fun)) (step/app/arg (step/app/beta-v (value/s value/z)) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z))))) value/fun)) (step/app/fun (step/ifz/s (value/s (value/s value/z))))) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/ifz/s (value/s value/z))) (step/app/beta-v (value/s (value/s value/z)))) (step/app/arg (step/s (step/s (step/app/beta-v value/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun step/ifz/z))) value/fun)) (step/app/arg (step/s (step/s (step/app/fun (step/app/beta-v value/z)))) value/fun)) (step/app/arg (step/s (step/app/beta-v value/z)) value/fun)) (step/app/arg (step/s (step/app/fun (step/ifz/s value/z))) value/fun)) (step/app/arg (step/s (step/app/fun (step/app/beta-v (value/s value/z)))) value/fun)) (step/app/arg (step/app/beta-v value/z) value/fun)) (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun) value/fun)) (step/app/arg (step/app/fun (step/ifz/s (value/s value/z))) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/ifz/s value/z) value/fun)) (step/app/arg (step/app/beta-v (value/s value/z)) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/beta-v value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/fun step/ifz/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/s (step/app/fun (step/app/beta-v value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/ifz/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/ifz/s value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v (value/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg step/ifz/z value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/arg (step/app/beta-v value/z) value/fun) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/fun (step/app/beta-v (value/s value/z))) value/fun) value/fun)) (step/app/arg (step/app/arg (step/ifz/s value/z) value/fun) value/fun)) (step/app/arg (step/app/arg (step/app/beta-v (value/s value/z)) value/fun) value/fun)) (step/app/arg (step/app/fun (step/app/beta-v (value/s (value/s value/z)))) value/fun)) (step/app/arg (step/ifz/s (value/s value/z)) value/fun)) (step/app/arg (step/app/beta-v (value/s (value/s value/z))) value/fun)) (step/app/fun (step/app/beta-v (value/s (value/s (value/s value/z)))))) (step/ifz/s (value/s (value/s value/z)))) (step/app/beta-v (value/s (value/s (value/s value/z)))).
%% OK %%
| Summer school 2008 |
| Previous: Type safety for MinML (intrinsic encoding) |
| Next: Exercises 3 |
