***DRAFT*** (Sep 1, 2006) Syntax t = A | t->t | t/\t | %t ======================================================= Source language rules: G = {...t...} G,t |- t G,ta |- tb ----------- G |- ta->tb G |- ta->tb G |- ta ----------- G |- tb G |- t1 G |- t2 ----------- G |- t1/\t2 G |- t1/\t2 ----------- k in {1,2} G |- tk G |- t ------- G |- %t G |- %(ta->tb) G |- %ta ----------- G |- %tb ======================================================= Target language rules: See figure 4.1 of Simpson (omitting False and \/) G = {...w(t)...} G,w(t) |- w(t) G,w(ta) |- w(tb) ---------------- G |- w(ta->tb) G |- w(ta->tb) G |- w(ta) -------------- G |- w(tb) G |- w(t1) G |- w(t2) -------------- G |- w(t1/\t2) G |- w(t1/\t2) -------------- k in {1,2} G |- w(tk) G,wRw' |- wRw' G,wRw' |- w'(t) ---------------- where w' does not appear in G |- w(%t) G |- w(%t) G |- w(%t) G |- wRw' ---------- G |- w'(t) G |- w(t) G |- wRw' ---------- G |- w'(t) (note: not in Simpson) ======================================================= Lemma[soundness] If t1...tn |- t0 then w(t1)...w(tn) |- w(t0) Proof by induction on t1...tn |- t0. CASE G,t |- t G = t1...tn G' = w(t1)...w(tn) G',w(t) |- w(t) CASE G,ta |- tb ----------- G |- ta->tb G = t1...tn G' = w(t1)...w(tn) induction: G',w(ta) |- w(tb) G',w(ta) |- w(tb) ----------------- G' |- w(ta->tb) CASE G |- ta->tb G |- ta ----------- G |- tb G = t1...tn G' = w(t1)...w(tn) induction: G' |- w(ta->tb) induction: G' |- w(ta) G' |- w(ta->tb) G' |- w(ta) --------------- G' |- w(tb) EASY CASES: G |- t1 G |- t2 ----------- G |- t1/\t2 G |- t1/\t2 ----------- k in {1,2} G |- tk CASE G |- t ------- G |- %t G = t1...tn G' = w(t1)...w(tn) induction: G' |- w(t) By weakening, G',wRw' |- w(t) where w' is fresh. G',wRw' |- w(t) ---------------- G',wRw' |- w'(t) ---------------- G' |- w(%t) CASE G |- %(ta->tb) G |- %ta ----------- G |- %tb G = t1...tn G' = w(t1)...w(tn) induction: G' |- w(%(ta->tb)) induction: G' |- w(%ta) By weakening: G',wRw' |- w(%(ta->tb)) G',wRw' |- w(%ta) where w' is fresh. G',wRw' |- w(%(ta->tb)) G',wRw' |- w(%ta) ----------------------- ----------------- G',wRw' |- w'(ta->tb) G',wRw' |- w'(ta) -------------------------------------------- G',wRw' |- w'(tb) ----------------- G' |- w(%tb) ======================================================= Definitions. Let Graph(G,w1,...,wn) be the smallest directed graph satisfying: - Graph(G,...wk...) contains a node wk - if G contains w'Rw'', then Graph(G,w) contains a node w', a node w'', and an edge from w' to w'' Say that a graph contains a path w1...wn (where n>=1) if for each wk,wk+1, wk and wk+1 are nodes in the graph and there is an edge in the graph from wk to wk+1. Call a path w1...wn "a path from w1 to wn". Define a list with head w1 and tail wn to be a directed graph with nodes w1,w2,...,wn (where n>=1) where for each wk,wk+1 there is an edge from wk,wk+1, and there are no other edges. Define the depth "Depth(L,w')" of a node w' in a list L to be the distance from L's head to the node. For any context G, let w(G) be the union of the following sets: - {w'(t) in G | there is a path from w' to w in Graph(G)} - {w''Rw' in G | there is a path from w' to w in Graph(G)} ======================================================= Lemma[Possible future irrelevance]: (1) if G |- w(t) then w(G) |- w(t) (2) if G |- wRw' then w'(G) |- wRw' Proof by induction on derivation of G |- w(t). CASE G,w(t) |- w(t) w(G,w(t)) contains w(t), so: w(G,w(t)) |- w(t) CASE G,w(ta) |- w(tb) ---------------- G |- w(ta->tb) induction: w(G,w(ta)) |- w(tb) w(G,w(ta)) = w(G) union {w(ta)}, so w(G),w(ta) |- w(tb) w(G),w(ta) |- w(tb) ------------------- w(G) |- w(ta->tb) EASY CASES: G |- w(ta->tb) G |- w(ta) -------------- G |- w(tb) G |- w(t1) G |- w(t2) -------------- G |- w(t1/\t2) G |- w(t1/\t2) -------------- k in {1,2} G |- w(tk) CASE G,wRw' |- wRw' w'(G,wRw') contains wRw', so w'(G,wRw') |- wRw' CASE G,wRw' |- w'(t) ---------------- where w' does not appear in G |- w(%t) G |- w(%t) induction: w'(G,wRw') |- w'(t) w' does not appear in G, so Graph(G,wRw') equals Graph(G) with one extra node w' and one extra edge from w to w'. Therefore, any path from any node w1 in Graph(G,wRw') to w' go through w (unless w1=w'). Therefore: w'(G,wRw') = w(G),wRw' so: w(G),wRw' |- w'(t) ------------------ w(G) |- w(%t) CASE G |- w(%t) G |- wRw' ---------- G |- w'(t) induction: w(G) |- w(%t) By inversion, G contains wRw', so Graph(G) contains an edge from w to w'. Therefore, for any path from any node w1 in Graph(G) to w, there is a path in Graph(G) from w1 to w'. Therefore, w(G) is a subset of w'(G). By weakening: w'(G) |- w(%t). Since w'(G) contains wRw', w'(G) |- wRw'. w'(G) |- w(%t) w'(G) |- wRw' -------------- w'(G) |- w'(t) CASE G |- w(t) G |- wRw' ---------- G |- w'(t) induction: w(G) |- w(t) Just as in the previous case, conclude w'(G) |- w(t) and w'(G) |- wRw'. w'(G) |- w(t) w'(G) |- wRw' -------------- w'(G) |- w'(t) ======================================================= Define [G] = ...t... where G = ...w(t)... Lemma[completeness]: if G |- wn(t) and Graph(G,wn) is a list L = w1...wn then there is some ...tk... such that [G],...tk... |- t and there is a mapping F from each tk to some j where 1<=jtb) Graph((G,wn(ta)),wn) = Graph(G,wn) induction: [G,wn(ta)],...tk... |- tb for each tk: [wj(G,wn(ta))],...ti... |- %tk where jtb goal: [G],...tk... |- ta->tb for each tk: [wj(G)],...ti... |- %tk CASE G |- w(ta->tb) G |- w(ta) -------------- G |- w(tb) induction: [G],...tk... |- ta->tb [G],...tk'... |- ta Let ...tk''... = ...tk...,...tk'... By weakening: [G],...tk''... |- ta->tb [G],...tk''... |- ta Conclude [G],...tk''... |- tb. CASE G |- w(t1) G |- w(t2) -------------- G |- w(t1/\t2) induction: [G],...tk... |- t1 [G],...tk'... |- t2 Let ...tk''... = ...tk...,...tk'... By weakening: [G],...tk''... |- t1 [G],...tk''... |- t2 Conclude [G],...tk''... |- t1/\t2. CASE G |- w(t1/\t2) -------------- z in {1,2} G |- w(tz) induction: [G],...tk... |- t1/\t2 Conclude [G],...tk... |- tz. CASE G,wRw' |- wRw' not applicable CASE G,(wn)R(wn+1) |- wn+1(t) ------------------------ where wn+1 does not appear in G |- wn(%t) G |- wn(%t) Let L = Graph(G,wn) = w1...wn. Let L' = Graph((G,(wn)R(wn+1))). Since wn+1 does not appear in Graph(G,wn), L' is a list, equal to w1...wn,wn+1. induction: [G,(wn)R(wn+1)],...tk'... |- t and for each tk', [wj(G,(wn)R(wn+1))],...ti'... |- %tk' where F(tk')=j and ...F(ti')t ---------------------------------------- ... ---------------------------------------- [G],...tk...,tkm' |- ...->tk2'->tk1'->t ---------------------------------------- [G],...tk... |- tkm'->...->tk2'->tk1'->t ------------------------------------------- [G],...tk... |- %(tkm'->...->tk2'->tk1'->t) [G],...tk... |- %tkm' ----------------------------------------------------------------------- ... ----------------------------------------------------------------------- [G],...tk... |- %(tk2'->tk1'->t) [G],...tk... |- %tk2' ----------------------------------------------------------------------- [G],...tk... |- %(tk1'->t) [G],...tk... |- %tk1' ----------------------------------------------------------------------- [G],...tk... |- %(t) goal: [G],...tk... |- %t and for each tk, [wj(G)],...ti... |- %tk where F(tk)=j and ...F(ti)