% Simply typed call-by-value lambda-calculus with constants, % in the intrinsic encoding. % % The main attractions are: % - Twelf doing all type inference, % - subject reduction is more than trivial: it is the very definition of eval, % - progress is quite straightforward. % The intrinsic encoding is explained in % http://twelf.plparty.org/wiki/Intrinsic_encoding % and has been independently pointed out by Chung-chieh Shan. % The present code is similar in spirit (but not in detail) to the code % presented in Class 3 "Type safety for MinML (intrinsic encoding)" % of http://twelf.plparty.org/wiki/Summer_school_2008 % % Calculus: % - Call-by-value lambda-calculus with integers, arithmetic, fix-point % - Simply typed % - Small-step semantics with NO explicit contexts % % Formalization: % - Higher-order abstract syntax % - Includes both evaluation and type inference (`theory') and % the type soundness proofs (`meta-theory') % - No explicit contexts (neither on the object level, nor on the % meta-level. All world declarations are empty) % - Proved value/expression classification % - Proved subject reduction: type preservation in one-step evaluation % and many-step evaluation. % - Proved progress: the one-step evaluation is total % Types tp: type. int: tp. % one single primitive type for now. => : tp -> tp -> tp. %infix right 200 =>. % Expressions exp : tp -> type. % All expressions are typed % Abstractions and applications l : (exp A -> exp B) -> exp (A => B). @ : exp (A => B) -> exp A -> exp B. %infix left 300 @. % primitive values: natural literals and the increment function nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. n : nat -> exp int. %prefix 400 n. % numeric literals inc : exp (int => int). dec : exp (int => int). ifz : exp int -> exp A -> exp A -> exp A. fix : (exp A -> exp A) -> exp A. % The static semantics -- the definition of the type system -- % has already been specified above! % Type judgements are commonly syntactially defined: % in the above, they are really specified right with the syntax. % ------------------------------------------------------------------------ % Dynamic semantics % % The advantage of the present approach is that the dynamic semantics % below both specifies the evaluation behavior and embodies the proof % of soundness. % Type preservation is stated in the very definition of eval and eval*: % eval : {E:exp T} non-value E -> exp T -> type. % eval*: exp T -> exp T -> type. % % the expressions related by eval have the same type T. % Progress is even more straighforward. All our expressions are typed. % So, we should prove that if E is not a value, it is in the domain of eval. % Thus we merely have to prove that the eval relation is total, % along with the auxiliary proof that each expression is either a value % or not a value. % -------------------------------------------------- % Value classification % Some expressions are values, some other are non-values value: exp T -> type. %mode value +E. v-n: value (n _). v-l: value (l _). v-i: value inc. v-d: value dec. %worlds () (value _). %terminates {} (value _). non-value: exp T -> type. %mode non-value +E. % The following simple rule would have sufficed. % c-@: non-value (_ @ _). % But the following more elaborate rules simplify the congruences. c-@00: non-value (E1 @ E2) <- value E2 <- value E1. c-@1x: non-value (E1 @ E2) <- non-value E1. c-@01: non-value (E1 @ E2) <- non-value E2 <- value E1. % c-z: non-value (ifz _ _ _). c-z0: non-value (ifz E _ _) <- value E. c-z1: non-value (ifz E _ _) <- non-value E. c-f: non-value (fix _). %worlds () (non-value _). %terminates {E} (non-value E). % The following constructively proves that each expression is % either a value or non-value. % The following is purely automatic, and auxiliary % relations vclassify-@ and vclassify-z are defined only because % Twelf's output coverage checker can't deal with pattern-matching % on output arguments . vhood: exp T -> type. a-value : vhood E <- value E. a-non-value : vhood E <- non-value E. vclassify: {E:exp T} vhood E -> type. %mode vclassify +E -P. -: vclassify _ (a-value v-n). -: vclassify _ (a-value v-l). -: vclassify _ (a-value v-i). -: vclassify _ (a-value v-d). vclassify-@: vhood E1 -> vhood E2 -> non-value (E1 @ E2) -> type. %mode vclassify-@ +VE1 +VE2 -VE. -: vclassify-@ (a-value V1) (a-value V2) (c-@00 V1 V2). -: vclassify-@ (a-value V1) (a-non-value V2) (c-@01 V1 V2). -: vclassify-@ (a-non-value V1) _ (c-@1x V1). %worlds () (vclassify-@ _ _ _). %total {} (vclassify-@ _ _ _). -: vclassify (E1 @ E2) (a-non-value R) <- vclassify E1 PE1 <- vclassify E2 PE2 <- vclassify-@ PE1 PE2 R. vclassify-z: vhood E -> {E1:exp T} {E2:exp T} non-value (ifz E E1 E2) -> type. %mode vclassify-z +VE +E1 +E2 -PE. -: vclassify-z (a-value V1) _ _ (c-z0 V1). -: vclassify-z (a-non-value V1) _ _ (c-z1 V1). %worlds () (vclassify-z _ _ _ _). %total {} (vclassify-z _ _ _ _). -: vclassify (ifz E E1 E2) (a-non-value R) <- vclassify E PE <- vclassify-z PE E1 E2 R. -: vclassify _ (a-non-value c-f). %worlds () (vclassify _ _). %total {E} (vclassify E _). % -------------------------------------------------- % Small-step evaluation. Values are not in the domain of eval eval : {E:exp T} non-value E -> exp T -> type. %mode eval +E1 +VC -E2. ev-@: eval ((l EB) @ E) (c-@00 _ _) (EB E). % beta-v ev-@1: eval (E1 @ E2) (c-@1x PE1-NV) (E1' @ E2) <- eval E1 PE1-NV E1'. ev-@2: eval (E1 @ E2) (c-@01 _ PE2-NV) (E1 @ E2') <- eval E2 PE2-NV E2'. ev-i: eval (inc @ (n N)) _ (n (1 N)). ev-d0: eval (dec @ (n 0)) _ (n 0). % to keep dec total, we assume ev-d+: eval (dec @ (n (1 N))) _ (n N). % that dec 0 is 0 ev-z0: eval (ifz (n 0) E1 E2) _ E1. ev-z+: eval (ifz (n (1 _)) E1 E2) _ E2. ev-z1: eval (ifz E E1 E2) (c-z1 PE-NV) (ifz E' E1 E2) <- eval E PE-NV E'. ev-f: eval (fix EB) _(EB (fix EB)). %worlds () (eval _ _ _). %terminates {E} (eval E _ _). %covers eval +E1 +VC -E2. %total {E} (eval E _ _). % Transitive closure of eval eval*: exp T -> exp T -> type. %mode eval* +E1 -E2. -: eval* E E <- value E. -: eval* E ER <- vclassify E (a-non-value PNV) <- eval E PNV E' <- eval* E' ER. % Evaluation tests n0 = n 0. n1 = n (1 0). n2 = n (1 1 0). n3 = n (1 1 1 0). n4 = n (1 1 1 1 0). n5 = n (1 1 1 1 1 0). n6 = n (1 1 1 1 1 1 0). n7 = n (1 1 1 1 1 1 1 0). % The addition function add = fix ([self] l [x] l [y] ifz x y (inc @ (self @ (dec @ x) @ y))). % Nice to see all types inferred: % add : exp (int => int => int) % = fix % ([self:exp (int => int => int)] % l % ([x:exp int] % l ([y:exp int] ifz x y (inc @ (self @ (dec @ x) @ y))))). %query 1 2 eval* (add @ n2 @ n3) n5. % The multiplication function mul = fix ([self] l [x] l [y] ifz x (n 0) (ifz (dec @ x) y (add @ y @ (self @ (dec @ x) @ y)))). %query 1 2 eval* (mul @ n2 @ n0) n0. %query 1 2 eval* (mul @ n0 @ n3) n0. %query 1 2 eval* (mul @ n2 @ n3) n6. % The factorial function fact = fix ([self] l [x] ifz x n1 (mul @ x @ (self @ (dec @ x)))). %query 1 2 eval* (fact @ n3) n6. %%query 1 2 eval* (fact @ n4) R. % R = n (1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0).