THEOREM[preservation] If C = D;U;R;G;P;L and |- C and C |- prog and (U;R;L;prog) --> (U';R';L';prog') then |- C' and C' |- prog' where C' = D;U';R';G;P;L' Follows from: (1) If |- C and C |- e:t and e --> e' then C |- e':t (2) If C = D;Up;R;G;P;L and |- C,Us and C |- e:t and Us,Up;R;e --> U';R';e' then |- C',Us and C' |- e':t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' (3) If C = D;Up;R;G;P;L and |- C,Us and C |- c:t and Us,Up;R;c --> U';R';c' then |- C',Us and C' |- c':t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' (4) If C = D;Up;R;G;P;Lp and |- C,Us,Ls and C |- prog and Us,Up;R;Ls,Lp;prog --> U';R';L';prog' then |- C',Us,Ls and C' |- prog' where C' = D;Up';R';G;P;Lp' and U'=Us,Up' and L'=Ls,Lp' and R' = R R'' for some R'' and Up' and Lp' Proof by induction on the typing derivation. See below. THEOREM[progress] If C = {};U;R;{};P;L and |- C and C |- prog then there is some U';R';L';prog' such that U;R;L;prog --> U';R';L';prog' Follows from: (1) If C = {};U;R;{};P;L and |- C and C |- e:t and e is not a value and there is no t' such that C |- t = %t' then there is some e' such that e --> e' (2) If C = {};Up;R;{};P;L and |- C,Us and C |- e:t and e is not a value then there is some Up';R';e' such that Us,Up;R;e --> Us,Up';R';e' (3) If C = {};Up;R;{};P;L and |- C,Us and C |- c:t and c is not a value then there is some Up';R';c' such that Us,Up;R;c --> Us,Up';R';c' (4) If C = {};Up;R;{};P;Lp and |- C,Us,Ls and C |- prog then there is some U';R';L';prog' such that Us,Up;R;Ls,Lp;prog --> Us,Up';R';Ls,Lp';prog' Proof by induction on the typing derivation. See below. LEMMA[typing inversion] If C |- e:t than a rule other than C |- e:t1 C |- t1 = t2 ------------ C |- e:t2 concludes C |- e:t', where C |- t=t' Proof by induction on C |- e:t, where any derivation not rooted at the t1=t2 rule above is a base case. (The only induction case is the t1=t2 rule above.) LEMMA[type weakening] If D |- t:k and D'=D,A:k then D' |- t:k Proof by induction on D |- t:k LEMMA[type equivalence weakening] If R |- t1=t2 and R'=R,q_k->t then R' |- t1=t2 Proof by induction on R |- t1=t2 LEMMA[expression weakening] If C = D;U;R;G;P;L and C'=D,A:k;U;R;G;P;L or C'=D;U;R,q_k->t;G;P;L or C'=D;U;R;G,!x->t;P;L then (1) If C |- e:t then C' |- e:t (2) If C |- c:t then C' |- c:t (3a) If (C);(Cb) |- ins:t then (C');(Cb) |- ins:t (3b) If (Ca);(C) |- ins:t then (Ca);(C') |- ins:t (4) If C |- blk then C' |- blk (5) If C |- n->b:t then C' |- n->b:t (6) If C' = D';U;R';G;{};L and C |- prog then C' |- prog Proof by inductions on typing derivations. LEMMA[single-step type confluence] If R |- ta => tb and R |- ta => tc then there is a td s.t. R |- tb=>td and R |- tc => td Proof by induction on sum of sizes of derivations of R |- ta => tb and R |- ta => tc. Label the => rules as follows: R |- t =1> t R |- tj => tj' ... R |- tk => tk' --------------------------------- R |- T[t1...tk] =2> T[t1'...tk'] R |- (\A:k.tb) ta =3> [A<-ta]tb R,q_k->t |- type(q_k) =4> type(t) R |- (type(t1)) t2 =5> type(t1 t2) R |- (pf(t1)) t2 =6> pf(t1 t2) For brevity, the cases below elide the "R |- ". The following x,y produce syntactically legal ta =x> tb and ta =y> tc: x,x 1,y x,1 2,y x,2 CASE 1,y: ta=tb, so choose td=tc CASE x,1: ta=tc, so choose td=tb CASE 2,2: T[ta1...tak] => T[tb1...tbk] T[ta1...tak] => T[tc1...tck] By induction, tb1=>td1...tbk=>tdk and tc1=>td1...tck=>tdk By rule =2>: T[tb1...tbk] => T[td1...tdk] T[tc1...tck] => T[td1...tdk] CASE x,x for x=3,4,5,6: tb=tc, so choose td=tb=tc CASE 2,3: (\A:k.ta') ta'' => (\A:k.tb') tb'' where ta'=>tb' and ta''=>tb'' (\A:k.ta') ta'' => [A<-ta'']ta' Choose td = [A<-tb'']tb' CASE 2,4: type(qa) => type(qb) where qa => qb R,qa->t |- type(qa) => type(t) The only => rule for qa=>qb is qa=>qa, so qb=qa Choose td = type(t) CASE 2,5: (type(ta1)) ta2 => type(ta1 ta2) Similar to case 2,6. CASE 2,6: (pf(ta1)) ta2 => (pf(tb1)) tb2 where ta1=>tb1 and ta2=>tb2 (pf(ta1)) ta2 => pf(ta1 ta2) Choose td = pf(tb1 tb2) CASES 3,2 and 4,2 and 5,2 and 6,2: see cases 2,3 and 2,4 and 2,5 and 2,6 LEMMA[type confluence] Define t0 =>* tn to mean t0=>t1=>t2=>t3...=>tn, where n>=0. If R |- tb = tc then there is a td s.t. R |- tb =>* td and R |- tc =>* td Proof by single-step type confluence using standard tiling argument. (e.g. see Pierce, "Types and Programming Languages") LEMMA[single-step type equivalence inversion] If R |- S[t1...tn] => t' then t' = S[t1'...tn'] where R |- t1=>t1' ... R |- tn=>tn' and: S[t1] = !t1 | s(t1) | all A:k.t1 | exists A:k.t1 | \A:k.t1 | Delay t1 | %t1 S[t1,t2] = t1 -o t2 | t1*t2 | Reg t1 t2 | Mem t1 t2 | Code t1 t2 (S is the same as T, but excludes (if0 t1 t2 t3) and (t1 t2) and type(t1) and pf(t1), and includes %t1) Proof by cases of definition of => (no induction). For example: R |- t1 => t1' ---------------------- R |- pf(t1) => pf(t1') ---------------------------------- R |- type(pf(t1)) => type(pf(t1')) (i.e. R |- %t1 => %t1') (no other derivation of type(pf(t1)) => type(pf(t1')) is possible) It's important to observe that these rules are not applicable to S[t1...tn]=>t': R |- (\A:k.tb) ta => [A<-ta]tb R |- if0 0 tz ts => tz R |- if0 s(tm) tz ts => ts tm R,q_k->t |- type(q_k) => type(t) R |- (type(t1)) t2 => type(t1 t2) R |- (pf(t1)) t2 => pf(t1 t2) For example, type(q_k) does not match any S[t1] or S[t1,t2], since type(q_k) does not syntactically match %t=type(pf(t)) for any t. LEMMA[type equivalence inversion] If R |- S[t1...tn] = S'[t1'...tm'] then S = S' and n=m and R |- t1=t1' ... R |- tn=tn' Proof: By lemma[type confluence], then there is some t'' such that R |- S[t1...tn] =>* t'' and R |- S'[t1'...tm'] =>* t'' By induction on number of => steps and single-step type equivalence inversion lemma: - If t = S[t1...tn] and R |- t =>* t'' then t'' = S[t1''...tn''] where R |- t1 =>* t1'' ... R |- tn =>* tn'' - If t' = S'[t1'...tm'] and R |- t' =>* t'' then t'' = S'[t1''...tm''] where R |- t1' =>* t1'' ... R |- tm' =>* tm'' So S=S' and m=n. From R |- tk =>* tk'' conclude R |- tk = tk'' (repeated transitivity) From R |- tk' =>* tk'' conclude R |- tk' = tk'' (repeated transitivity) Thus conclude R |- tk = tk' (symmetry, transitivity). LEMMA[type(q) equivalence inversion] If R |- type(q_k) = type(q_k') and q_k not in domain(R) and q_k' not in domain(R) then q_k=q_k' Proof: By lemma[type confluence], then there is some t'' such that R |- type(q_k) =>* t'' and R |- type(q_k') =>* t'' Consider R |- type(q_k) =>* t''. The rule R,q_k->t |- type(q_k) => type(t) is inapplicable, since q_k,q_k' not in domain(R) The only applicable rule is: R |- q_k => q_k --------------------------- R |- type(q_k) => type(q_k) Therefore, t'' = type(q_k) By the same reasoning, t'' = type(q_k'). So q_k = q_k'. LEMMA[type equivalence kinds] If C = D;U;R;G;P;L and |- C and D |- t1:k and R |- t1=t2 then D |- t2:k Proof by induction on R |- t1=t2. Sample case: R,q_k->t |- type(q_k) = type(t) Kinding rule for q_k says D |- q_k:k. Kinding rule for type(...) says D |- type(q_k):k |- C implies forall q_k->t in R, |- t:k. Kinding rule for type(...) says D |- type(t):k LEMMA[environment typing / expression kinds] (1) If C = D;U;R;G;P;L and |- C and C |- e:t then D |- t:type (2) Suppose C |- e:t by some typing rule with premises ...C' |- e':t'.... Then |- C implies |- C'. Proof by induction on C |- e:t. LEMMA[type substitution] If C,A:ka |- t:k and D |- ta:ka then D |- [A<-ta]t:k Proof by induction on C,A:ka |- t:k. LEMMA[type equivalence substitution] If R |- t1=t2 and (forall q_k->t in R, |- t:k) then R |- [A<-t']t1=[A<-t']t2 Proof by induction on R |- t1=t2. LEMMA[expression type substitution] If C = D;U;R;G;P;L and |- C and C |- ta:ka then (1) If C,A:ka |- eb:tb then D;U;R;[A<-ta]G;P;L |- [A<-ta]eb:[A<-ta]tb (2) If C,A:ka |- cb:tb then D;U;R;[A<-ta]G;P;L |- [A<-ta]cb:[A<-ta]tb (3) If C,A:ka |- blk then D;U;R;[A<-ta]G;P;L |- [A<-ta]blk (4) If C,A:ka |- n->b:tb then D;U;R;[A<-ta]G;P;L |- n->[A<-ta]b:[A<-ta]tb (5) If C,A:ka |- prog then D;U;R;[A<-ta]G;P;L |- [A<-ta]prog Proof by induction on typing derivations for eb,cb,blk,n->b,prog. LEMMA[expression nonlinear substitution] If |- !Ca,Cb and !Ca |- ea:ta then (1) If Cb,!x:ta |- eb:tb then !Ca,Cb |- [x<-ea]eb:tb (2) If Cb,!x:ta |- cb:tb then !Ca,Cb |- [x<-ea]cb:tb (3) If Cb,!x:ta |- blk then !Ca,Cb |- [x<-ea]blk (4) If Cb,!x:ta |- n->b:tb then !Ca,Cb |- n->[x<-ea]b:tb (5) If Cb,!x:ta |- prog and Ca=D;U;R;G;{};L then !Ca,Cb |- [x<-ea]prog Proof by induction on typing derivations for eb,cb,blk,n->b,prog. CASE !C,!x:ta |- x:ta !Ca |- [x<-ea]x:ta By weakening, !Cb,!Ca |- [x<-ea]x:ta CASE !Cb,!x:ta |- e:t ------------------ !Cb,!x:ta |- !e:!t By induction, !Ca,!Cb |- [x<-ea]e:t By rule, !Ca,!Cb |- !([x<-ea]e):!t !([x<-ea]e) = [x<-ea](!e) OTHER CASES SIMILAR LEMMA[expression linear substitution] If |- Ca,Cb and Ca |- ea:ta then (1) If Cb,x:ta |- eb:tb then Ca,Cb |- [x<-ea]eb:tb (2) If Cb,x:ta |- cb:tb then Ca,Cb |- [x<-ea]cb:tb (3) If Cb,x:ta |- blk then Ca,Cb |- [x<-ea]blk (4) If Cb,x:ta |- prog and Ca=D;U;R;G;{};L then Ca,Cb |- [x<-ea]prog Proof by induction on typing derivations for eb,cb,blk,n->b,prog. CASE !Cb,x:ta |- x:ta Ca |- [x<-ea]x:ta By weakening, !Cb,Ca |- [x<-ea]x:ta CASE !Cb,!x:ta |- e:t ------------------ !Cb,!x:ta |- !e:!t Case does not apply, because !x:ta does not match assumption x:ta. OTHER CASES SIMILAR LEMMA[pattern substitution] If |- Ca,Cb and |- pat:ta => D;G and Ca |- ea:ta and pat<-ea => [s] then (1) If Cb D;G |- eb:tb and Ca,Cb |- tb:type then Ca,Cb |- [s]eb:tb (2) If Cb D;G |- cb:tb and Ca,Cb |- tb:type then Ca,Cb |- [s]cb:tb (3) If Cb D;G |- blk then Ca,Cb |- [s]blk (4) If Cb D;G |- n->b:tb and Ca,Cb |- tb:type then Ca,Cb |- n->[s]b:tb (5) If Cb D;G |- prog and Ca=D;U;R;G;{};L then Ca,Cb |- [s]prog By induction on pat. Only eb cases are shown below. CASE pat = x |- x:ta => {};{x:ta} x<-ea => [x<-ea] |- Ca,Cb Ca |- ea:ta Cb,x:ta |- eb:tb By lemma[expression linear substitution], Ca,Cb |- [x<-ea]eb:tb CASE pat = !x |- !x:!ta => {};{!x:ta} !x<-!ea => [x<-ea] Ca |- !ea:!ta By typing inversion and type equivalence inversion: !Ca' |- ea:ta' where !C |- ta=ta' --------------- !Ca' |- !ea:!ta Thus Ca=!Ca' and !Ca' |- ea:ta. |- !Ca',Cb !Ca' |- ea:ta Cb,!x:ta |- eb:tb By lemma[expression nonlinear substitution], Ca,Cb |- [x<-ea]eb:tb CASE pat = A,pat1 Alpha-rename so that A does not appear in Ca,Cb. |- pat1:t' => D;G --------------------------------- |- A,pat1:exists A:k.t' => D,A:k;G pat1<-e1 => [s] ------------------------------------ A,pat1<-pack t,e1 as exists A:k.t'' => [A<-t][s] Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t' By typing inversion: Ca |- t:k Ca |- e1:[A<-t]t'' --------------------------------- Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t'' where Ca |- exists A:k.t' = exists A:k.t'' By type equivalence inversion, Ca |- t' = t'' By type equivalence substitution, Ca |- [A<-t]t' = [A<-t]t'' So Ca |- e1:[A<-t]t' |- pat1:t' => D;G implies |- pat1:[A<-t]t' => D;[A<-t]G (easy induction) We know Cb D,A:k;G |- eb:tb. Substitution implies Cb D;[A<-t]G |- [A<-t]eb:[A<-t]tb. Since Ca,Cb |- tb:type and A does not appear in Ca,Cb, A does not appear free in tb and [A<-t]tb = tb. Therefore we know: |- Ca,Cb and |- pat1:[A<-t]t' => D;[A<-t]G and Ca |- e1:[A<-t]t' and Cb D;[A<-t]G |- [A<-t]eb:tb and Ca,Cb |- tb:type and pat1<-e1 => [s] so by induction: then Ca,Cb |- [s][A<-t]eb:tb CASE pat = pat1,pat2 |- pat1:t1 => D1;G1 |- pat2:t2 => D2;G2 --------------------------------- |- pat1,pat2:t1*t2 => D1 D2;G1 G2 pat1<-e1 => [s1] pat2<-e2 => [s2] --------------------------- pat1,pat2<-e1,e2 => [s1][s2] ta = t1*t2 ea = e1,e2 By typing inversion, type equivalence inversion: C1 |- e1:t1' where C1,C2 |- t1=t1' C2 |- e2:t2' where C1,C2 |- t2=t2' -------------------- C1,C2 |- e1,e2:t1*t2 Thus C1 |- e1:t1 and C2 |- e2:t2 and Ca=C1,C2. Cb D;G = Cb D1 D2;G1 G2 = (Cb D2;G2) D1;G1 By induction, C2,Cb D2;G2 |- [s1]eb:tb By induction, C1,C2,Cb |- [s2][s1]eb:tb OTHER CASES SIMILAR THEOREM[preservation] (1) If |- C and C |- e:t and e --> e' then C |- e':t CASE !C |- e:t ----------- !C |- !e:!t where e-->e' -------- !e-->!e' By induction, !C |- e':t By rule, !C |- !e':!t CASE C |- e:t C |- t = t' ----------- C |- e:t' where e-->e' By induction, C |- e':t By rule, C |- e':t' CASE C1 |- ef:ta -o tb C2 |- ea:ta ----------------- C1,C2 |- ef ea:tb where ea --> ea' ---------------- ef ea --> ef ea' C2 = D;U2;R;G2;P;L2 U=U1,U2 G=G1,G2 L=L1,L2 |- C2 By induction, C2 |- ea':ta By rule, C1,C2 |- ef ea':tb CASE C1 |- ef:ta -o tb C2 |- ea:ta ----------------- C1,C2 |- ef ea:tb where ef=(\pat:ta'.eb) and pat<-ea => [s] -------------------------- (\pat:ta'.eb) ea --> [s]eb By typing inversion and type equality inversion: |- pat:ta' => D;G C1 D;G |- e:tb' C1 |- tb':type ------------------------------ C1 |- (\pat:ta'.eb):ta' -o tb' where C1 |- ta=ta' and C1 |- tb=tb' By rule, C2 |- ea:ta' So we know: |- C1,C2 and |- pat:ta' => D;G and C2 |- ea:ta' and C1 D;G |- e:tb' and C1,C2 |- tb':type and pat<-ea => [s] By pattern substitution, C1,C2 |- [s]e:tb' By rule, C1,C2 |- [s]e:tb OTHER CASES SIMILAR THEOREM[preservation] (2) If C = D;Up;R;G;P;L and |- C,Us and C |- e:t and Us,Up;R;e --> U';R';e' then |- C',Us and C' |- e':t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' CASE C |- e:t C |- t = t' ----------- C |- e:t' where Us,Up;R;e --> U';R';e' By induction, |- C',Us and C' |- e':t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' By weakening, R' |- t = t' By rule, C' |- e':t' CASE Ca |- ea:%ta Cf |- ef:ta -o tb ------------------------ Ca,Cf |- ea >>@ ef : %tb where Us,Up;R;ea --> U';R';ea' -------------------------------------- Us,Up;R;ea >>@ ef --> U';R';ea' >>@ ef Ca = D;Upa;R;Ga;P;La Cf = D;Upf;R;Gf;P;Lf Up=Upa,Upf G=Ga,Gb L=La,Lb Us,Up=(Us,Upf),Upa |- Ca,(Us,Upf) By induction, |- Ca',(Us,Upf) and Ca' |- ea':%ta where Ca' = D;Upa';R';Ga;P;La and U'=(Us,Upf),Upa' and R' = R R'' for some R'' and Upa' Let Cf' = D;Upf;R';Gf;P;Lf By weakening, Cf' |- ef:ta -o tb U'=Us,(Upa',Upf) Let C' = Ca',Cf' = D;Upa',Upf;R';Ga,Gf;P;La,Lf |- C',Us By rule, C' |- ea' >>@ ef : %tb CASE Ca |- %ea:%ta Cf |- vf:ta -o tb ------------------------- Ca,Cf |- %ea >>@ vf : %tb where (U;R; %ea >>@ vf) --> (U;R; %(vf ea)) C=Ca,Cf By typing inversion and type equivalence inversion: Ca |- ea:ta' where Ca |- ta=ta' -------------- Ca |- %ea:%ta' By rule, Ca |- ea:ta Cf |- vf:ta -o tb Ca |- ea:ta ------------------- Ca,Cf |- vf ea : tb ----------------------- Ca,Cf |- %(vf ea) : %tb Let C'=C and R'=R and Up'=Up CASE !C |- delay k: %(exists A:k.Delay type(A)) where (U;R; delay k) --> (U,q_k;R; %pack q_k,fact as exists A:k.Delay type(A)) where q_k is fresh !C=D;{};R;!G;P;{} and |- !C,Us U=Us Let C'=!C,q_k |- C',Us !C,q_k |- fact : Delay type(q_k) !C,q_k |- q_k : k ------------------------------------------------------------------------------ !C,q_k |- pack q_k,fact as exists A:k.Delay type(A) : exists A:k.Delay type(A) ---------------------------------------------------------------------------------- !C,q_k |- %pack q_k,fact as exists A:k.Delay type(A) : %(exists A:k.Delay type(A)) CASE C |- fact:Delay type(q_k) C |- type(q_k):k C |- t':k ---------------------------------------------------------------------------- C |- commit[type(q_k)=type(t')]e:%(!all F:k->type.F type(q_k) -o F type(t')) where 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) C = D;Up;R;G;P;L U,q_k = Us,Up By typing inversion: D;{q_k'};R;!G';P;{} |- fact:Delay type(q_k') where Up={q_k'} and G=!G' and L={} and R |- Delay type(q_k) = Delay type(q_k') By type equivalence inversion, R |- type(q_k) = type(q_k') |- D;U,q_k;R;!G';P;{} implies q_k not in domain(R) |- D;Us,q_k';R;!G';P;{} implies q_k' not in domain(R) By type(q) equivalence inversion, q_k=q_k'. Us = U Let C'=D;{};R,q_k->t';!G';P;{}. |- C',Us C',F:k->type,x:F type(q_k) |- x : F type(q_k) C' |- F type(q_k) = F type(t') --------------------------------------------- C',F:k->type,x:F type(q_k) |- x : F type(t') -------------------------------------------- C',F:k->type |- \x:F type(q_k).x : F type(q_k) -o F type(t') --------------------------------------------------------------------------- C' |- \F:k->type.\x:F type(q_k).x : all F:k->type.F type(q_k) -o F type(t') ----------------------------------------------------------------------------- C' |- !\F:k->type.\x:F type(q_k).x : !all F:k->type.F type(q_k) -o F type(t') --------------------------------------------------------------------------------- C' |- %!\F:k->type.\x:F type(q_k).x : %(!all F:k->type.F type(q_k) -o F type(t')) OTHER CASES SIMILAR THEOREM[preservation] (3) If C = D;Up;R;G;P;L and |- C,Us and C |- c:t and Us,Up;R;c --> U';R';c' then |- C',Us and C' |- c':t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' (note: case c=e handled by (2)) CASE C |- c:%t --------- C |- #c:t where (U;R;c) --> (U';R';c') ------------------------ (U;R;#c) --> (U';R';#c') By induction: then |- C' and C' |- c':%t where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up' By rule, C' |- #c':t CASE C |- %e:%t ----------- C |- #%e:t where (U;R;#%e) --> (U;R;e) By typing inversion: C |- e:t' ----------- C |- %e:%t' where C |- %t=%t' By type equivalence inversion, C |- t=t' By rule, C |- e:t Let C' = C THEOREM[preservation] (4) If C = D;Up;R;G;P;Lp and |- C,Us,Ls and C |- prog and Us,Up;R;Ls,Lp;prog --> U';R';L';prog' then |- C',Us,Ls and C' |- prog' where C' = D;Up';R';G;P;Lp' and U'=Us,Up' and L'=Ls,Lp' and R' = R R'' for some R'' and Up' and Lp' (note: prog = B blk is covered by (6)) CASE prog = (B [c]jmp m) C1 |- c:(Code m t') * t' ------------------------ C1 |- [c]jmp m !C1 |- n1->b1:t1' ... !C1 |- nn->bn:tn' -------------------------------------------- D;Up;R;G;{};Lp |- B [c]jmp m where B = {n1->b1,...,nn->bn} where C1 = D;Up;R;G;{n1->t1',...,nn->tn');Lp where c = (code(n)[t1...tj],v) and U=Us,Up and L=Ls,Lp and: pat<-v => [s] ------------------------------------------------------------------------ B |- U;R;L;[c]jmp m --> U;R;L;[s][Aj<-tj]...[A1<-t1]blk ------------------------------------------------------------------------- (U;R;L;B [c]jmp m) --> U;R;L;B [s][Aj<-tj]...[A1<-t1]blk where bm = \A1:k1...\An:kj.\pat:t.blk Let Up'=Up, Lp'=L, R'=R. C1 |- (code(n)[t1...tj],v):(Code m t') * t' By typing inversion and type equivalence inversion: C1 |- v:t' !C1 |- code(m)[t1...tj]:Code m [Aj<-tj]...[A1<-t1]t'' where !C1 |- t1:k1 ... !C1 |- tj:kj and !C1 |- t' = [A1<-t1,...,An<-tj]t'' and !C1 |- tm' = all A1:k1...all An:kn.Code n t'' !C1 |- m->\A1:k1...\An:kj.\pat:t.blk : tm' By inversion: !C1,A1:k1...An:kj |- m->\pat:t.blk : tm'' where tm' = all A1:k1...all An:kj.tm'' By inversion: |- pat:t => D1;G1 !C1,A1:k1...An:kj D1;G1 |- blk where tm'' = Code m t By substitution: !C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk tm' = all A1:k1...all An:kj.Code m t !C1 |- tm' = all A1:k1...all An:kn.Code n t'' By type equivalence inversion, !C1 |- t = t'' !C1 |- t' = [Aj<-tj]...[A1<-t1]t'' By type equivalence substitution: !C1 |- t' = [Aj<-tj]...[A1<-t1]t |- pat:[Aj<-tj]...[A1<-t1]t => D1;[Aj<-tj]...[A1<-t1]G1 C1 |- v:[Aj<-tj]...[A1<-t1]t pat<-v => [s] !C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk By pattern substitution: C1 |- [s][Aj<-tj]...[A1<-t1]blk D;Up;R;G;{};Lp |- B [s][Aj<-tj]...[A1<-t1]blk CASE prog = (B let pat = [c|e]add r1<-r2+m in blk) Cr |- fact:Reg r1 t1 Ca,Cr |-* fact:Reg r2 t2 ------------------------------------------------------- (Ca,Cr);(Cr) |- [fact|fact]add r1<-r2+m : Reg r1 (t2+m) ------------------------------------------------------- |- pat:Reg r1 (t2+m) => D;G Ca D;G |- blk ---------------------------------------------- C1 |- let pat = [fact|fact]add r1<-r2+m in blk !C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn ------------------------------------------------------------------------------ D;Up;R;G;{};Lp |- {n1->b1,...,nn->bn} let pat = [fact|fact]add r1<-r2+m in blk where C1 = D;Up;R;G;{n1->t1,...,nn->tn);Lp and C1 = Ca,Cr and: Us,Up;R;Ls,Lp;[fact|fact]add r1<-r2+m --> Us,Up;R;L0,r1->L(r2)+m;fact ------------------------------------------------------------------------------------------------------------ B |- Us,Up;R;Ls,Lp;let pat = [fact|fact]add r1<-r2+m in blk --> Us,Up;R;L0,r1->L(r2)+m;let pat = fact in blk --------------------------------------------------------------------------------------------------------------- (Us,Up;R;Ls,Lp;B let pat = [fact|fact]add r1<-r2+m in blk) --> (Us,Up;R;L0,r1->L(r2)+m;B let pat = fact in blk) where L = L0,r1->m0 and L = Ls,Lp By typing inversion and type equivalence inversion: !_Cr,r1->m1 |- fact:Reg r1 t1 where R |- t1=m1 and Cr=!_Cr,r1->m1 _Car,r2->m2 |- fact:Reg r2 t2 where R |- t2=m2 and Ca,Cr=_Car,r2->m2 Lp(r1) = m1 Lp(r2) = m2 L0 = Ls,Lp0 Let Lp' = Lp0,r1->L(r2)+m and Up'=Up and R'=R |- C',Us,Ls Lp'(r1) = L(r2)+m = Lp(r2)+m = m2+m Let Cr'=!_Cr,r1->m2+m Cr' |- fact:Reg r1 (m2+m) Cr' |- fact:Reg r1 (t2+m) C' |- B let pat = fact in blk OTHER CASES SIMILAR LEMMA[canonical forms] If C |- v:t then: (1) If C |- t=!t' then v = !v' (2) If C |- t=ta -o tb then v = \pat:t'.e and C |- t'=ta (3) If C |- t=t1*t2 then v = v1,v2 (4) If C |- t=all A:k.t1 then v = \A:k.e (5) If C |- t=exists A:k.t1 then v = pack t',v' as t'' and C |- t''=exists A:k.t1 (6) If C |- t=%t' then v = %e (7) If C |- t=Reg t1 t2 or C |- v:Mem t1 t2 or C |- v:Delay t1 then v = fact (8) If C |- t=Code t1 t2 then v = code(n)[t1'...tn'] Proof by induction on C |- v:t CASE C |- v:t' C |- t' = t ----------- C |- v:t By induction, (1)...(8) hold. (note: this is the only induction case; all other C |- v:t are base cases) CASE C |- e:t'' ------------ C |- %e:%t'' Only case (6) applies: C |- %t''=t=%t' Type equivalence inversion rules out other cases. For example, C |- %t''=t=!t' violates type equivalence inversion. So v = %e. OTHER CASES SIMILAR THEOREM[progress] (1) If C = {};U;R;{};P;L and |- C and C |- e:t and e is not a value and there is no t' such that C |- t = %t' then there is some e' such that e --> e' CASE C |- e:t'' C |- t'' = t ----------- C |- e:t There is no t' such that C |- t'' = %t' (otherwise, C |- t = t'' = %t') By induction, there is some e' such that e --> e' CASE C1 |- ef:ta -o tb C2 |- ea:ta ----------------- C1,C2 |- ef ea:tb Suppose ef is not a value: By type equivalence inversion, there is no t' s.t. C |- ta -o tb = %t' By induction, ef-->ef', so ef ea-->ef' ea. Otherwise, ef is a value. By canonical forms, ef = \pat:t'.e. (\pat:t'.e) ea steps. CASES delay k | commit[t=type(t)] e | e >>@ e | e >>* e These have type %t'; (1) does not apply. (See (2) instead.) OTHER CASES SIMILAR THEOREM[progress] (2) If C = {};Up;R;{};P;L and |- C,Us and C |- e:t and e is not a value then there is some Up';R';e' such that Us,Up;R;e --> Us,Up';R';e' CASE C1 |- ef:ta -o tb C2 |- ea:ta ----------------- C1,C2 |- ef ea:tb By (1), ef ea --> e' By rule, Us,Up;R;ef ea --> Us,Up;R;e' CASE !C |- delay k: %(exists A:k.Delay type(A)) (Us,Up;R; delay k) --> (Us,(Up,q_k);R; %pack q_k,fact as exists A:k.Delay type(A)) where q_k is fresh CASE C |- e:Delay t C |- t:k C |- t':k ------------------------------------------------------------ C |- commit[t=type(t')]e:%(!all F:k->type.F t -o F type(t')) Suppose e is not a value: By induction, U;R;e --> U';R';e', so U;R;commit[t=type(t')]e --> U';R';commit[t=type(t')]e' Otherwise, e is a value. By canonical forms, e = fact. By typing inversion: D;{q_k};R;!G;P;{} |- fact:Delay type(q_k) where C = D;{q_k};R;!G;P;{} and R |- Delay t = Delay type(q_k). By type equivalence inversion, R |- t = type(q_k). Up = {q_k}. Let Up' = {}. R |- t=type(q_k) ----------------------------------------------------------------------------------- (Us,q_k;R; commit[t=type(t')] fact) --> (Us;R,q_k->t'; %!\F:k->type.\x:F type(q_k).x) CASE C1 |- e1:%ta C2 |- e2:ta -o tb ------------------------ C1,C2 |- e1 >>@ e2 : %tb Suppose e1 is not a value: By induction, U;R;e1 --> U';R';e1', so U;R;e1>>@e2 --> U';R';e1'>>@e2 Otherwise, suppose e2 is not a value: By induction, U;R;e2 --> U';R';e2', so U;R;e1>>@e2 --> U';R';e1>>@e2' Otherwise, e1 and e2 are values. By canonical forms, e1=%ea. (U;R; %ea >>@ e2) --> (U;R; %(e2 ea)) (where e2 is a value) OTHER CASES SIMILAR THEOREM[progress] (3) If C = {};Up;R;{};P;L and |- C,Us and C |- c:t and c is not a value then there is some Up';R';c' such that Us,Up;R;c --> Us,Up';R';c' (note: c = e is handled by (2)) CASE C |- c:%t --------- C |- #c:t Suppose c is not a value: By induction, U;R;c --> U';R';c', so U;R;#c --> U';R';#c' Otherwise, c is a value. By canonical forms, c = %e. (U;R;#%e) --> (U;R;e) THEOREM[progress] (4) If C = {};Up;R;{};P;Lp and |- C,Us,Ls and C |- prog then there is some U';R';L';prog' such that Us,Up;R;Ls,Lp;prog --> Us,Up';R';Ls,Lp';prog' CASE prog = B [c]jmp m C1 |- c:(Code m t) * t ---------------------- C1 |- [c]jmp m !C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn ------------------------------------- D;U;R;G;{};L |- B [c]jmp m where C1 = D;U;R;G;{n1->t1,...,nn->tn);L and B = {n1->b1,...,nn->bn} If c is not a value: By (3), c steps, so [c]jmp n steps by congruence. Otherwise, c is a value. By canonical forms, c = (code(m)[t1...tj],v) where: D |- t1:k1 ... D |- tj:kj tm = all A1:k1...all Aj:kj.Code m t' t = [Aj<-tj]...[A1<-t1]t' By inversion on !C1 |- m->bm:tm : !C1,A1:k1,...,Aj:kj |- m->bm':Code m t' where bm = \A1:k1...\Aj:kj.bm' bm' = \pat:t'.blk pat<-v => [s] ------------------------------------------------------------------------ B |- U;R;L;[code(n)[t1...tj],v]jmp n --> U;R;L;[s][Aj<-tj]...[A1<-t1]blk where bm=\A1:k1...\An:kj.\pat:t'.blk OTHER CASES SIMILAR