THEOREM[expression termination] If C1 = {};U1;R1;{};P;L and |- C1 and C1 |- e1:t then all sequences of reduction steps U1;R1;e1-->U2;R2;e2-->U3;R3;e3-->... terminate at some Un;Rn;vn Proof: The language Fwn is defined below. Fwn is a subset of the calculus of inductive constructions (i.e. every well-typed Fwn program is a well-typed CIC program, and every reduction rule in Fwn is 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 = {};Uk;Rk;{};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 U1;R1;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 Uk;Rk;ek-->Uk+1;Rk+1;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 U1;R1;e1 implies an infinite sequence of Fwn steps starting from ~e1. Therefore, U1;R1;e1 can take only a finite number of steps to some Un;Rn;en, which can step no further. By progress, en must be a value vn. THEOREM[coercion termination] If C1 = {};U1;R1;{};P;L and |- C1 and C1 |- c1:t then all sequences of reduction steps U1;R1;c1-->U2;R2;c2-->U3;R3;c3-->... terminate at some Un;Rn;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;U;R;G;P;L and |- C ~~> D';G' and D |- t:k ~~> t' then D' |- t':~k (2) If C = D;U;R;G;P;L and |- C ~~> D';G' and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and R |- t1=t2 then |- t1'=t2' (3) If C = D;U;R;G;P;L and |- C ~~> D';G' then D' |- G' (4) If C = D;U;R;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;U;R;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) | if0 t t t | A | 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 ------------------- D |- if0 tn tz ts:k D,A:k |- A: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 R |- t1 = t1' ------------------- R |- T[t1] = T[t1'] R |- t1 = t1' R |- t2 = t2' -------------------------- R |- T[t1,t2] = T[t1',t2'] R |- t1 = t1' R |- t2 = t2' R |- t3 = t3' ----------------------------------- R |- 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] = if0 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' 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)->A ~0 = 0 ~s(t) = s(~t) ~(if0 t1 t2 t3) = if0 ~t1 ~t2 ~t3 ~A = A ~(all A:k.t) = all A:~k.~t ~(exists A:k.t) = all B:type.(all A:~k.~t->B)->B ~(\A:k.t) = \A:~k.~t ~(t1 t2) = ~t1 ~t2 ~(Delay t) = True ~q_k = `k ~r = True ~(Reg t t) = True ~(Mem t t) = True ~(Code t t) = True D |- t:k --------------------- D |- type(t):k ~~> `k D |- t:k ------------------- D |- pf(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 |- 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).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).x t1' e' C |- e:t ~~> e' C |- t = t' ----------- C |- e:t' ~~> e' C1 |- e1:%ta ~~> e1' C2 |- e2:ta -o tb ~~> e2' ------------------------ C1,C2 |- e1 >>@ e2 : %tb ~~> (\_:~ta->~tb.e1') e2' ~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 ~(delay k) = (\_:True.true) true ~(commit[t=type(t)] e) = (\_:True.true) ~e ~(%e) = true ~(e1 >>* e2) = (\_:True.~e2) ~e1 ~fact = true ~(code(n)[t...t]) = true LEMMA (1) If C = D;U;R;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 |- type(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;U;R;G;P;L and |- C ~~> D';G' and D |- t1:k ~~> t1' and D |- t2:k ~~> t2' and R |- t1=t2 then |- t1'=t2' Induction on R |- t1=t2 EASY CASES R |- t = t R |- t1 = t2 ------------ R |- t2 = t1 R |- t1 = t2 R |- t2 = t3 ------------ R |- t1 = t3 CASE R |- (\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 R |- if0 0 tz ts = tz R |- if0 s(tm) tz ts = ts tm ~(if0 0 tz ts) = if0 0 ~tz ~ts = ~tz ~(if0 s(tm) tz ts) = if0 s(~tm) ~tz ~ts = ~ts ~tm = ~(ts tm) CASE R,q_k->t |- type(q_k) = type(t) D |- type(q_k):k D |- type(t):k ~type(q_k) = `k ~type(t) = `k CASE R |- (type(t1)) t2 = type(t1 t2) D |- (type(t1)):ka->kb D |- t2:ka -------------- D |- (type(t1)) t2:kb D |- type(t1 t2):kb ~(type(t1) t2) = ~type(t1) ~t2 = `(ka->kb) ~t2 = (\A:~ka.`kb) ~t2 = `kb ~type(t1 t2) = `kb CASE R |- (pf(t1)) t2 = pf(t1 t2) see previous case CONGRUENCE CASES easy LEMMA (3) If C = D;U;R;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;U;R;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)->B D';G' |- \x:~(exists A:k.t).x (\A:~k.e'') : ta'->tb' LEMMA (5) If C = D;U;R;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 |- 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'';U;R;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 ~~> e1' C2 |- e2:ta -o tb ~~> e2' ------------------------ C1,C2 |- e1 >>@ e2 : %tb ~~> (\_:~ta->~tb.e1') e2' D |- %ta:type ~~> True D |- (ta -o tb):type ~~> ta'->tb' |- C1 ~~> D';G1' |- C2 ~~> D';G2' G' = G1',G2' By induction, D';G1' |- e1':True By induction, D';G2' |- e2':ta'->tb' By weakening, D';G' |- e1':True By weakening, D';G' |- e2':ta'->tb' D';G' |- (\_:~ta->~tb.e1'):(ta'->tb')->True D';G' |- (\_:~ta->~tb.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' (3) If C |- e:t ~~> ex and C |- e':t ~~> ex' and U;R;e-->U';R';e' then ex -->+ ex' (where -->+ indicates one or more steps) Proof by induction on pat<-ea=>[s] and e-->e' and U;R;e-->U';R';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 |- 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 e-->e' ------------------ (U;R;e)-->(U;R;e') By induction, ex -->+ ex' CASE (U;R; %ea >>@ vf) --> (U;R; %(vf ea)) C1 |- %ea:%ta ~~> e1' C2 |- vf:ta -o tb ~~> e2' ------------------------ C1,C2 |- %ea >>@ vf : %tb ~~> (\_:~ta->~tb.e1') e2' e1' = true (by inversion) ~(%(vf ea)) = true (\_:~ta->~tb.e1') e2' --> e1' = true CASE (U;R; delay k) --> (U,q_k;R; %pack q_k,fact as exists A:k.Delay type(A)) where q_k is fresh ~(delay k) = (\_:True.true) true --> true = ~(%pack q_k,fact as exists A:k.Delay type(A)) CASE R |- t=type(q_k) ----------------------------------------------------------------------------------- (U,q_k;R; commit[t=type(t')] fact) --> (U;R,q_k->t'; %!\F:k->type.\x:F type(q_k).x) ~(commit[t=type(t')] e) = (\_:True.true) ~e --> true = ~(%!\F:k->type.\x:F q_k.x) OTHER CASES SIMILAR