% Small-step semantics for System F with constants and additional % typing rules, closely following the `Syntactic Approach to Type % Soundness' with contexts, focusing and redexing. % The type preservation and progress proofs indeed factor out into % the type preservation for redexes, and the progress for typed pre-values. % Plus the context typing rules, which are shared across the % preservation and progress proofs. % Indeed, the lemma `tpsfocus' -- asserting that if an expression is % well-typed then the result of its focusing is well-typed -- % is used both in the type preservation proof (see `tps' -- only one line % of proof) and in the progress proof (see `fprog' below -- again % only one rule). % Evaluation contexts are modeled as meta-level functions. % Our particular application is safety of list access % % Proving soundness of the `strict' type system for % the language made of System F plus lists and non-empty lists. % The progress theorem below assures the safety property: % a well-typed program shall not attempt to take the head or tail % of a non-empty list. % % This is a joint work with Chung-chieh Shan. % For the context, please see % http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html tp : type. %name tp T. % type constructors => : tp -> tp -> tp. %infix right 10 =>. all : (tp -> tp) -> tp. list : tp -> tp. list+ : tp -> tp. % value constructors and constants: the term language exp : type. %name exp E. lam : (exp -> exp) -> exp. app : exp -> exp -> exp. tlam : (tp -> exp) -> exp. % type lambda tapp : exp -> tp -> exp. % type application nil : exp. cons : exp -> exp -> exp. head : exp -> exp. tail : exp -> exp. indeed : exp -> exp -> exp -> exp. nonempty : exp -> exp. % ---------------------------------------------------------------------- % Static semantics: type checking of : exp -> tp -> type. %name of P. %mode of +E *T. % Expression E has type T tp_lam : of (lam E) (T1 => T2) <- {x:exp} of x T1 -> of (E x) T2. tp_app : of (app E1 E2) T2 <- of E1 (T1 => T2) <- of E2 T1. tp_tlam : of (tlam E) (all T) <- {t:tp} of (E t) (T t). tp_tapp : of (tapp E T1) (T T1) <- of E (all T). tp_nil : of (nil) (list T). tp_cons : of (cons E1 E2) (list T) <- of E1 T <- of E2 (list T). tp_head : of (head E) T <- of E (list+ T). tp_tail : of (tail E) (list T) <- of E (list+ T). tp_indeed : of (indeed E1 E2 E3) W <- of E1 (list T) <- of E2 W <- of E3 (list+ T => W). % security properties, via special typing rules: % nonempty E has a type only if E structurally is a cons expression, that is, % a non-empty list. tp_nonempty : of (nonempty (cons E1 E2)) (list+ T) <- of E1 T <- of E2 (list T). %block tp_var : some {T:tp} block {x:exp} {u:of x T}. %block tp_tvar : block {t:tp}. %worlds (tp_var | tp_tvar) (of E T). %terminates E (of E T). % This fails thanks to nonempty: %covers of +E *T. % examples of typechecking of various expressions c0 = (lam [f] lam [x] x). c1 = (lam [f] lam [x] (app f x)). c2 = (lam [f] lam [x] app f (app f x)). c3 = (lam [f] lam [x] app f (app f (app f x))). sample_list = (cons c0 (cons c1 (cons c2 nil))). %query 1 2 of (tlam [t] cons (lam [x] x) nil) T. %query 1 2 of (tlam [t] indeed (cons (lam [x] x) nil) (lam [x] x) (lam [y] head y)) T. %query 1 1 of (indeed (cons c0 nil) c3 (lam [l] (indeed (tail l) c2 (lam [l] (head l))))) T. % If we attempt to use non-empty by itself, it won't typecheck %query 0 1 of (indeed sample_list c3 (lam [l] head (nonempty (tail l)))) T. % ---------------------------------------------------------------------- % Classification of expressions: values and contexts val : exp -> type. %name val P. %mode val +E. val_lam : val (lam E). val_tlam : val (tlam E). val_nil : val (nil). val_cons : val (cons E1 E2) <- val E1 <- val E2. val_nonempty : val (nonempty E) <- val E. %worlds () (val E). %terminates E (val E). % pre-values: non-values that can't be focused further % That is, pre-values can either be reduced by a redex rule, or % otherwise get stuck. pre-val : exp -> type. %mode pre-val +E. preval-app : val E1 -> val E2 -> pre-val (app E1 E2). preval-tapp : {T:tp} val E -> pre-val (tapp E T). preval-head : val E1 -> pre-val (head E1). preval-tail : val E1 -> pre-val (tail E1). preval-indeed : val E1 -> pre-val (indeed E1 E2 E3). %worlds () (pre-val _). %terminates E (pre-val E). % Focusing: given a non-value expression, return a pre-value and % its context. Actually, we produce the proof of a pre-value (from % whose type we can extract the pre-value itself). % A context is a function exp->exp. % We later prove that any non-value can be focused. % contexts %{ ctx : (exp -> exp) -> type. %name ctx C. %mode ctx +F. ctx-null : ctx ([x] x). ctx-app1 : ctx ([x] (app (C1 x) E2)) <- ctx C1. ctx-app2 : ctx ([x] (app E1 (C2 x))) <- val E1 <- ctx C2. %terminates F (ctx F). %worlds () (ctx _). }% % The expression to focus into is implicit: it is the application % of the context to ER. focus : pre-val ER -> (exp -> exp) -> type. %name focus F. focus-app : {PE1 : val E1} {PE2 : val E2} focus (preval-app PE1 PE2) ([x] x). focus-app1 : focus PPV C1 -> focus PPV ([x] (app (C1 x) E2)). focus-app2 : val E1 -> focus PPV C2 -> focus PPV ([x] (app E1 (C2 x))). focus-tapp : {PE : val E} focus (preval-tapp T PE) ([x] x). focus-tapp1 : focus PPV C -> focus PPV ([x] (tapp (C x) T)). focus-cons1 : focus PPV C1 -> focus PPV ([x] (cons (C1 x) E2)). focus-cons2 : val E1 -> focus PPV C2 -> focus PPV ([x] (cons E1 (C2 x))). focus-nonempty1 : focus PPV C -> focus PPV ([x] nonempty (C x)). focus-head : {PE : val E} focus (preval-head PE) ([x] x). focus-head1 : focus PPV C -> focus PPV ([x] head (C x)). focus-tail : {PE : val E} focus (preval-tail PE) ([x] x). focus-tail1 : focus PPV C -> focus PPV ([x] tail (C x)). focus-indeed : {PE1 : val E1} focus ((preval-indeed PE1) : pre-val (indeed _ E2 E3)) ([x] x). focus-indeed1 : focus PPV1 C -> focus PPV1 ([x] (indeed (C x) E2 E3)). % Proving the classification theorem: every expression is either a value % or can be focused (that is, decomposed into the context and a pre-value). % This is the most tiresome part... % It's purely syntactical, there aren't any (object-level) types involved... val-or-focus : exp -> type. % The (dependent) sum type val-or-focus-val : val E -> val-or-focus E. val-or-focus-focus : focus (_ : pre-val E) C -> val-or-focus (C E). % classification of expressions. val-focus-disj : {E:exp} val-or-focus E -> type. %mode val-focus-disj +E -VOF. - : val-focus-disj _ (val-or-focus-val val_lam). - : val-focus-disj _ (val-or-focus-val val_tlam). - : val-focus-disj _ (val-or-focus-val val_nil). % lemma for application. Factoring. vfd-app : val-or-focus E1 -> val-or-focus E2 -> val-or-focus (app E1 E2) -> type. %mode vfd-app +P1 +P2 -P3. - : vfd-app (val-or-focus-val P1) (val-or-focus-val P2) (val-or-focus-focus (focus-app P1 P2)). - : vfd-app (val-or-focus-focus P1) _ (val-or-focus-focus (focus-app1 P1)). - : vfd-app (val-or-focus-val P1) (val-or-focus-focus P2) (val-or-focus-focus (focus-app2 P1 P2)). %worlds () (vfd-app _ _ _). %total {} (vfd-app _ _ _). - : val-focus-disj _ P <- val-focus-disj _ PE1 <- val-focus-disj _ PE2 <- vfd-app PE1 PE2 P. vfd-tapp : {T:tp} val-or-focus E1 -> val-or-focus (tapp E1 T) -> type. %mode vfd-tapp +T +P1 -P2. - : vfd-tapp _ (val-or-focus-val P1) (val-or-focus-focus (focus-tapp P1)). - : vfd-tapp _ (val-or-focus-focus P1) (val-or-focus-focus (focus-tapp1 P1)). %worlds () (vfd-tapp _ _ _). %total {} (vfd-tapp _ _ _). - : val-focus-disj (tapp _ T) P <- val-focus-disj _ PE1 <- vfd-tapp T PE1 P. vfd-cons : val-or-focus E1 -> val-or-focus E2 -> val-or-focus (cons E1 E2) -> type. %mode vfd-cons +P1 +P2 -P3. - : vfd-cons (val-or-focus-val P1) (val-or-focus-val P2) (val-or-focus-val (val_cons P2 P1)). - : vfd-cons (val-or-focus-focus P1) _ (val-or-focus-focus (focus-cons1 P1)). - : vfd-cons (val-or-focus-val P1) (val-or-focus-focus P2) (val-or-focus-focus (focus-cons2 P1 P2)). %worlds () (vfd-cons _ _ _). %total {} (vfd-cons _ _ _). - : val-focus-disj _ P <- val-focus-disj _ PE1 <- val-focus-disj _ PE2 <- vfd-cons PE1 PE2 P. vfd-nonempty : val-or-focus E1 -> val-or-focus (nonempty E1) -> type. %mode vfd-nonempty +P1 -P2. - : vfd-nonempty (val-or-focus-val P1) (val-or-focus-val (val_nonempty P1)). - : vfd-nonempty (val-or-focus-focus P1) (val-or-focus-focus (focus-nonempty1 P1)). %worlds () (vfd-nonempty _ _). %total {} (vfd-nonempty _ _). - : val-focus-disj _ P <- val-focus-disj _ PE1 <- vfd-nonempty PE1 P. vfd-head : val-or-focus E1 -> val-or-focus (head E1) -> type. %mode vfd-head +P1 -P2. - : vfd-head (val-or-focus-val P1) (val-or-focus-focus (focus-head P1)). - : vfd-head (val-or-focus-focus P1) (val-or-focus-focus (focus-head1 P1)). %worlds () (vfd-head _ _). %total {} (vfd-head _ _). - : val-focus-disj _ P <- val-focus-disj _ PE1 <- vfd-head PE1 P. vfd-tail : val-or-focus E1 -> val-or-focus (tail E1) -> type. %mode vfd-tail +P1 -P2. - : vfd-tail (val-or-focus-val P1) (val-or-focus-focus (focus-tail P1)). - : vfd-tail (val-or-focus-focus P1) (val-or-focus-focus (focus-tail1 P1)). %worlds () (vfd-tail _ _). %total {} (vfd-tail _ _). - : val-focus-disj _ P <- val-focus-disj _ PE1 <- vfd-tail PE1 P. vfd-indeed : {E2:exp} {E3:exp} val-or-focus E1 -> val-or-focus (indeed E1 E2 E3) -> type. %mode vfd-indeed +E2 +E3 +P1 -P2. - : vfd-indeed _ _ (val-or-focus-val P1) (val-or-focus-focus (focus-indeed P1)). - : vfd-indeed _ _ (val-or-focus-focus P1) (val-or-focus-focus (focus-indeed1 P1)). %worlds () (vfd-indeed _ _ _ _). %total {} (vfd-indeed _ _ _ _). - : val-focus-disj (indeed _ E2 E3) P <- val-focus-disj _ PE1 <- vfd-indeed E2 E3 PE1 P. %worlds () (val-focus-disj _ _). %total E (val-focus-disj E _). % At long last... % ---------------------------------------------------------------------- % Dynamic semantics: small-step evaluation relation % Redexes and their reductions. The small-step semantics. % At last the interesting part. rdx : exp -> exp -> type. %name rdx R. %mode rdx +E1 -E2. rdx-app : rdx (app (lam E1) E2) (E1 E2) <- val E2. rdx-tapp : {t:tp} rdx (tapp (tlam E) t) (E t). rdx-head : rdx (head (nonempty (cons E1 E2))) E1 <- val E1 <- val E2. rdx-tail : rdx (tail (nonempty (cons E1 E2))) E2 <- val E1 <- val E2. rdx-indeed-nil : rdx (indeed (nil) E2 E3) E2. rdx-indeed-cons : rdx (indeed (cons E11 E12) E2 E3) (app E3 (nonempty (cons E11 E12))) <- val E11 <- val E12. %worlds () (rdx _ _). %terminates E (rdx E _). % Combine focusing and evaluation. % We can now reap the fruits of our labor: the eval relation % is fully generic and does not depend on the details of focusing % or reductions. We can freely add more reduction/context rules. eval : exp -> exp -> type. %name eval D. eval1 : eval (CF ER) (CF ER') <- focus (_ : pre-val ER) CF <- rdx ER ER'. % Big step: transitive closure of eval*: just to be able to run examples eval* : exp -> exp -> type. eval1* : eval* E E <- val E. eval2* : eval* E E'' <- eval E E' <- eval* E' E''. % sample example %query 1 1 eval* (indeed sample_list c3 (lam [l] head l)) E. %query 1 1 eval* (indeed sample_list c3 (lam [l] (indeed (tail l) c3 (lam [l] (head l))))) E. %query 1 1 eval* (indeed (cons c0 nil) c3 (lam [l] (indeed (tail l) c2 (lam [l] (head l))))) E. % ---------------------------------------------------------------------- % Proving type-preservation: small-step evaluation preserves types % First show that redex reductions preserve typing. These % are the interesting rules in this section. tpsrdx : rdx E E' -> of E T -> of E' T -> type. %mode tpsrdx +R +P -Q. - : tpsrdx (rdx-app _) (tp_app P2 (tp_lam P1)) (P1 _ P2). - : tpsrdx (rdx-tapp T) (tp_tapp (tp_tlam P)) (P T). - : tpsrdx (rdx-head _ _) (tp_head (tp_nonempty P2 P1)) P1. - : tpsrdx (rdx-tail _ _) (tp_tail (tp_nonempty P2 P1)) P2. - : tpsrdx (rdx-indeed-nil) (tp_indeed P3 P2 tp_nil) P2. - : tpsrdx (rdx-indeed-cons _ _) (tp_indeed P3 P2 (tp_cons P12 P11)) (tp_app (tp_nonempty P12 P11) P3). %worlds () (tpsrdx D P _). %total D (tpsrdx D P _). % If an expression is well-typed, then the result of its focusing % is well-typed. % The last argument of tpsfocus is to prove the reverse, that is, % the context substitution. tpsfocus : focus (PPV : pre-val ER) CF -> of (CF ER) T -> of ER TR -> ({ER':exp} {p:of ER' TR} of (CF ER') T) -> type. %mode tpsfocus +F +P -P' -PF. - : tpsfocus (focus-app _ _) P P ([e] [p] p). - : tpsfocus (focus-app1 F) (tp_app PA PO) PO' ([e] [p] (tp_app PA (PF _ p))) <- tpsfocus F PO PO' PF. - : tpsfocus (focus-app2 _ F) (tp_app PA PO) PA' ([e] [p] (tp_app (PF _ p) PO)) <- tpsfocus F PA PA' PF. - : tpsfocus (focus-tapp _) P P ([e] [p] p). - : tpsfocus (focus-tapp1 F) (tp_tapp PE) PE' ([e] [p] (tp_tapp (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-cons1 F) (tp_cons PL PE) PE' ([e] [p] (tp_cons PL (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-cons2 _ F) (tp_cons PL PE) PL' ([e] [p] (tp_cons (PF _ p) PE)) <- tpsfocus F PL PL' PF. - : tpsfocus (focus-head _) P P ([e] [p] p). - : tpsfocus (focus-head1 F) (tp_head PE) PE' ([e] [p] (tp_head (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-tail _) P P ([e] [p] p). - : tpsfocus (focus-tail1 F) (tp_tail PE) PE' ([e] [p] (tp_tail (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-indeed _) P P ([e] [p] p). - : tpsfocus (focus-indeed1 F) (tp_indeed PE3 PE2 PE) PE' ([e] [p] (tp_indeed PE3 PE2 (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-nonempty1 (focus-cons1 F)) (tp_nonempty PL PE) PE' ([e] [p] (tp_nonempty PL (PF _ p))) <- tpsfocus F PE PE' PF. - : tpsfocus (focus-nonempty1 (focus-cons2 _ F)) (tp_nonempty PL PE) PL' ([e] [p] (tp_nonempty (PF _ p) PE)) <- tpsfocus F PL PL' PF. %worlds () (tpsfocus _ _ _ _). %total F (tpsfocus F _ _ _). % Now, the full preservation. It is only one rule now, regardless % of evaluation and typing rules. tps : eval E E' -> of E T -> of E' T -> type. %mode tps +R +P -Q. - : tps (eval1 PR PF) PTE (PF' _ PTR') <- tpsfocus PF PTE PTR PF' <- tpsrdx PR PTR PTR'. %worlds () (tps D P _). %total D (tps D P _). % ---------------------------------------------------------------------- % Proving progress: a well-typed expression is either a value, % or can be reduced. % If a preval has a type, it is a redex. % This is the only interesting rule. typed-preval : pre-val E -> of E T -> rdx E E' -> type. %mode typed-preval +PPV +PT -R. - : typed-preval (preval-app PV1 PV2) (tp_app _ _) (rdx-app PV2). - : typed-preval (preval-tapp T PV) (tp_tapp _) (rdx-tapp T). - : typed-preval (preval-head (val_nonempty (val_cons PVL PVE))) (tp_head (tp_nonempty _ _)) (rdx-head PVL PVE). - : typed-preval (preval-tail (val_nonempty (val_cons PVL PVE))) (tp_tail (tp_nonempty _ _)) (rdx-tail PVL PVE). - : typed-preval (preval-indeed (val_nil)) (tp_indeed _ _ _) (rdx-indeed-nil). - : typed-preval (preval-indeed (val_cons PVL PVE)) (tp_indeed _ _ _) (rdx-indeed-cons PVL PVE). %worlds () (typed-preval _ _ _). %total {} (typed-preval _ _ _). % If a focusable expression has a type, it can make progress. % This rule has only one clause and it is generic over the number % of evaluation/typing rules. fprog : focus (_ : pre-val ER) C -> of (C ER) T -> eval (C ER) E' -> type. %mode fprog +F +P -D. - : fprog (PF : focus PPV _) PT (eval1 R PF) <- tpsfocus PF PT PTPV _ <- typed-preval PPV PTPV R. %worlds () (fprog _ _ _). %total {} (fprog _ _ _). % The final straw: any typed expression is either a value or can % make progress. progress : exp -> type. % The sum type. progress-val : val E -> progress E. progress-eval : eval E E' -> progress E. % Aux lemma tprog-vf : {E:exp} val-or-focus E -> of E T -> progress E -> type. %mode tprog-vf +E +VF +T -G. - : tprog-vf _ (val-or-focus-val PV) _ (progress-val PV). - : tprog-vf _ (val-or-focus-focus PF) T (progress-eval D) <- fprog PF T D. %worlds () (tprog-vf _ _ _ _). %total VF (tprog-vf VF _ _ _). tprog : {E:exp} of E T -> progress E -> type. %mode tprog +E +T -G. - : tprog E T G <- val-focus-disj E VF <- tprog-vf E VF T G. %worlds () (tprog _ _ _). %total {} (tprog _ _ _). % And it accepts the totality declaration. We have the progress proof!