THEOREM[expression termination] If C1 = {};{};P;L and |- C1 and C1 |- e1:t then all sequences of reduction steps e1-->e2-->e3-->... terminate at some en=vn Proof: The language Fwn is defined below. Fwn is, roughly, a subset of the calculus of inductive constructions (i.e. by lemma[expression type translation 2] every well-typed Fwn program is a well-typed CIC program, by lemma[expression simulation 2], every reduction in Fwn corresponds to a reduction in CIC), and therefore all well-typed Fwn programs terminate. (See Shao et al, "A Type System for Certified Binaries (Extended Version)", for a concise definition of a variant of CIC, including definitions of natural numbers, and a proof of strong normalization.) Let Ck = {};{};P;L. By preservation, |- Ck and Ck |- ek:t. Let C1 |- e1:t~~> ~e1 and {} |- t:type~~> ~t (see definitions below). By lemma[expression type translation 1], {};{} |- ~e1:~t. Suppose e1 takes an infinite sequence of steps. Then we can show that e1' also takes an infinite number of steps, which contradicts Fwn's termination: For each step that ek-->ek+1, lemma[expression simulation 1] shows that ~ek steps to ~(ek+1) in one or more steps. Therefore, an infinite sequence of steps starting from e1 implies an infinite sequence of Fwn steps starting from ~e1. Therefore, e1 can take only a finite number of steps to some en, which can step no further. By progress, en must be a value vn. THEOREM[coercion termination] If C1 = {};{};P;L and |- C1 and C1 |- c1:t then all sequences of reduction steps c1-->c2-->c3-->... terminate at some en=vn Proof by induction on structure of c1. Case c1 = e: follows directly from theorem[expression termination]. Case c1 = #c: By inversion, c has type %t for some t. By induction, c reaches a value v in zero or more steps. By preservation, v has type %t. By canonical forms, v = %e. Therefore, #c -->* #v and #v = #%e and #%e --> e. By theorem[expression termination], e terminates at some value. The lemmas below make frequent use of lemma[type equivalence kinds] and lemma[expression kinds]. ==================================================================== LEMMA[expression type translation 1] (1) If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' then D' |- t':~k (2) If C = D;G;P;L and |- C ~~> D';G' and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and |- t1=t2 then |- t1'=t2' (3) If C = D;G;P;L and |- C ~~> D';G' then D' |- G' (4) If C = D;G;P;L and |- C ~~> D';G' and D |- ta:k ~~> ta' and |- pat:ta => D'';G'' ; e':tb' ::> e'' and |- C D'';G'' ~~> D''';G''' and D''';G''' |- e':tb' then D';G' |- e'':ta'->tb' (5) If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' and C |- e:t ~~> e' then D';G' |- e':t' Define the target language "Fwn" for the translation ~~> as follows: D = {A->k} G = {x->t} C=D;G k = k->k | type | nat t = t -> t | 0 | s(t) | elim k t t t | A:k | all A:k.t | \A:k.t | t t e = x | \x:t.e | e e | induction t t e e | \A:k.e | e t D |- t1:type D |- t2:type ---------------- D |- t1 -> t2:type D |- 0:nat D |- t:nat ------------- D |- s(t):nat D |- tn:nat D |- tz:k D |- ts:nat->k->k ---------------------- D |- elim k tn tz ts:k D,A:k |- (A:k):k D,A:k |- t:type ------------------- D |- all A:k.t : type D,A:ka |- t:kb --------------------- D |- \A:ka.t : ka->kb D |- tf:ka->kb D |- ta:ka -------------- D |- tf ta:kb |- t = t |- t1 = t2 ---------- |- t2 = t1 |- t1 = t2 |- t2 = t3 ---------- |- t1 = t3 |- (\A:k.tb) ta = [A<-ta]tb |- elim k 0 tz ts = tz |- elim k s(tm) tz ts = ts tm (elim k tm tz ts) |- t1 = t1' ----------------- |- T[t1] = T[t1'] |- t1 = t1' |- t2 = t2' ------------------------ |- T[t1,t2] = T[t1',t2'] |- t1 = t1' |- t2 = t2' |- t3 = t3' -------------------------------- |- T[t1,t2,t3'] = T[t1',t2',t3'] T[t1] = s(t1) | all A:k.t1 | \A:k.t1 T[t1,t2] = t1 -> t2 | t1 t2 T[t1,t2,t3] = elim k t1 t2 t3 C,x:t |- x:t C,xa:ta |- e:tb C |- tb:type ----------------------- C |- \x:ta.e : ta -> tb C |- ef:ta -> tb C |- ea:ta ------------- C |- ef ea:tb C |- tn:nat C |- tF:nat->type C |- e0:tF 0 C |- es:all A:nat.tF A -> tF s(A) --------------------------------- C |- induction tn tF e0 es: tF A C,A:k |- e:t ----------------------- C |- \A:k.e : all A:k.t C |- e : all A:k.t' C |- t:k ------------------- C |- e t : t' C |- e:t C |- t = t' ----------- C |- e:t' forall x->t in G, D |- t:type ----------------------------- D |- G (\x:t.eb) ea --> [x<-ea]eb |- tn = 0 ---------------------------- induction tn tf e0 es --> e0 |- tn = s(tm) --------------------------------------------------------- induction tn tf e0 !es --> es tm (induction tm tf e0 !es) (\A:k.e) t --> [A<-t]e E[e1] = \x:t.e1 | \A:k.e1 | e1 t | e1 e | e1,e | induction t t e1 e | e e1 | e,e1 | induction t t e e1 e-->e' ------------ E[e]-->E[e'] Define the translations ~~> as follows (using the abbreviations ~e = e' for C |- e:t ~~> e' and ~t = t' for C |- t:k ~~> t' where the surrounding judgments aren't immediately necessary) Define the abbreviations True = all A:type.A->A and true = \A:type.\x:A.x ~(k1->k2) = ~k1->~k2 ~nat = nat ~reg = type ~type = type ~(!t) = t ~(t1 -o t2) = ~t1->~t2 ~(t1*t2) = all A:type.(~t1->~t2->(A:type))->(A:type) ~0 = 0 ~s(t) = s(~t) ~(all A:k.t) = all A:~k.~t ~(exists A:k.t) = all B:type.(all A:~k.~t->(B:type))->(B:type) ~(\A:k.t) = \A:~k.~t ~(t1 t2) = ~t1 ~t2 ~r = True ~(Reg t t) = True ~(Mem t t) = True ~(Code t t) = True D,A:k |- A:k ~~> A:k D |- tn:nat ~~> ~tn D |- tz:k ~~> ~tz D |- ts:nat->k->k ~~> ~ts -------------------- D |- elim tn tz ts:k ~~> elim ~k ~tn ~tz ~ts D |- t:k->k ------------------- D |- rec t:k ~~> `k D |- t:k ---------------- D |- %t:k ~~> `k `(k1->k2) = \A:~k1.`k2 `nat = True `reg = True `type = True |- x:t => {};{x:t} ; e:tb ::> \x:~t.e |- !x:!t => {};{!x:t} ; e:tb ::> \x:~t.e |- pat:t => D;G ; e:tb ::> e' -------------------- |- !(pat):!t => D;G ; e:tb ::> e' |- pat:t => D;G ; e:tb ::> e' -------------------------------- |- A,pat:exists A:k.t => D,A:k;G ; e:tb ::> \x:~(exists A:k.t).x tb (\A:~k.e') |- pat1:t1 => D1;G1 ; e':~t2->tb ::> e'' |- pat2:t2 => D2;G2 ; e:tb ::> e' --------------------------------- |- pat1,pat2:t1*t2 => D1 D2;G1 G2 ; e ::> \x:~(t1*t2).x tb e'' |- pat:ta => D;G ; e' ::> e'' C D;G |- e:tb ~~> e' C |- ta -o tb : type ------------------------- C |- \pat:ta.e : ta -o tb ~~> e'' C |- e1:t1 ~~> e1' |- pat:t1 => D;G ; e2' ::> e'' C D;G |- e2:t2 ~~> e2' C |- t2:type -------------------------- C |- let pat = e1 in e2:t2 ~~> e'' e1' C1 |- e1:t1 ~~> e1' C2 |- e2:t2 ~~> e2' -------------------- C1,C2 |- e1,e2:t1*t2 ~~> \A:type.\x:(~t1->~t2->(A:type)).x e1' e2' C |- t1:k ~~> t1' C |- e:[A<-t1]t2 ~~> e' ------------------------------- C |- pack t1,e as exists A:k.t2 ~~> \B:type.\x:(all A:~k.~t2->(B:type)).x t1' e' C |- e:t ~~> e' C |- t = t' ----------- C |- e:t' ~~> e' ~x = x ~(!e) = ~e ~(e1 e2) = ~e1 ~e2 ~(induction t1 t2 e1 e2) = induction ~t1 ~t2 ~e1 ~e2 ~(\A:k.e) = \A:~k.~e ~(e t) = ~e ~t ~(%e) = true ~(e1 %<< e2) = (\_:True.~e2) ~e1 ~fact = true ~(code(n)[t...t]) = true LEMMA (1) If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' then D' |- t':~k Induction on D |- t:k. Also use following lemma: lemma: In any D, D |- `k:~k. proof: easy induction on k. CASE D |- t:k ---------------- D |- %t:k ~~> `k By lemma, D' |- `k:~k. CASE D,A:ka |- t:kb ~~> ~t --------------------- D |- \A:ka.t : ka->kb ~~> \A:~ka.~t By induction, D',A:~ka |- ~t:~kb By rule, D' |- (\A:~ka.~t):~ka->~kb ~ka->~kb = ~(ka->kb) OTHER CASES SIMILAR LEMMA (2) If C = D;G;P;L and |- C ~~> D';G' and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and |- t1=t2 then |- t1'=t2' Induction on |- t1=t2 EASY CASES |- t = t |- t1 = t2 ---------- |- t2 = t1 |- t1 = t2 |- t2 = t3 ---------- |- t1 = t3 CASE |- (\A:k.tb) ta = [A<-ta]tb (\A:~k.~tb) ~ta = [A<-~ta]~tb ~((\A:k.tb) ta) = ~([A<-ta]tb) where ~([A<-ta]tb) = [A<-~ta]~tb by induction on derivation of ~tb CASES |- elim 0 tz ts = tz |- elim s(tm) tz ts = ts tm (elim tm tz ts) ~(elim 0 tz ts) = elim ~k 0 ~tz ~ts = ~tz ~(elim s(tm) tz ts) = elim ~k s(~tm) ~tz ~ts = ~ts ~tm (elim ~k ~tm ~tz ~ts) = ~(ts tm (elim tm tz ts)) CASE |- rec t = %(t (rec t)) These are the only possible derivations of ~~> for rec t and %(t (rec t)): D |- t:k->k ------------------- D |- rec t:k ~~> `k D |- t:k->k ------------ D |- t:k->k D |- rec t:k ----------------------------- D |- t (rec t):k -------------------------- D |- %(t (rec t)):k ~~> `k Because the kinding rules are syntax directed, there is only one possible derivation of D |- t:..., so both `k must refer to the same k, so the case is proven by: |- `k = `k CASE |- (%t1) t2 = %(t1 t2) Only possible derivations: D |- t1:ka->kb --------------- D |- %t1:ka->kb ~~> `(ka->kb) D |- t2:ka ~~> ~t2 ------------------------------------------- D |- (%t1) t2:kb ~~> `(ka->kb) ~t2 D |- t1:ka->kb D |- t2:ka ---------------------------- D |- t1 t2:kb ---------------- D |- %(t1 t2):kb ~~> `kb `(ka->kb) ~t2 = (\A:~ka.`kb) ~t2 = `kb CONGRUENCE CASES easy LEMMA (3) If C = D;G;P;L and |- C ~~> D';G' then D' |- G' |- C implies forall x->t and !x->t in G, D |- t:type. By lemma(1), forall x->t and !x->t in G, D' |- ~t:type. LEMMA (4) If C = D;G;P;L and |- C ~~> D';G' and D |- ta:k ~~> ta' and |- pat:ta => D'';G'' ; e':tb' ::> e'' and |- C D'';G'' ~~> D''';G''' and D''';G''' |- e':tb' then D';G' |- e'':ta'->tb' CASE |- x:ta => {x:ta} ; e':tb' ::> \x:~ta.e' D'' = {}, so D''' = D' G'' = {x:ta}, so G''' = G',x:~ta D''';G''' |- e':tb' D';G',x:ta' |- e':tb' ------------------------------- D';G' |- \x:ta'.e':ta'->tb' CASE |- pat:t => D'';G'' ; e':tb' ::> e'' ------------------------------------ |- A,pat:exists A:k.t => D'',A:k;G''; e':tb' ::> \x:~(exists A:k.t).x tb' (\A:~k.e'') |- C,A:k ~~> D',A:~k;G' D,A:k |- t:k ~~> t' |- pat:t => D'';G'' ; e':tb' ::> e'' C'' = C D'',A:k;G'' |- C'' ~~> D''';G''' D''' |- e':tb' By induction, D',A:~k;G' |- e'':t'->tb' D';G' |- (\A:~k.e''):all A:~k.t'->tb' D';G',x:~(exists A:k.t) |- x tb' (\A:~k.e''):tb' since ~(exists A:k.t) = all B:type.(all A:~k.~t->(B:type))->(B:type) D';G' |- \x:~(exists A:k.t).x (\A:~k.e'') : ta'->tb' LEMMA (5) If C = D;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' and C |- e:t ~~> e' then D';G' |- e':t' By induction on C |- e:t ~~> e'. CASE |- pat:ta => D'';G'' ; e' ::> e'' C'' = C D'';G'' C'' |- e:tb ~~> e' C |- ta -o tb:type ------------------------- C |- \pat:ta.e : ta -o tb ~~> e'' |- C ~~> D';G' D |- (ta -o tb):type ~~> ta'->tb' C |- (\pat:ta.e):(ta -o tb) ~~> e'' C'' = D'';G'';P;L |- C'' ~~> D''';G''' By weakening, D'' |- tb:type ~~> tb' // Yuck C'' |- e:tb ~~> e' By induction, D''';G''' |- e':tb' By lemma(4), then D';G' |- e'':ta'->tb' CASE C |- e:t1 ~~> e' C |- t1 = t2 ----------- C |- e:t2 ~~> e' D |- t2:k ~~> t2' By induction, D';G' |- e':t1' By lemma 2, |- t1' = t2' By rule, D';G' |- e':t2' CASE C |- e:t ---------- C |- %e:%t ~~> true D |- %t:type ~~> True D';G' |- true:True CASE C1 |- e1:%(ta -o tb) ~~> ~e1 C2 |- e2:%ta ~~> ~e2 ------------------------ C1,C2 |- e1 %<< e2 : %tb ~~> (\_:True.~e2) ~e1 D |- %ta:type ~~> True D |- %(ta -o tb):type ~~> True |- C1 ~~> D';G1' |- C2 ~~> D';G2' G' = G1',G2' By induction, D';G1' |- ~e1:True By induction, D';G2' |- ~e2:True By weakening, D';G' |- ~e1:True By weakening, D';G' |- ~e2:True D';G' |- (\_:True.~e1):True->True D';G' |- (\_:True.~e1) ~e2:True OTHER CASES SIMILAR ==================================================================== LEMMA[expression simulation 1] (1) If |-pat:ta=>D';G';eb:tb::>ef and pat<-ea=>[s] and C |- ea:ta~~>eax then ef eax -->+ [~s]eb (2) If C |- e:t ~~> ex and C |- e':t ~~> ex' and e-->e' then ex -->+ ex' (where -->+ indicates one or more steps) Proof by induction on pat<-ea=>[s] and e-->e'. CASE x<-ea => [x<-ea] |- x:ta => {};{x:ta} ; eb:tb ::> \x:~ta.eb C |- ea:ta~~>eax (\x:~ta.eb) eax --> [x<-eax]eb = [~(x<-ea)]eb CASE pat<-ea' => [s] --------------------------------------- A,pat<-pack ta',ea' as ta => [s][A<-ta'] |- pat:t => D';G' ; eb:tb ::> e' ----------------------------- |- A,pat:exists A:k.t => {A:k}D';G' ; eb:tb ::> \x:~(exists A:k.t).x tb (\A:~k.e') C |- ta':k ~~> ta'' C |- ea':[A<-ta']t ~~> ea'' --------------------------------- C |- pack ta',ea' as exists A:k.t ~~> \B:type.\x:(all A:~k.~t->B).x ta'' ea'' |- pat:t => D';G' ; eb:tb ::> e' |- pat:[A<-ta']t => D';[A<-ta']G' ; [A<-ta'']eb:tb ::> [A<-ta'']e' (easy induction) pat<-ea' => [s] C |- ea':[A<-ta']t ~~> ea'' By induction, ([A<-ta'']e') ea'' -->+ [~s][A<-ta'']eb (\x:~(exists A:k.t).x tb (\A:~k.e')) (\B:type.\x:(all A:~k.~t->B).x ta'' ea'') --> (\B:type.\x:(all A:~k.~t->B).x ta'' ea'') tb (\A:~k.e') --> (\x:(all A:~k.~t->tb).x ta'' ea'') (\A:~k.e') --> (\A:~k.e') ta'' ea'' --> ([A<-ta'']e') ea'' -->+ [~s][A<-ta'']eb = [~s][~(A<-ta')]eb CASE pat<-ea => [s] ------------------------ (\pat:ta.eb) ea --> [s]eb |- pat:ta => D';G' ; e' ::> e'' C' |- eb:tb ~~> e' C |- ta -o tb : type ------------------------- C |- \pat:ta.eb : ta -o tb ~~> e'' C |- (\pat:ta.eb) ea:t ~~> e'' ~ea C |- [s]eb:t ~~> [~s]e' By lemma(1), e'' ~ea -->+ [~s]e' CASE %ef %<< %ea --> %(ef ea) C1 |- %ef:%(ta -o tb) ~~> ~%ef C2 |- %ea:%ta ~~> ~%ea ------------------------ C1,C2 |- %ef %<< %ea : %tb ~~> (\_:True.~%ea) ~%ef ~%ea = true (by inversion) ~(%(ef ea)) = true (\_:True.~%ea) ~%ef --> ~%ea = true OTHER CASES SIMILAR ==================================================================== LEMMA[expression type translation 2] Target language ("TL", Shao et al's variant of CIC, omitting "Ext"): s = Kind | Kscm X = x | A D = {} | {},X:t t = s | X | \X:t.t | t t | #X:t.t | Ind(X:Kind){...t...} | Ctor(i,t) | Elim[t,t](t){...t...} abbreviation: (t1->t2) = (#x:t1.t2) where x is not free in t2 abbreviation: (t1=>t2) = (#A:t1.t2) where A is not free in t2 abbreviation: nat = Ind(A:Kind){A;A->A} abbreviation: 0 = Ctor(1,nat) abbreviation: s(t) = Ctor(2,nat) t note that nat's constructors are "small" ("small(A)" and "small(A->A)") note that |- nat:Kind S(k1->k2) = S(k2) S(type) = Kscm S(nat) = Kind K(k1->k2) = K(k1)=>K(k2) where S(k1) = Kscm K(k1->k2) = K(k1)->K(k2) where S(k1) = Kind K(type) = Kind K(nat) = nat For each type variable "A", define a corresponding object variable "xA". X(A,Kind) = xA X(A,Kscm) = A T(t1->t2) = T(t1)->T(t2) T(0) = 0 T(s(t)) = s(T(t)) T(elim k tn tz ts) = Elim[nat,K(k)](T(tn)){T(tz);T(ts)} where S(k)=Kscm T(elim k tn tz ts) = Elim[nat,\_:nat.K(k)](T(tn)){T(tz);T(ts)} where S(k)=Kind T(A:k) = X(A,S(k)) T(\A:k.t) = \X(A,S(k)):K(k).T(t) T(all A:k.t) = #X(A,S(k)):K(k).T(t) T(t1 t2) = T(t1) T(t2) E(x) = x E(\x:t.e) = \x:T(t).E(e) E(e1 e2) = E(e1) E(e2) E(induction tf tn ez es) = Elim[nat,T(tf)](T(tn)){E(ez);E(es)} E(\A:k.e) = \A:K(k).E(e) E(e t) = E(e) T(t) D(...A->k...} = ...X(A,S(k)):K(k)... G(...x->t...} = ...x:T(t)... Lemma: |- K(k):S(k) By induction on k. (Straightforward, since |- nat:Kind and |- Kind:Kscm and the rules assign #X:t1.t2 sort s2 if t2 has sort s2.) Lemma: If |- t1:t2 then D(D) |- t1:t2 By induction on D. Lemma: If D |- t:k then D(D) |- T(t):K(k) By induction on derivation of D |- t:k. CASE D,A:ka |- t:kb --------------------- D |- \A:ka.t : ka->kb where S(ka)=S(kb)=Kind By induction, D(D),X(A,S(ka)):K(ka) |- T(t):K(kb) So D(D),xA:K(ka) |- T(T):K(kb) By lemma, |- K(ka->kb) : S(ka->kb) So |- K(ka)->K(kb) : Kind So |- #xA:K(ka).K(kb) : Kind (since xA not free in K(kb)) By lemma, D(D) |- #xA:K(ka).K(kb) : Kind D(D),xA:K(ka) |- T(t) : K(kb) D(D) |- #xA:K(ka).K(kb) : Kind --------------------------------------------------------- D(D),xA:K(ka) |- \X(A,S(ka)):K(ka).T(t) : #xA:K(ka).K(kb) OTHER CASES SIMILAR Lemma: If D |- G and D;G |- e:t then D(D),G(G) |- E(e):T(t) By induction on derivation of D;G |- e:t. LEMMA[expression simulation 2] If C |- e:t ~~> tx and C |- e':t ~~> tx' and e-->e' then tx -->+ tx' by beta-eta-iota reduction. (where -->+ indicates one or more steps) By induction on e-->e'. The application rules are trivial, but note that the rules for "induction", such as: |- tn = 0 ---------------------------- induction tn tf e0 es --> e0 take a single step in the source language, but it may take multiple steps in the target language for tn to reduce to 0. By confluence, there is a sequence of steps tn=>tn'=>tn''=>...=>0, and this sequence translates into a sequence ~tn -->* ~tn' -->* ... -->* 0 in the target language, where -->* indicates zero or more steps.