Summer school 2008:Type safety for MinML (extrinsic encoding)

From The Twelf Project
Jump to: navigation, search
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