Computer Science 591i
More Tree-Surgery for Church-Rosser Theorems

In the first case of the proof of Church-Rosser Theorem we showed that if we used path p to select a redex, and alternatively used path q to select another redex, then we could arrive at a common result by using q and p respectively, provided the two paths diverged.

This leaves us with the cases in which we have one path contained in another. We'll need to tuck a few more appropriate lemmas under our belt before we can essay the remaining cases.

We'll need to prove these using induction on path-length, so let's define this useful concept.

Definition

If p is a path, we define the length of p recursively by

length(s::p) = 1+length(p)

A Confession

It seems that we would have been better to disallow addressing of a constant or variable by a non-empty path... But the definition of proper addressing given below attempts to remedy this.

Also, a certain amount of hand-waving with respect to -conversion (and other matters) is going to occur. This is marked by the symbol

However the following Lemma from Hindley's book should assuage our collective conscience:

Lemma-

If P P' and Q Q' and P Q then P' Q'

Proof

See Hindley, Lemma 1.27

Definition

Let E be a term of the

-calculus, and let p be a path. We say that p properly addresses the term E if cases PH2, PH3 of the definition of the concept of address by a path don't occur.

Definition

Let E be a term of the

-calculus, with v a variable, and let p be a path. We say that v remains in scope from E down p, and write seen(v,E,p) according to the following definition:

SC1 It is always the case that seen(v,E,())

SC2 Otherwise, if E = u, a variable, or E = c, a constant, then seen(v,E,p) holds.

SC3 Otherwise, if E = (F G), an application, then

SC3.1 If hd(p) = 0 then seen(v,E,p) iff seen(v,F,tl(p))

SC3.2 If hd(p) = 1 then seen(v,E,p) iff seen(v,G,tl(p))

SC4 Otherwise, if E = v.G then it is not the case that seen(v,E,p). In this case, we say that v goes out of scope.

SC5 Otherwise, if E = u.G then

SC5.1 If hd(p) = 0 then seen(v,E,p)

SC5.2 If hd(p) = 1 then seen(v,E,p) iff seen(v,G,tl(p))

We're going to need the odd lemma here, mostly to say how substitution interacts with path-indexing.

Lemma PT3

If E,F are terms of the

-calculus, and v is a variable of the aforementioned, and p is a path which properly addresses E and seen(v,E,p) then there is an E' which is

-congruent to E for which

E'[v:=F][p] = E'[p][v:=F]

Proof

Let E' be formed from E by

-converting any

-abstraction found on p whose bound variable is a member of FV(F) to an abstraction whose bound variable is not a member of FV(F).

We now proceed by induction on the length of p.

Base Case

In the base-case length(p)=0, so that p = (). In this case, since by PH1 E'[p]=E' and v is in scope, we have

E'[p][v:=F] = E'[v:=F] = E'[v:=F][p]

Inductive Step

Suppose for some natural number n that length(p) n implies that

