================================================= =================== LANG2 ======================= ================================================= define based on lang0 ================================================= ================== SYNTAX ======================= ================================================= same t,p,g,v,h,l,e k = type | res | cap p b = A | t | q _t = all A:cap+ where u1#A<=a1,...,un#A<=an.t q,u,a = A | {} | {A p} | q1+q2 c = u#a d = . | d,A:k | d,A:cap+ where u1#A<=a1,...,un#A<=an _h = \A:cap+ where u1#A<=a1,...,un#A<=an.h by convention: u:cap~ a:cap+ Let d |- u#a:cap mean d |- u:cap~ and d |- a:cap+ Let d |- u#a=u'#a':cap mean d |- u=u':cap~ and d |- a=a':cap+ [Question: can {A p} be written as just {A}?] ================================================= ================= SEMANTICS ===================== ================================================= d |- . d |- d' ----------- (A not in Dom(d,d')) d |- d',A:k d |- d' d,d' |- u1:cap~ ... d,d' |- un:cap~ d,d' |- a1:cap+ ... d,d' |- an:cap+ ------------------------------------------ (A not in Dom(d,d')) d |- d',A:cap+ where u1#A<=a1,...,un#A<=an ================================================= drop rule: all A<=c.t:type drop rules: d |- c:cap ...,A:cap+ where u1#A<=a1,...,un#A<=an,... |- A:cap+ d |- u1:cap~ ... d |- un:cap~ d |- a1:cap+ ... d |- an:cap+ d,A:cap+ where u1#A<=a1,...,un#A<=an |- t:type -------------------------------------------------- (A not in Dom(d)) d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t:type d |- {}:cap p d |- A:res ---------------- d |- {A p}:cap p d |- q1:cap p d |- q2:cap p ---------------- d |- q1+q2:cap p ================================================= drop rule: d |- c1 = /c1' drop rule: d |- /c = /c+/c drop rule: d |- /{} = {} drop rule: d |- /{A~} = {A+} drop rule: d |- //c = /c drop rule: d |- /(c1+c2) = /c1+/c2 modify rules: "where k = cap" --> "where k = cap p" modify rules: c,c1,c1',c2,c2',c3 --> q,q1,q1',q2,q2',q3 d |- a:cap+ ----------------- d |- a = a+a:cap+ ================================================= drop rules: d |- c1 <= c2 ...,(A:cap+ where ...,u#A<=a,...),... |- u#A<=a d |- A:res -------------------- d |- {A~}#{} <= {A+} d |- a1 = a2:cap+ ----------------- d |- {}#a1 <= a2 d |- u1#a1 <= a2 d |- u2#a2 <= a3 ------------------- d |- u1+u2#a1 <= a3 d |- u1#a1 <= a1' d |- u2#a2 <= a2' --------------------------- d |- u1+u2#a1+a2 <= a1'+a2' d |- u:cap~ d |- a:cap+ -------------- (optional) d |- u#a <= {} ================================================= drop rule: d |- all A<=c.t = all A<=c'.t':type d |- u1 = u1':cap~ ... d |- un = un':cap~ d |- a1 = a1':cap+ ... d |- an = an':cap+ d,A:cap+ where u1#A<=a1,...,un#A<=an |- t = t':type -------------------------------------------------------------------------------------------------- (A not in Dom(d)) d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t = all A:cap+ where u1'#A<=a1',...,un'#A<=an'.t':type ================================================= drop rule: d;g |- \A<=c.h: all A<=c.t d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t: type d,(A:cap+ where u1#A<=a1,...,un#A<=an);g |- h:t --------------------------------------------------- (A not in Dom(d)) d;g |- \A:cap+ where u1#A<=a1,...,un#A<=an.h: all A:cap+ where u1#A<=a1,...,un#A<=an.t ================================================= drop rule: d;g |- v[c:cap]: [A<-c]t d;g |- v: all A:cap+ where u1#A<=a1,...,un#A<=an.t d |- u1#a <= a1 ... d |- un#a <= an d;g |- a:cap+ -------------------------------------------------- d;g |- v[a:cap+]: [A<-a]t ================================================= drop rule: d;g |- new A,x drop rule: d;g |- free v drop rule: d;g |- use v d;g;u#a |- new A,x ==> d,A:res;g,x:A handle;u+{A~}#a (A not in Dom(d) and x not in Dom(g)) d;g |- v: A handle d |- u = u'+{A~}:cap~ ------------------------------ d;g;u#a |- free v ==> d;g;u'#a d;g |- v: A handle //d;g |- c <= {A+} (optional) c = u#a d |- u = u1+u2:cap~ d |- u1#a <= a'+{A+} ------------------------ d;g;c |- use v ==> d;g;c ================================================= drop rule: d;g;c |- v1 v2 drop rule: d;g;c |- halt d;g |- v1: (u'#a',t)->0 d;g |- v2: t d |- u = ub+u':cap~ d |- ub#a <= a' ----------------------- d;g;u#a |- v1 v2 d |- u = {}:cap~ d |- a = {}:cap+ ---------------- d;g;u#a |- halt ================================================= ========== LANG1->LANG2 TRANSLATION ============= ================================================= T(A) = A T(A handle) = A handle T(all A:type.t) = all A:type.T(t) T(all A:res.t) = all A:res.T(t) T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t) T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t) T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t) T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t) T((c,t)->0) = (C(c),T(t))->0 T() = U(A) = Au U({}) = {} U({A~}) = {A~} U({A+}) = {} U(c1+c2) = U(c1)+U(c2) A(A) = Aa A({}) = {} A({A~}) = {} A({A+}) = {A+} A(c1+c2) = A(c1)+A(c2) C(c) = U(c)#A(c) D(.) = . D(A:type,d) = A:type, D(d) D(A:res,d) = A:res, D(d) D(A:cap,d) = Aa:cap+, Au:cap~, D(d) D(A:cap+,d) = Aa:cap+. [Au<-{}]D(d) D(A:cap+<=c,d) = Aa:cap+ where {}#Aa<=A(c), [Au<-{}]D(d) D(A:cap<=c0,c1,...,cn,d) = Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), [Au<-Ab+U(c0)]D(d) [.] = [] [A:type,d] = [d] [A:res,d] = [d] [A:cap,d] = [d] [A:cap+,d] = [Au<-{}][d] [A:cap+<=c,d] = [Au<-{}][d] [A:cap<=c0,c1,...,cn,d] = [Au<-Ab+U(c0)][d] G(.) = . G(x:t,g) = x:T(t),G(g) d;g |- v:t ~~> v' d;g |- h:t ~~> h' d;g;c |- l ==> d';g';c' ~~> l' d;g;c |- e ~~> e' (ugly, but probably relegated to the appendix or TR anyway) V(x) = x V(v[t:type]) = V(v)[T(t):type] V(v[A:res]) = V(v)[A:res] d;g |- v: all A:cap.t ~~> v' d |- c:cap ----------------------------------------------------- d;g |- v[c:cap]: [A<-c]t ~~> v'[A(c):cap+][U(c):cap~] d;g |- v: all A:cap+.t ~~> v' d |- c:cap+ ------------------------------------------- d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+] d;g |- v: all A:cap+<=c0.t ~~> v' d |- c <= c0 d |- c:cap+ ------------------------------------------- d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+] d;g |- v: all A:cap<=c0,...,cn.t ~~> v' d |- c <= c0 ~~> ub d |- c <= c1 ... d |- c <= cn d |- c:cap --------------------------------------------------- d;g |- v[c:cap]: [A<-c]t ~~> v'[ub:cap~][A(c):cap+] d;g |- v: t' ~~> v' d |- t' = t:type ------------------- d;g |- v: t ~~> v' H(\A:type.h) = \A:type.H(h) H(\A:res.h) = \A:res.H(h) H(\A:cap.h) = \Aa:cap+.\Au:cap~.H(h) H(\A:cap+.h) = \Aa:cap+.[Au<-{}]H(h) H(\A:cap+<=c.h) = \Aa:cap+ where {}#Aa<=A(c).[Au<-{}]H(h) H(\A:cap<=c0,c1,...,cn.h) = \Ab:cap~. \Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]H(h) H(\(c,x:t).e) = \(C(c),x:T(t)).E(e) H() = d;g |- h: t' ~~> h' d |- t' = t:type ------------------- d;g |- h: t ~~> h' L(x=v) = x=V(v) L(x=h) = x=H(h) L(x=v.n) = x=V(v).n L(new A,x) = new A,x L(free v) = free V(v) L(use v) = use V(v) E(let l in e) = let L(l) in E(e) E(v1 v2) = V(v1) V(v2) E(halt) = halt ================================================= d |- c1 = c2:k -------------------- where k = cap or k = cap+ d |- c1 <= c2 ~~> {} d |- c1 <= c2 ~~> u d |- c2 <= c3 ~~> u' ---------------------- d |- c1 <= c3 ~~> u+u' d |- c1 <= c1' ~~> u1 d |- c2 <= c2' ~~> u2 ------------------------------- d |- c1+c2 <= c1'+c2' ~~> u1+u2 ...,(A:cap+<=c),... |- A<=c ~~> {} ...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab ...,(A:cap<=c0,...,ck,...),... |- A<=ck ~~> Ab+U(c0) d |- A:res -------------------------- d |- {A~} <= {A+} ~~> {A~} // (optional) //d |- c:cap //--------------------- //d |- c <= {} ~~> U(c) ================================================= =================== LEMMAS ====================== ================================================= Language lemmas: - if |- d and d |- g and d;g |- v:t then d |- t:type - if |- d and d |- g and d;g |- h:t then d |- t:type - if |- d and d |- [A<-c1]t:type and d |- c1=c2:cap~ then d |- [A<-c1]t=[A<-c2]t:type Translation lemmas: -- if |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]U(c):cap~ -- if |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]A(c):cap+ -- if |- d and d |- c1<=c2~~>u then D(d) |- [d]u:cap~ -- if d |- d' then D(d) |- [d]D(d') -- if |- d and d |- t:type then D(d) |- [d]T(t):type -- if |- d and d |- c:cap+ then D(d) |- [d]U(c)={}:cap~ -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]U(c1)=[d]U(c2):cap~ -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]A(c1)=[d]A(c2):cap+ -- if |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type -- if |- d and d |- c1<=c2~~>u then D(d) |- [d]U(c1)=[d]u+[d]U(c2):cap~ and D(d) |- [d]u#[d]A(c1)<=[d]A(c2) corollary: if |- d and d |- c1<=c2 and d |- c2:cap+ then D(d) |- [d]U(c1)#[d]A(c1)<=[d]A(c2) -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then A([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]A(c) -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then U([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]U(c) -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- t:type then T([A'<-c']t) = [Au'<-U(c'),Aa'<-A(c')]T(t) -- if |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t) -- if |- d and d |- g then D(d) |- [d]G(g) -- if |- d and d |- g then: - if d;g |- v:t ~~> v' then D(d);[d]G(g) |- [d]v':[d]T(t) - if d;g |- h:t ~~> h' then D(d);[d]G(g) |- [d]h':[d]T(t) - if d;g;c |- l==>d';g';c' ~~> l' then D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c') and [d]=[d'] - if d;g;c |- e ~~> e' then D(d);[d]G(g);[d]C(c) |- [d]e' ================================================= If |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]U(c):cap~ By induction on d, then by induction on derivation of d |- c:k CASE: ...,A:cap,... |- A:cap [...,A:cap,...]U(A) = [...,A:cap,...]Au = Au D(...,A:cap,...) = ...,Aa:cap+,Au:cap~,... CASE: ...,A:cap+,... |- A:cap+ [...,A:cap+,...]U(A) = [...,A:cap+,...]Au = {} CASE: ...,(A:cap+<=c),... |- A:cap+ [...,A:cap+<=c,...]U(A) = [...,A:cap+<=c,...]Au = {} CASE: ...,(A:cap<=c0,c1,...,cn),... |- A:cap d = d1,(A:cap<=c0,c1,...,cn),d2 |- d1,(A:cap<=c0,c1,...,cn),d2 implies d1 |- c0:cap By induction, D(d1) |- [d1]U(c0):cap~ [d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1 By weakening, D(d) |- [d]U(c0):cap~ [...,(A:cap<=c0,c1,...,cn),...]U(A) = [...,(A:cap<=c0,c1,...,cn),...]Au = Ab+U(c0) D(...,(A:cap<=c0,c1,...,cn),...) = Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)]D(d) EASY CASES: d |- c:cap+ ----------- d |- c:cap d |- {}:cap+ d |- A:res -------------- d |- {A+}:cap+ d |- A:res ------------- d |- {A~}:cap d |- c1:k d |- c2:k ------------ where k = cap or k = cap+ d |- c1+c2:k ================================================= If |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]A(c):cap+ CASE: ...,A:cap,... |- A:cap [...,A:cap,...]A(A) = [...,A:cap,...]Aa = Aa D(...,A:cap,...) = ...,Aa:cap+,Au:cap~,... CASE: ...,A:cap+,... |- A:cap+ [...,A:cap+,...]A(A) = [...,A:cap+,...]Aa = Aa D(...,A:cap+,...) = ...,Aa:cap+,... CASE: ...,(A:cap+<=c),... |- A:cap+ [...,A:cap+<=c,...]A(A) = [...,A:cap+<=c,...]Aa = Aa D(...,A:cap+<=c,...) = ...,Aa:cap+ where {}#Aa<=A(c),... CASE: ...,(A:cap<=c0,c1,...,cn),... |- A:cap [...,(A:cap<=c0,c1,...,cn),...]A(A) = [...,(A:cap<=c0,c1,...,cn),...]Aa = Aa D(...,(A:cap<=c0,c1,...,cn),...) = Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)]D(d) EASY CASES: d |- c:cap+ ----------- d |- c:cap d |- {}:cap+ d |- A:res -------------- d |- {A+}:cap+ d |- A:res ------------- d |- {A~}:cap d |- c1:k d |- c2:k ------------ where k = cap or k = cap+ d |- c1+c2:k ================================================= If |- d and d |- c1<=c2~~>u then D(d) |- [d]u:cap~ EASY CASES: d |- c1 = c2:k -------------------- where k = cap or k = cap+ d |- c1 <= c2 ~~> {} d |- c1 <= c2 ~~> u d |- c2 <= c3 ~~> u' ---------------------- d |- c1 <= c3 ~~> u+u' d |- c1 <= c1' ~~> u1 d |- c2 <= c2' ~~> u2 ------------------------------- d |- c1+c2 <= c1'+c2' ~~> u1+u2 ...,(A:cap+<=c),... |- A<=c ~~> {} CASE: ...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab D(...,(A:cap<=c0,...),...) = ..., Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), ... CASE: d1,(A:cap<=c0,...,ck,...),d2 |- A<=c ~~> Ab+U(c0) d = d1,(A:cap<=c0,...,ck,...),d2 |- d1,(A:cap<=c0,...,ck,...),d2 implies that d1 |- c0:cap By weakening, d |- c0:cap By lemma, D(d) |- [d]U(c0):cap~ D(d) = ..., Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), ... [d] = [d1][Au<-Ab+U(c0)][d2] EASY CASE: d |- A:res -------------------------- d |- {A~} <= {A+} ~~> {A~} ================================================= If d |- d' then D(d) |- [d]D(d') (Note: D(d,d') = D(d),[d]D(d')) EASY CASES: d |- . d |- d' ----------- (A not in Dom(d,d'),k=type or k=res or k=cap) d |- d',A:k CASE: d |- d' -------------- (A not in Dom(d,d')) d |- d',A:cap+ Induction: D(d) |- [d]D(d') Aa not in Dom(D(d),[d]D(d')) By rule, D(d) |- [d]D(d'),Aa:cap+ CASE: d |- d' d,d' |- c:cap+ ----------------- (A not in Dom(d,d')) d |- d',A:cap+<=c Induction: D(d) |- [d]D(d') Lemma: D(d,d') |- [d]A(c):cap+ By rule, D(d) |- [d]D(d'),Aa:cap+ where {}#Aa<=[d]A(c) CASE: d |- d' d,d' |- c0:cap d,d' |- c1:cap+ ... d,d' |- cn:cap+ ----------------------------------- (A not in Dom(d,d')) d |- d',A:cap<=c0,c1,...,cn Induction: D(d) |- [d]D(d') Lemma: D(d,d') |- [d]U(c0):cap~ Lemma: D(d,d') |- [d]A(c0):cap+ Lemma: D(d,d') |- [d]A(ck):cap+ for 1<=k<=n By rule, D(d) |- [d]D(d'),Ab:cap~ By rule, D(d) |- [d]D(d'),Ab:cap~,Aa:cap+ where [d]Ab#Aa<=[d]A(c0),[d]Ab+[d]U(c0)#Aa<=[d]A(c1),...,[d]Ab+[d]U(c0)#Aa<=[d]A(cn) ================================================= If |- d and d |- t:type then D(d) |- [d]T(t):type EASY CASES: ...,A:type,... |- A:type d |- A:res ------------------ d |- A handle:type d |- t1:type d |- t2:type ----------------- d |- :type d,A:k |- t:type ------------------- (where k=type or k=res or k=cap) d |- all A:k.t:type CASE: d,A:cap+ |- t:type ---------------------- (A not in Dom(d)) d |- all A:cap+.t:type Induction: D(d,A:cap+) |- [d,A:cap+]T(t):type D(d),A:cap+ |- [d][Au<-{}]T(t):type ----------------------------------------- D(d) |- all Aa:cap+. [d][Au<-{}]T(t):type CASE: d |- c:cap+ d,A:cap+<=c |- t:type ------------------------- (A not in Dom(d)) d |- all A:cap+<=c.t:type Lemma: D(d) |- [d]A(c):cap+ Induction: D(d,A:cap+<=c) |- [d,A:cap+<=c]T(t):type D(d),Aa:cap+ where {}#Aa<=[d]A(c) |- [d][Au<-{}]T(t):type -------------------------------------------------------------- D(d) |- all Aa:cap+ where {}#Aa<=[d]A(c). [d][Au<-{}]T(t):type CASE: d |- c0:cap d |- c1:cap+ ... d |- cn:cap+ d,A:cap<=c0,c1,...,cn |- t:type ------------------------------- (A not in Dom(d)) d |- all A:cap<=c0,c1,...,cn.t:type Lemma: D(d) |- [d]A(c0):cap+ Lemma: D(d) |- [d]U(c0):cap~ Lemma: D(d) |- [d]A(ck):cap+ where 1<=k<=n Induction: D(d,A:cap<=c0,c1,...,cn) |- [d,A:cap<=c0,c1,...,cn]T(t):type Au not in freevars(U(ck)), because A not in freevars(ck) Au not in freevars(A(c0)), because A not in freevars(c0) D(d),Ab:cap~, Aa:cap+ where [d]Ab#Aa<=[d][Au<-Ab+U(c0)]A(c0), [d]Ab+[d][Au<-Ab+U(c0)]U(c0)#Aa<=[d][Au<-Ab+U(c0)]A(c1),..., [d]Ab+[d][Au<-Ab+U(c0)]U(c0)#Aa<=[d][Au<-Ab+U(c0)]A(cn) |- [d][Au<-Ab+U(c0)]T(t):type -------------------------------------------- D(d) |- all Ab:cap~. all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=A(c1),...,Ab+[d]U(c0)#Aa<=A(cn). [d][Au<-Ab+U(c0)] T(t) EASY CASE: d |- t:type d |- c:cap ------------------ d |- (c,t)->0:type ================================================= If |- d and d |- c:cap+ then D(d) |- [d]U(c)={}:cap~ Abbreviations: D = D(d), U1 = [d]U(c1), A1 = [d]A(c1), etc. CASE: d1,A:cap+,d2 |- A:cap+ [d1,A:cap+,d2]U(A) = [d1][Au<-{}][d2]Au = {} CASE: d1,A:cap+<=c,d2 |- A:cap+ [d1,A:cap+<=c,d2]U(A) = [d1][Au<-{}][d2]Au = {} CASE: d |- {}:cap+ U({}) = {} CASE: d |- A:res -------------- d |- {A+}:cap+ U({A+}) = {} CASE: d |- c1:cap+ d |- c2:cap+ --------------- d |- c1+c2:cap+ Induction: D(d) |- [d]U(c1)={}:cap~ Induction: D(d) |- [d]U(c2)={}:cap~ D(d) |- [d]U(c1)={}:cap~ D(d) |- [d]U(c2)={}:cap~ D(d) |- {}:cap~ ---------------------------------------------------- --------------------- D(d) |- [d]U(c1)+[d]U(c2)={}+{}:cap~ D(d) |- {}+{}={}:cap~ ----------------------------------------------------------------------------- D(d) |- [d]U(c1)+[d]U(c2)={}:cap~ ================================================= If |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type EASY CASES: d |- t:type --------------- d |- t = t:type d |- t2 = t1:type ----------------- d |- t1 = t2:type d |- t1 = t2:type d |- t2 = t3:type ----------------- d |- t1 = t3:type d |- t1 = t1':type d |- t2 = t2':type ----------------------------- d |- = :type d,A:k |- t = t':type -------------------------------- (A not in Dom(d)) d |- all A:k.t = all A:k.t':type CASE: d |- c = c':cap+ d,A:cap+<=c |- t = t':type --------------------------------------------- (A not in Dom(d)) d |- all A:cap+<=c.t = all A:cap+<=c'.t':type similar to proof for lemma "If |- d and d |- t:type then D(d) |- [d]T(t):type" CASE: d |- c0 = c0':cap d |- c1 = c1':cap+ ... d |- cn = cn':cap+ d,A:cap<=c0,c1,...,cn |- t = t':type ------------------------------------------------------------------- (A not in Dom(d)) d |- all A:cap<=c0,c1,...,cn.t = all A:cap<=c0',c1',...,cn'.t':type similar to proof for lemma "If |- d and d |- t:type then D(d) |- [d]T(t):type" EASY CASE: d |- t = t':type d |- c = c':cap ------------------------------- d |- (c,t)->0 = (c',t')->0:type ================================================= If |- d and d |- c1<=c2~~>u then D(d) |- [d]U(c1)=[d]u+[d]U(c2):cap~ and D(d) |- [d]u#[d]A(c1)<=[d]A(c2) Corollary: If |- d and d |- c1<=c2 and d |- c2:cap+ then D(d) |- [d]U(c1)#[d]A(c1)<=[d]A(c2) Abbreviations: D = D(d), U1 = [d]U(c1), A1 = [d]A(c1), etc. Abbreviations: Ux = [d]ux, Uy = [d]uy (If d |- c1<=c2~~>ux then D |- U1=Ux+U2:cap~ and D |- Ux#A1<=A2) Proof of corollary: By lemma, D |- U2={}:cap~ By main lemma, D |- U1=Ux+U2:cap~ D |- U1=Ux+{}:cap~ D |- U1=Ux:cap~ By main lemma, D |- Ux#A1<=A2 D |- U1#A1<=A2 Proof of main lemma: CASE: d |- c1 = c2:k -------------------- where k = cap or k = cap+ d |- c1 <= c2 ~~> {} By lemma, D |- U1=U2:cap~ By rule, D |- {}+U2=U2:cap~, so D |- U1={}+U2:cap~ By lemma, D |- A1=A2:cap+ By rule, D |- {}#A1<=A2 CASE: d |- c1 <= c2 ~~> ux d |- c2 <= c3 ~~> uy ----------------------- d |- c1 <= c3 ~~> ux+uy Induction: D |- U1=Ux+U2:cap~ and D |- Ux#A1<=A2 D |- U2=Uy+U3:cap~ and D |- Uy#A2<=A3 D |- Ux=Ux:cap~ D |- U2=Uy+U3:cap~ ------------------------------------- D |- U1=Ux+U2:cap~ D |- Ux+U2=Ux+(Uy+U3):cap~ ------------------------------------------------ D |- U1=Ux+(Uy+U3):cap~ ----------------------- D |- U1=(Ux+Uy)+U3:cap~ D |- Ux#A1<=A2 D |- Uy#A2<=A3 -------------------------------- D |- Ux+Uy#A1<=A3 CASE: d |- c1 <= c1' ~~> ux d |- c2 <= c2' ~~> uy ------------------------------- d |- c1+c2 <= c1'+c2' ~~> ux+uy Induction: D |- U1=Ux+U1':cap~ and D |- Ux#A1<=A1' D |- U2=Uy+U2':cap~ and D |- Uy#A2<=A2' D |- U1=Ux+U1':cap~ D |- U2=Uy+U2':cap~ ------------------------------------------ D |- U1+U2=(Ux+U1')+(Uy+U2'):cap~ --------------------------------- D |- U1+U2=(Ux+Uy)+(U1'+U2'):cap~ D |- Ux#A1<=A1' D |- Uy#A2<=A2' ---------------------------------- D |- Ux+Uy#A1+A2<=A1'+A2' CASE: d1,(A:cap+<=c),d2 |- A<=c ~~> {} d = d1,(A:cap+<=c),d2 [d1]Aa = Aa [d1]A(c) = [d]A(c) because freevars(c) are declared in d1 [d] = [d1,A:cap+<=c,d2] = [d1][Au<-{}][d2] [d]A(A) = [d]Aa = Aa [d]U(A) = [d]Au = {} |- d1,(A:cap+<=c),d2 implies d1 |- c:cap+ By weakening, d |- c:cap+ By lemma, D(d) |- [d]U(c) = {}:cap~ Prove D(d) |- [d]U(A)=[d]{}+[d]U(c):cap~ [d]U(A) = {} [d]{} = {} D(d) |- [d]U(c) = {}:cap~ Prove D(d) |- [d]{}#[d]A(A)<=[d]A(c) D(d) = D(d1,A:cap+<=c,d2) = ...,Aa:cap+ where {}#[d1]Aa<=[d1]A(c), ... = ...,Aa:cap+ where {}#Aa<=[d]A(c), ... ...,Aa:cap+ where {}#Aa<=[d]A(c), ... |- {}#Aa<=[d]A(c) CASE: ...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab d = d1,(A:cap<=c0,...),d2 [d] = [d1,(A:cap<=c0,...),d2] = [d1][Au<-[d1]Ab+[d1]U(c0)][d1] [d1]A(c0) = [d]A(c0) because freevars(c0) are declared in d1 [d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1 [d]Ab = Ab [d]U(A) = [d]Au = [d1]Ab+[d1]U(c0) = Ab+[d]U(c0) [d]A(A) = [d]Aa = Aa Prove D(d) |- [d]U(A)=[d]Ab+[d]U(c0):cap~ D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0):cap~ Prove D(d) |- [d]Ab#[d]A(A)<=[d]A(c0) D(d) |- Ab#Aa<=[d]A(c0) D(d) = D(d1,(A:cap<=c0,...),d2) = ...,Ab:cap~, (Aa:cap+ where [d1]Ab#Aa<=[d1]A(c0),...),... = ...,Ab:cap~, (Aa:cap+ where Ab#Aa<=[d]A(c0),...),... CASE: ...,(A:cap<=c0,...,ck,...),... |- A<=ck ~~> Ab+U(c0) d = d1,(A:cap<=c0,...,ck,...),d2 [d] = [d1,(A:cap<=c0,...,ck,...),d2] = [d1][Au<-[d1]Ab+[d1]U(c0)][d1] [d1]A(c0) = [d]A(c0) because freevars(c0) are declared in d1 [d1]A(ck) = [d]A(ck) because freevars(ck) are declared in d1 [d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1 [d1]U(ck) = [d]U(ck) because freevars(ck) are declared in d1 [d]Ab = Ab [d]U(A) = [d]Au = [d1]Ab+[d1]U(c0) = Ab+[d]U(c0) [d]A(A) = [d]Aa = Aa |- d1,(A:cap<=c0,...,ck,...),d2 implies d1 |- ck:cap+ By weakening, d |- ck:cap+ By lemma, D(d) |- [d]U(ck) = {}:cap~ Prove D(d) |- [d]U(A)=[d](Ab+U(c0))+[d]U(ck):cap~ D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0)+[d]U(ck):cap~ D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0)+{}:cap~ Prove D(d) |- [d](Ab+U(c0))#[d]A(A)<=[d]A(ck) D(d) |- Ab+[d]U(c0)#Aa<=[d]A(ck) D(d) = D(d1,(A:cap<=c0,...,ck,...),d2) = ...,Ab:cap~, (Aa:cap+ where [d1]Ab#Aa<=[d1]A(c0),...,[d1](Ab+U(c0))#Aa<=[d1]A(ck),...),... = ...,Ab:cap~, (Aa:cap+ where Ab#Aa<=[d]A(c0),...,Ab+[d]U(c0)#Aa<=[d]A(ck),...),... CASE: d |- A:res -------------------------- d |- {A~} <= {A+} ~~> {A~} [d]{A p} = {A p} Prove D(d) |- [d]U({A~})=[d]{A~}+[d]U({A+}):cap~ D(d) |- {A~}={A~}+{}:cap~ Prove D(d) |- [d]{A~}#[d]A({A~})<=[d]A({A+}) D(d) |- {A~}#{}<={A+} ================================================= If |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]U(c1)=[d]U(c2):cap~ CASE: d |- c:k ------------ k=cap or k=cap+ d |- c = c:k By lemma, D(d) |- [d]U(c):cap~ EASY CASES: d |- c2 = c1:k -------------- k=cap or k=cap+ d |- c1 = c2:k d |- c1 = c2:k d |- c2 = c3:k -------------- k=cap or k=cap+ d |- c1 = c3:k d |- c1 = c1':k d |- c2 = c2':k ---------------------- k=cap or k=cap+ d |- c1+c2 = c1'+c2':k d |- c:k --------------- k=cap or k=cap+ d |- {}+c = c:k d |- c1:k d |- c2:k -------------------- k=cap or k=cap+ d |- c1+c2 = c2+c1:k d |- c1:k d |- c2:k d |- c3:k ------------------------------ k=cap or k=cap+ d |- (c1+c2)+c3 = c1+(c2+c3):k d |- c1 = c2:cap+ ----------------- d |- c1 = c2:cap CASE: d |- c:cap+ ----------------- d |- c = c+c:cap+ By lemma, D(d) |- [d]U(c)={}:cap~ ================================================= If |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]A(c1)=[d]A(c2):cap+ CASE: d |- c:k ------------ k=cap or k=cap+ d |- c = c:k By lemma, D(d) |- [d]A(c):cap+ EASY CASES: d |- c2 = c1:k -------------- k=cap or k=cap+ d |- c1 = c2:k d |- c1 = c2:k d |- c2 = c3:k -------------- k=cap or k=cap+ d |- c1 = c3:k d |- c1 = c1':k d |- c2 = c2':k ---------------------- k=cap or k=cap+ d |- c1+c2 = c1'+c2':k d |- c:k --------------- k=cap or k=cap+ d |- {}+c = c:k d |- c1:k d |- c2:k -------------------- k=cap or k=cap+ d |- c1+c2 = c2+c1:k d |- c1:k d |- c2:k d |- c3:k ------------------------------ k=cap or k=cap+ d |- (c1+c2)+c3 = c1+(c2+c3):k d |- c1 = c2:cap+ ----------------- d |- c1 = c2:cap CASE: d |- c:cap+ ----------------- d |- c = c+c:cap+ By lemma, D(d) |- [d]A(c):cap+ D(d) |- [d]A(c):cap+ -------------------------------------- D(d) |- [d]A(c) = [d]A(c)+[d]A(c):cap+ ================================================= If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then A([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]A(c) CASE: A(A') = Aa' A([A'<-c']A') = A(c') [Au'<-U(c'),Aa'<-A(c')]A(A') = [Au'<-U(c'),Aa'<-A(c')]Aa' = A(c') CASE: A(A) = Aa A([A'<-c']A) = A(A) = Aa [Au'<-U(c'),Aa'<-A(c')]A(A) = [Au'<-U(c'),Aa'<-A(c')]Aa = Aa (where Au'!=Aa and Aa'!=Aa because A'!=A) CASE: A({A'+}) = {A'+} Impossible case: d |- A':k' and d |- A':res cannot both be true EASY CASES: A({}) = {} A({A~}) = {} A({A+}) = {A+} A(c1+c2) = A(c1)+A(c2) ================================================= If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then U([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]U(c) CASES JUST LIKE LEMMA FOR A(c): U(A') = Au' U(A) = Au U({}) = {} U({A~}) = {A~} U({A'~}) = {A'~} U({A+}) = {} U(c1+c2) = U(c1)+U(c2) ================================================= If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- t:type then T([A'<-c']t) = [Au'<-U(c'),Aa'<-A(c')]T(t) CASE: T(A') = A' Impossible case: d |- A':k' and d |- A':type cannot both be true EASY CASES: T(A) = A T(A handle) = A handle T(A' handle) = A' handle T(all A:type.t) = all A:type.T(t) T(all A:res.t) = all A:res.T(t) T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t) T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t) T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t) T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t) T((c,t)->0) = (C(c),T(t))->0 T() = ================================================= If |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t) (easy supporting lemmas: If |- d and d |- A':type and d |- c:k (k=cap or k=cap+) then A([A'<-t']c) = [A'<-T(t')]A(c) If |- d and d |- A':type and d |- c:k (k=cap or k=cap+) then U([A'<-t']c) = [A'<-T(t')]U(c) ) EASY CASES: T(A') = A' T(A) = A T(A handle) = A handle T(A' handle) = A' handle T(all A:type.t) = all A:type.T(t) T(all A:res.t) = all A:res.T(t) T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t) T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t) T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t) T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t) T((c,t)->0) = (C(c),T(t))->0 T() = ================================================= If |- d and d |- g then D(d) |- [d]G(g) easy induction using lemma: if |- d and d |- t:type then D(d) |- [d]T(t):type ================================================= If |- d and d |- g then: - if d;g |- v:t ~~> v' then D(d);[d]G(g) |- [d]v':[d]T(t) - if d;g |- h:t ~~> h' then D(d);[d]G(g) |- [d]h':[d]T(t) - if d;g;c |- l==>d';g';c' ~~> l' then D(d);[d]G(g);[d]C(c) |- [d']l'==>D(d');[d']G(g');[d']C(c') - if d;g;c |- e ~~> e' then D(d);[d]G(g);[d]C(c) |- [d]e' EASY CASE: d,A:k;g |- h:t ------------------------ (k=type or k=res) (A not in Dom(d)) d;g |- \A:k.h: all A:k.t CASE: d,A:cap;g |- h:t ~~> h' ---------------------------- (A not in Dom(d)) d;g |- \A:cap.h: all A:cap.t ~~> \Aa:cap+.\Au:cap~.h' T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t) Induction: D(d,A:cap);[d,A:cap]G(g) |- [d,A:cap]h':[d,A:cap]T(t) D(d),Aa:cap+, Au:cap~;[d]G(g) |- [d]h':[d]T(t) ---------------------------------------------------------- D(d),Aa:cap+;[d]G(g) |- \Au:cap~.[d]h':all Au:cap~.[d]T(t) ----------------------------------------------------------------------- D(d);[d]G(g) |- \Aa:cap+.\Au:cap~.[d]h':all Aa:cap+.all Au:cap~.[d]T(t) D(d);[d]G(g) |- [d]\Aa:cap+.\Au:cap~.h':[d]all Aa:cap+.all Au:cap~.T(t) CASE: d,A:cap+;g |- h:t ~~> h' ----------------------------- (A not in Dom(d)) d;g |- \A:cap+.h: all A:cap.t ~~> \Aa:cap+.[Au<-{}]h' T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t) Induction: D(d,A:cap+);[d,A:cap+]G(g) |- [d,A:cap+]h':[d,A:cap+]T(t) D(d),Aa:cap+;[d][Au<-{}]G(g) |- [d][Au<-{}]h':[d][Au<-{}]T(t) -------------------------------------------------------------------------- D(d);[d][Au<-{}]G(g) |- \Aa:cap+.[d][Au<-{}]h':all Aa:cap+.[d][Au<-{}]T(t) D(d);[d][Au<-{}]G(g) |- [d]\Aa:cap+.[Au<-{}]h':[d]all Aa:cap+.[Au<-{}]T(t) [Au<-{}]G(g) = G(g) because d |- g implies A not in freevars(g) CASE: d |- all A:cap+<=c.t: type d,A:cap+<=c;g |- h:t ~~> h' ---------------------------------------------- (A not in Dom(d)) d;g |- \A:cap+<=c.h: all A:cap+<=c.t ~~> \Aa:cap+ where {}#Aa<=A(c).[Au<-{}]h' T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t) By lemma, D(d) |- [d]T(all A:cap+<=c.t): type D(d) |- [d]all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t):type Induction: D(d,A:cap+<=c);[d,A:cap+<=c]G(g) |- [d,A:cap+<=c]h':[d,A:cap+<=c]T(t) D(d),Aa:cap+ where {}#Aa<=[d]A(c);[d][Au<-{}]G(g) |- [d][Au<-{}]h':[d][Au<-{}]T(t) -------------------------------------------------------------------------------------------------------------------- D(d);[d][Au<-{}]G(g) |- \Aa:cap+ where {}#Aa<=[d]A(c).[d][Au<-{}]h':all Aa:cap+ where {}#Aa<=[d]A(c).[d][Au<-{}]T(t) D(d);[d][Au<-{}]G(g) |- [d]\Aa:cap+ where {}#Aa<=A(c).[Au<-{}]h':[d]all Aa:cap+ where {}#Aa<=A(c).[Au<-{}]T(t) [Au<-{}]G(g) = G(g) because d |- g implies A not in freevars(g) CASE: d |- all A:cap<=c0,c1,...,cn.t: type d,(A:cap<=c0,c1,...,cn);g |- h:t ~~> h' ------------------------------------------------------------ (A not in Dom(d)) d;g |- \A:cap<=c0,c1,...,cn.h: all A:cap<=c0,c1,...,cn.t ~~> \Ab:cap~. \Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]h' T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t) By lemma, D(d) |- [d]T(all A:cap<=c0,c1,...,cn.t): type D(d) |- [d]all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t):type D(d), [d]all Ab:cap~. |- [d]all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t):type Induction: D(d,(A:k<=c1,...,cn));[d,(A:k<=c1,...,cn)]G(g) |- [d,(A:k<=c1,...,cn)]h':[d,(A:k<=c1,...,cn)]T(t) D(d),Ab:cap~, Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn); [d][Au<-Ab+U(c0)]G(g) |- [d][Au<-Ab+U(c0)]h':[d][Au<-Ab+U(c0)]T(t) ------------------------------------------------------------------------------------------------- D(d),Ab:cap~;[d][Au<-Ab+U(c0)]G(g) |- \Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]h': all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]T(t) --------------------------------------------------------------------------------------------------------------- D(d);[d][Au<-Ab+U(c0)]G(g) |- \Ab:cap~.\Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]h': all Ab:cap~.all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]T(t) D(d);[d][Au<-Ab+U(c0)]G(g) |- [d]\Ab:cap~.\Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]h': [d]all Ab:cap~.all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]T(t) [Au<-Ab+U(c0)]G(g) = G(g) because d |- g implies A not in freevars(g) EASY CASES: d |- c:cap d |- t:type d;g,x:t;c |- e --------------------------- (x not in Dom(g)) d;g |- \(c,x:t).e: (c,t)->0 d;g |- v1: t1 d;g |- v2: t2 ----------------------- d;g |- : CASE: d;g |- h: t' d |- t' = t:type ---------------- d;g |- h: t Lemma: D(d) |- [d]T(t')=[d]T(t):type CASE: d;...,x:t,... |- x: t V(x) = x G(...,x:t,...) = ...,x:T(t),... EASY CASE: d;g |- v: all A:k.t d |- b:k ---------------------- where k=type or k=cap d;g |- v[b:k]: [A<-b]t CASE: d;g |- v: all A:cap+.t ~~> v' d;g |- c:cap+ ------------------------------------------- d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+] By lemma, all A:cap+.t:type T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t) By lemma, D(d) |- all Aa:cap+. [Au<-{}]T(t):type By lemma, D(d) |- [d]A(c):cap+ By lemma, D(d) |- [d]U(c)={}:cap~ By lemma, D(d) |- [Au<-[d]U(c)][d]all Aa:cap+.T(t) =[Au<-{}][d]all Aa:cap+.T(t):type Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap+.t) D(d);[d]G(g) |- [d]v': all Aa:cap+. [d][Au<-{}]T(t) -------------------------------------------------------------------- D(d);[d]G(g) |- [d]v': all Aa:cap+. [d][Au<-U(c)]T(t) ---------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)] [d][Au<-U(c)]T(t) D(d);[d]G(g) |- [d](v'[A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)]T(t) [Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c)) By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t) CASE: d;g |- v: all A:cap.t ~~> v' d;g |- c:cap ----------------------------------------------------- d;g |- v[c:cap]: [A<-c]t ~~> v'[A(c):cap+][U(c):cap~] By lemma, d |- all A:cap.t:type T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t) By lemma, D(d) |- [d]A(c):cap+ By lemma, D(d) |- [d]U(c):cap~ Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap.t) D(d);[d]G(g) |- [d]v': all Aa:cap+. all Au:cap~. [d]T(t) ----------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)]all Au:cap~. [d]T(t) -------------------------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+][[d]U(c):cap~]: [Au<-[d]U(c)][Aa<-[d]A(c)][d]T(t) D(d);[d]G(g) |- [d](v'[A(c):cap+][U(c):cap~]): [d][Au<-U(c)][Aa<-A(c)]T(t) [Au<-U(c)][Aa<-A(c)] = [Au<-U(c),Aa<-A(c)] because Au not in freevars(A(c)) By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t) CASE: d;g |- v: all A:cap+<=c0.t ~~> v' d;g |- c <= c0 ~~> u d;g |- c:cap+ ------------------------------------------- d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+] By lemma, d |- all A:cap+<=c0.t:type By inversion, d |- c0:cap+ By lemma, D(d) |- [d]U(c0)={}:cap~ T(all A:cap+<=c0.t) = all Aa:cap+ where {}#Aa<=A(c0). [Au<-{}] T(t) By lemma, D(d) |- [d]all Aa:cap+ where {}#Aa<=A(c0). [Au<-{}] T(t):type By lemma, D(d) |- [d]A(c):cap+ By lemma, D(d) |- [d]U(c)={}:cap~ By lemma, D(d) |- all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-[d]U(c)] [d]T(t):type = all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-{}] [d]T(t):type By lemma, D(d) |- [d]U(c)#[d]A(c)<=[d]A(c0) Induction: D(d);[d]G(g) |- [d]v':[d]T(all A:cap+<=c0.t) D(d);[d]G(g) |- [d]v':all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-{}] [d]T(t) ----------------------------------------------------------------------------------- D(d);[d]G(g) |- [d]v':all Aa:cap+ where [d]U(c)#Aa<=[d]A(c0). [Au<-[d]U(c)] [d]T(t) ----------------------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)][Au<-[d]U(c)] [d]T(t) D(d);[d]G(g) |- [d](v'[A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)] T(t) [Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c)) By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t) CASE: d;g |- v: all A:cap<=c0,...,cn.t ~~> v' d;g |- c <= c0 ~~> ub d;g |- c <= c1 ... d;g |- c <= cn d;g |- c:cap --------------------------------------------------- d;g |- v[c:cap]: [A<-c]t ~~> v'[ub:cap~][A(c):cap+] By lemma, d |- all A:cap<=c0,...,cn.t:type By inversion, d |- ck:cap+ for 1<=k<=n T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t) By lemma, D(d) |- [d]ub:cap~ By lemma, D(d) |- [d]A(c):cap+ By lemma, D(d) |- [d]U(c)=[d]ub+[d]U(c0):cap~ and D(d) |- [d]ub#[d]A(c)<=[d]A(c0) By lemma, D(d) |- [d]U(c)#[d]A(c)<=A(ck) for 1<=k<=n By lemma, D(d) |- [Au<-[d]ub+[d]U(c0)][d][Aa<-A(c)][Ab<-ub] T(t) = [Au<-U(c)][d][Aa<-A(c)][Ab<-ub] T(t) Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap<=c0,...,cn.t) D(d);[d]G(g) |- [d]v': all Ab:cap~. all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),..., Ab+[d]U(c0)#Aa<=[d]A(cn). [d][Au<-Ab+U(c0)] T(t) ------------------------------------------------------------------------ D(d);[d]G(g) |- ([d]v')[[d]ub:cap~]: all Aa:cap+ where [d]ub#Aa<=[d]A(c0),[d]ub+[d]U(c0)#Aa<=[d]A(c1),..., [d]ub+[d]U(c0)#Aa<=[d]A(cn). [d][Au<-ub+U(c0)][Ab<-ub]T(t) ------------------------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]ub:cap~]: all Aa:cap+ where [d]ub#Aa<=[d]A(c0),[d]U(c)#Aa<=[d]A(c1),..., [d]U(c)#Aa<=[d]A(cn). [d][Au<-ub+U(c0)][Ab<-ub]T(t) ------------------------------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]ub:cap~][[d]A(c):cap+]: [d][Aa<-A(c)][Au<-ub+U(c0)][Ab<-ub] T(t) ------------------------------------------------------------------------------------------- D(d);[d]G(g) |- ([d]v')[[d]ub:cap~][[d]A(c):cap+]: [d][Aa<-A(c)][Au<-U(c)][Ab<-ub] T(t) D(d);[d]G(g) |- [d](v'[ub:cap~][A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)][Ab<-ub] T(t) [Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c)) [Ab<-ub]T(t) = T(t) because Ab not in freevars(T(t)) By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t) EASY CASES: d;g |- v: t' d |- t' = t:type ---------------- d;g |- v: t d;g |- v:t -------------------------- (x not in Dom(g)) d;g;c |- x=v ==> d;g,x:t;c d;g |- h:t -------------------------- (x not in Dom(g)) d;g;c |- x=h ==> d;g,x:t;c d;g |- v: ------------------------------ (x not in Dom(g) and 1<=n<=2) d;g;c |- x=v.n ==> d;g,x:t_n;c CASE: d;g;c |- new A,x ==> d,A:res;g,x:A handle;c+{A~} (A not in Dom(d) and x not in Dom(g)) C(c+{A~}) = C(c)+{A~} [d,A:res] = [d] EASY CASE: d;g |- v: A handle d |- c = c'+{A~}:cap -------------------------- d;g;c |- free v ==> d;g;c' CASE: d;g |- v: A handle d |- c <= c'+{A+} ------------------------ d;g;c |- use v ==> d;g;c Induction: D(d);G(g) |- V(v): A handle Lemma: D(d) |- C(c) <= C(c'+{A+}) D(d) |- C(c) <= C(C')+{A+} CASE: d;g;c |- l ==> d';g';c' ~~> l' d';g';c' |- e ~~> e' ----------------------- d;g;c |- let l in e ~~> let l' in e' Induction: D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d);[d]G(g');[d]C(c') and [d]=[d'] Induction: D(d');[d']G(g');[d']C(c') |- [d']e' D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c') D(d');[d]G(g');[d]C(c') |- [d]e' ------------------------------------------ D(d);[d]G(g);[d]C(c) |- let [d]l' in [d]e' CASE: d;g |- v1: (c',t)->0 ~~> v1' d;g |- v2: t ~~> v2' d |- c <= c' ~~> u -------------------- d;g;c |- v1 v2 ~~> v1' v2' Induction: D(d);[d]G(g) |- [d]v1': [d]T((c',t)->0) Induction: D(d);[d]G(g) |- [d]v2': [d]T(t) By lemma: D(d) |- [d]U(c)=[d]u+[d]U(c'):cap~ and D(d) |- [d]u#[d]A(c)<=[d]A(c') D(d);[d]G(g) |- [d]v1': ([d]U(c')#[d]A(c'),[d]T(t))->0 D(d);[d]G(g) |- [d]v2': [d]T(t) D(d) |- [d]U(c)=[d]u+[d]U(c'):cap~ D(d) |- [d]u#[d]A(c)<=[d]A(c') -------------------------------------------- D(d);[d]G(g);[d]U(c)#[d]A(c) |- v1' v2' EASY CASE: d |- c = {}:cap --------------- d;g;c |- halt =================================================