E'[p][v:=F] = E'[v:=F][p] Consider a path p for which length(p) = n+1 Then p = s::p', where p'=tl(p), and length(p')=n.

Case 1-2 E'=v, a variable, or E'=c, a constant. Since p properly addresses E', these cases don't occur.
Case 3: E' = (C D), an application. We have 2 sub-cases, s=0 and s=1
- Sub-case 3.1, s=0
  The last step above uses the inductive hypothesis, justified because length(p') = n, and seen(v,C,p') by SC3. On the other hand, using S5
  Hence the result holds in this sub-case.
- Sub-case 3.2, s=1 This is similar to 3.1
Case 4: E' = x . H, an abstraction. We have 2 sub-cases, s=0 and s=1
- Sub-case 4.1, s=0
  Since substitution converts an abstraction into an abstraction. So the result holds for this sub-case.
- Sub-case 4.2, s=1
  using the inductive hypothesis. On the other hand, we have our very favourite can of worms when we come to
  because we have to consider cases S5-S7 of the definition of substitution.
  - Sub-sub-case 4.2.1, x=v
    In this sub-sub-case, v goes out of scope, so, by ex falsa libet the result holds.
  - Sub-sub-case 4.2.2, x v and either x FV(F) or v FV(H) Here
    So the result holds in this sub-sub-case
  - Sub-sub-case 4.2.3, x v and x FV(F) or v FV(H)
    This sub-case can't occur because of the way we have defined E'.

Lemma PT4

If E,F,G are terms of the

-calculus, and v is a variable of the aforementioned, and p is a path which properly addresses E and seen(v,E,p) then there is an E' which is

-congruent to E for which

E'[p:=G][v:=F] = E'[v:=F][p:=G[v:=F]]

Proof

Let E' be formed from E by

-converting any

-abstraction found on p whose bound variable is a member of FV(F) to an abstraction whose bound variable is not a member of FV(F).

We now proceed by induction on the length of p.

Base Case

In the base-case length(p)=0, so that p = (). In this case, since by UP1 E'[p:=G]=G and v is in scope, we have

E'[p:=G][v:=F] = G[v:=F] While

E'[v:=F][p:=G[v:=F]] = G[v:=F]

Inductive Step

Suppose for some natural number n that length(p) n implies that

E'[p:=G][v:=F] = E'[v:=F][p:=G[v:=F]] Consider a path p for which length(p) = n+1 Then p = s::p', where p'=tl(p), and length(p')=n

Case 1-2 E'=v, a variable, or E'=c, a constant. Since p properly addresses E', these cases don't occur.
Case 3: E' = (C D), an application. We have 2 sub-cases, s=0 and s=1
- Sub-case 3.1, s=0
  The last step above uses the inductive hypothesis, justified because length(p') = n, and seen(v,C,p') by SC3. On the other hand, using S5
  Hence the result holds in this sub-case.
- Sub-case 3.2, s=1 This is similar to 3.1
Case 4: E' = x . H, an abstraction. We have 2 sub-cases, s=0 and s=1
- Sub-case 4.1, s=0
  Since substitution converts an abstraction into an abstraction. So the result holds for this sub-case.
- Sub-case 4.2, s=1
  Now we again (sigh!) have to consider cases S5-S7 of the definition of substitution.
  - Sub-sub-case 4.2.1, x=v
    In this sub-sub-case, v goes out of scope, so, by ex falsa libet the result holds.
  - Sub-sub-case 4.2.2, x v and either x FV(F) or v FV(H). Here
    On the other hand,
    So the result holds in this sub-sub-case
  - Sub-sub-case 4.2.3, x v and x FV(F) or v FV(H) This sub-case can't occur because of the way we have defined E'.

Lemma Sub.4

Let E, F, G be terms of the

-calculus, and let u, v be variables, for which u v
and u FV(G) and v FV(F). Let it be the case also that no variable bound in E is free in F or in G. Then

E[u:=F][v:=G] = E[v:=G][u:=F]

Proof

We proceed by induction on n, the height of E.

Base Case n=0

Suppose E = u.
By Lemma Sub.1, since v FV(F).
On the other hand
So the result is satisfied for this case.
Suppose E = v.
On the other hand
by Lemma Sub.1, since u FV(G)
Suppose E = x, where x is a variable for which x u,v
On the other hand
So the lemma holds in this case.
Suppose E = c C.
This case is similar to the preceding one.

Inductive Step

Suppose for a given n we have for any term E for which height(E) n

E[u:=F][v:=G] = E[v:=G][u:=F]

Consider an expression E of height n+1 We must show our result holds for E

Suppose E=(C D) .
Using S4 repeatedly we obtain:
So using the inductive hypothesis.
On the other hand,
So the lemma holds in this case.
Suppose E = u . H.
since u G.
On the other hand
thus the lemma holds for this case.
Suppose E = v . H.
since v FV[F]
On the other hand
Since v FV(F)
thus the lemma holds for this case.
Suppose E = x . H By the premises of this Lemma, x FV(F) and x FV(G).
Hence
by the inductive hypothesis.
On the other hand
since x FV[F] FV[G] this
So the result holds in this case.

Figure for Proposition LC2

Proposition LC2

Let (E = ( u.C) G) be a redex of the

-calculus.

Let p be a path for which E[p] = ( v.D) H) where hd(p)=0 and hd(tl(p))=1. and also seen(u,E,p). Let p' = tl(tl(p)). Then

Proof

Let C' be formed from C by

-converting any

-abstraction whose bound variable is a member of FV(G) FV(H) to an abstraction whose bound variable is not a member of {u} FV(G)) FV(H).

Let (E' = ( u'.C') G) and let v', D', H' be the converted forms of v,D,H.

Consider that by Lemma PT3.

= E'[p][u':=G] = (( v'.D') H)[u':=G]

using the definition of path-addressing, and expanding E. Now we apply S4 to distribute substitution across the application

= (( v'.D')[u':=G] H[u':=G])

and next we can apply S6 because we have

-converted to avoid variable-capture.

= (( v'.D'[u':=G]) H[u':=G])

Which is a redex. So, we can work out

that is

using lemma PT4, as being

= C'[u':=G][p':=D'[u':=G][v':=H']] On the other hand, we can immediately apply the definition of

obtaining

= (E'[p:=D'[v':=H']],())

Expanding E' and using (twice) the definition of path-addressing, we obtain

= ((( u'. C'[p':=D'[v':=H']])G)),())

which, by the definition of

= C'[p':=D'[v':=H']][u':=G]

Now, we can use lemma PT4 to distribute the outer-substitution across the path-update:

= C'[u':=G][p':=D'[v':=H'][u':=G]]

Whence we can apply Lemma Sub.4 because we have chosen v' FV(G) FV(H).

= C'[u':=G][p':=D'[u':=G][v':=H']]

Thus we have shown that local-confluence holds for E', which is

-congruent to E. Local confluence for Eitself follows from

-conversion.

Computer Science 591i More Tree-Surgery for Church-Rosser Theorems

Definition

A Confession

Lemma-

Proof

Definition

Definition

Lemma PT3

Proof

Base Case

Inductive Step

Lemma PT4

Proof

Base Case

Inductive Step

Lemma Sub.4

Proof

Proposition LC2

Proof

Computer Science 591i
More Tree-Surgery for Church-Rosser Theorems