Lambda Calculus Draw Parse Tree
W ^ \ / \ / \ / v X Yi.e., we first use some beta-expansions to get from X to some lambda expression W, then use some beta-reductions to get from W to Y. Because every beta-expansion is the inverse of a beta-reduction, this means that we can get from W to X (as well as from W to Y) using a sequence of beta-reductions; i.e., we have the following picture:
W / \ / \ / \ v v X YThe Church-Rosser Theorem guarantees that there's a Z such that both X and Y reduce to Z:
W / \ / \ v v X Y \ / \ / v v ZSince Y is (by assumption) in normal form, it must be that Y = Z, and our picture really looks like this:
W / \ / | v | X | \ | \ / v v Ywhich means that X reduces to Y without any expansions.
Now we're ready for the induction step:
Induction Hypothesis: If X has normal form Y, and we can get from X to Y using a sequence of beta-expansions and reductions that involve n changes of direction (for n >= 1), then we can get from X to Y using only beta-reductions.
Now we must show that (given the induction hypothesis) Corollary 1 holds for n+1 changes of direction.
Here's a picture of an X and a Y such that n+1 changes of direction are needed to get from X to Y:
W ^ \ ^ \ ^ \ / \ / \ / \ / \ / \ / / v / v / v X ... ... Y <--1 change --> <-- n changes of direction -->Note that there is some lambda expression W (shown in the picture above) such that:
- We can get from X to W using a series of beta-expansions, and
- we can get from W to Y using beta expansions and reductions, with n changes of direction.
W \ \ v YCombining this with point 1 we have:
W ^ \ / \ / \ / v X YIn other words, we can get from X to W using only beta-expansions, and from W to Y using only beta-reductions. Using the same reasoning that we used above to prove the second base case, we conclude that we can get from X to Y using only beta-reductions.
Recall that Corollary 2 says that if lambda-term X has normal form Y then Y is unique (up to alpha-reduction); i.e., X has no other normal form. We can prove that by contradiction: Assume that, in contradiction to the Corollary, Y and Z are two different normal forms of X. By Corollary 1, X reduces to both Y and Z:
X / \ / \ / \ v v Y ZBy the Church-Rosser Theorem, this means there is W, such that:
X / \ / \ v v Y Z \ / \ / v v WHowever, since by assumption Y and Z are already in normal form, there are no reductions to be done; thus, Y = W = Z, and X does not have two distinct normal forms.
Recall that the theorem is:
- if (X0 red X1) and (X0 red X2), then there is an X3 such that: (X1 red X3) and (X2 red X3).
Where "red" means "zero or more beta-reductions" (since we're assuming de Bruijn notation, and thus ignoring alph-reductions).
We'd like to prove the theorem by "filling in the diamond" from X0 to X3; i.e., by showing that something like the following situation must exist:
X0 / \ W1 Z1 / \ / \ W2 A X2 / \ / \ / X1 B C \ / \ / D E \ / F = X3In other words, we'd like to show that for every lambda term, if you can take two different "steps" (can do two different beta-reductions) to terms A and B, then you can come back to a common term C by doing one beta-reduction from A, and one from B. If we could show that, then we'd have the desired X3 by construction as shown in the picture above.
Unfortunately, this idea doesn't quite work; i.e., it is not true in general that we can get to common term C in just one step from A and one step from B. Below is an example that illustrates this, using * to mean a redex that reduces to y.
X0 = (λx.xx)(*) / \ / \ (**) (λx.xx)y \ / \ / \ / (y*) or (*y) / \ / \ / (yy)Note that there are two redexes in the initial term X0: * itself, and the one in which * is the argument to a lambda-term. So we can take two different "steps" from X0, arriving either at (**) or at (λx.xx)y. While we can come back to a common term, (yy), from both of those, it requires two steps from (**).
So to prove the Church-Rosser Theorem, we need a new definition:
Definition (the diamond property): A relation ~~> on terms has the diamond property iff
- ( X0 ~~> X1) and ( X0 ~~> X2) implies there is an X3 such that ( X1 ~~> X3 ) and ( X2 ~~> X3 )
Note:
- The Church-Rosser Theorem says that the relation beta-reduce* has the diamond property (i.e., if X beta-reduces to both A and B in zero or more steps, then both A and B beta-reduce to C in zero or more steps).
- The previous example showed that single beta reduction does not have the diamond property (just because X beta-reduces to both A and B in one step does not mean that both A and B beta-reduce to C in one step).
To prove the Church-Rosser Theorem we will perform the following 3 tasks:
- Define a new relation called a walk (written ⇒).
- Prove that X beta-reduce* Y iff X ⇒* Y
- Prove that ⇒ has the diamond property.
Finally, we'll prove that ⇒* (a sequence of zero or more walks) has the diamond property, and we'll use that to "fill in the diamond" and thus to prove the Church-Rosser Theorem.
Definition (walk): A walk is a sequence of zero or more beta-reductions restricted as follows:
- If the ith reduction in the sequence reduces a redex r, then no later reduction in the sequence can reduce an instance of a redex that was inside r; i.e., reductions must be done bottom-up in the abstract-syntax tree.
Here are some examples (again, * means a redex that reduces to y):
(λx.xx)(*) | | v (λx.xx)y | | v yyThis entire reduction sequence (2 beta-reductions) is a walk because the inner redex is reduced first. Here's what the reductions look like using the abstract-syntax tree:
apply apply apply / \ / \ / \ λ * λ y y y / \ --> / \ --> x apply x apply / \ / \ x x x xHowever, consider this sequence of beta-reductions (starting with the same initial term), first showing the lambda terms, then the abstract-syntax trees:
(λx.xx)(*) | | v (**) | | v (y*) | | v (yy) apply apply apply apply / \ / \ / \ / \ λ * * * y * y y / \ --> --> --> x apply / \ x x ==> =======================> this step is a these two steps constitute a walk walkAlthough as noted above, the first beta-reduction is a walk, and the second and third together are also a walk, the sequence of three reductions is not a walk because once the root "apply" is chosen to be reduced (which happens as the first reduction), no apply in the tree can be reduced as part of the same walk (so the reductions of the two "*" terms are illegal).
Here are two important insights about walks:
- You can't always concatenate two walks and get a walk (i.e., walk is not a transitive relation).
- Two walks that reduce non-overlapping redexes can be concatenated to form a walk.
NOTE: We've now accomplished task (1) toward proving the Church-Rosser Theorem.
Task 2 involves proving that (X beta-reduce* Y) iff (X walk* Y).
The => direction is trivial; we must show that every sequence of zero or more beta-reductions is also a sequence of walks. Since each individual beta-reduction is a walk, we just let the sequence of walks be exactly the sequence of beta-reductions.
The <= direction is easy, too. Every walk is a sequence of zero or beta-reductions. So every sequence of walks is a concatenation of sequences of beta-reductions, which is itself a sequence of beta-reductions.
For task 3 of our proof of the Church-Rosser Theorem we must prove a lemma that says that the walk relation has the diamond property. We'll call that CRT Lemma 2, because to do that proof we first need another lemma:
CRT Lemma 1 (the walk relation is preserved when free variables are replaced by terms): if (X ⇒ Y) then (X[P/x] ⇒ Y[P/x])
(Note: X ⇒ Y means "X walk Y", and X[P/x] means X with the free occurrences of x replaced by P without capture.)
We won't give a formal proof of the Lemma; instead we'll convince ourselves by considering what happens to the free occurrences of x in X when X ⇒ Y (remember that X ⇒ Y means zero or more of the redexes in X are reduced bottom-up):
- A free occurrence of x can be in the body of a function that is a part of a redex that is reduced as part of X ⇒ Y. In this case, the occurrence of x continues to be free after reduction. So if that occurrence of x is replaced by P before the reduction we get the same thing as if it is replaced by P after the reduction.
- A free occurrence of x can be in an argument that is a part of a redex that is reduced as part of X ⇒ Y. There are two subcases:
(i) If x is "ignored" by the function part of the redex, (i.e., the function body does not include any occurrences of its formal parameter) then there will be no occurrences of x after the reduction, so replacing occurrences of x with P after the reduction is an empty operation; similarly, if we replace x with P before the reduction there will be NO occurrences of P after the reduction. Thus, it doesn't matter if we do the substitution before or after.
(ii) If x is not ignored, then there will be one or more occurrences of x after the reduction; if the x's are replaced with P's before the reduction then there will be the same number of P's after the reduction. Note that these occurrences of x cannot be themselves reduced when X ⇒ Y, because the x's are variables, not applications. So again we get the same thing by doing the substitution before or after the reduction.
Show that CRT Lemma 1 is not iff; i.e., find an example X, Y, and P such that (X[P/x] ⇒ Y[P/x]) but it is not true that (X ⇒ Y).
Now we can prove CRT Lemma 2.
CRT Lemma 2 ( ⇒ has the diamond property): if (X0 ⇒ X1) and (X0 ⇒ X2) then there is an X3 such that (X1 ⇒ X3) and (X2 ⇒ X3).
Pictorially, Lemma 2 says that given X0, X1, and X2 with the following relationship (where the diagonal lines mean a walk):
Base case: X0 is a variable (i.e., the height of the tree = 1).
In this case, to get from X0 to X1 or from X0 to X2 must require zero reductions (since a variable has no redexes). So X0 = X1 = X2, and the X3 we're looking for is the same thing, too: X0 = X3.
Inductive Step: Assume that CRT Lemma 2 holds for all lambda terms X0 with abstract-syntax tree of height less than or equal to n; show that it holds for all terms of height n+1. Note that there are two ways to get a lambda term of height n+1:
X0 = λx.M0 // \\ v v X1 = λx.M1 X2 = λx.M2By the induction hypothesis there exists an M3 such that:
M1 M2 \\ // v v M3since the height of M0 is n. By choosing X3 = λx.M3, the lemma is proved for this case.
X0 = M0 N0 // \\ v v X1 = M1 N1 X2 = M2 N2By the induction hypothesis, there exist M3 and N3 such that:
M1 M2 N1 N2 \\ // and \\ // v v v v M3 N3Since the walks M1 ⇒ M3 and N1 ⇒ N3 involve non-overlapping redexes, they can be concatenated to produce a walk, and similarly for M2, N2. Thus, we can choose X3 = M3 N3, and the lemma is proved for this case:
X0 = M0 N0 // \\ v v X1 = M1 N1 X2 = M2 N2 \\ // v v M3 N3
Case 2.2: Both X1 and X2 reduce the root 'apply'.
For this to happen, the root apply must be a redex; i.e., M0 must be of the form (λy.W0), which makes X0 of the form (λy.W0)(N0). Also, by the definition of walk, reduction of the root apply must be the last step in the walks from X0 to X1 and from X0 to X2, with earlier reductions walking from W0 to W1 and W2, and from N0 to N1 and N2. Pictorially:
By the induction hypothesis, there exists an N3 such that:
N0 // \\ v v N1 N2 \\ // v v N3
Claim: W1[N1/y] ⇒ W1[N3/y]
Justification: The form of W1[N1/y] is:
/\ / \ / \ /\ /\ /\ N1 N1 N1i.e., in its abstract-syntax tree, all of the N1's are at the "bottom" and do not overlap, because the y's in W1 were leaves.
This means that we can concatenate walks from each of the N1's to an N3 to get a walk on the entire tree (W1[N1/y]) that takes all of the N1's to N3's. Pictorially we have:
/\ /\ /\ /\ / \ / \ / \ / \ / \ ==> / \ ==> / \ ==>... / \ /\ /\ /\ /\ /\ /\ /\ /\ /\ /\ /\ /\ N1 N1 N1 N3 N1 N1 N3 N3 N1 N3 N3 N3and the whole thing is itself a walk: W1[N1/y] ⇒ W1[N3/y].
Similarly W1[N2/y] => W1[N3/y]. Now we have:
By the induction hypothesis there exists a W3 such that:
W1 W2 \\ // v v W3And by Lemma 1:
- because W1 ⇒ W3, it must be that W1[N3/y] ⇒ W3[N3/y], and
- because W2 ⇒ W3, it must be that W2[N3/y] ⇒ W3[N3/y].
None of the beta-reductions used to walk from W1[N3/y] to W3[N3/y] takes place inside an N3; therefore, we can combine the "W" walk and the "N" walk to get a walk; i.e., given:
W1[N1/y] ⇒ W1[N3/y] ⇒ W3[N3/y] ^ ^ | | all reductions all reductions are inside N1s are above N3swe have:
W1[N1/y] ⇒ W3[N3/y]Here's the final picture:
By choosing X3 = W3[N3/y], the lemma is proved for this case.
Case 2.3: Exactly one of X1 and X2 (say X1) reduces the root 'apply'.
As for case 2.2., for this to happen X0 must be of the form (Ly.W0)(N0). Pictorially:
By the induction hypothesis, there must be an N3 and a W3 such that the following pictures hold:
W0 N0 // \\ // \\ v v v v W1 W2 N1 N2 \\ // \\ // v v v v W3 N3Now we're ready to put the pictures together:
Here's an explanation of each of the labeled transitions:
- This is the same as for case 2.2: N1 ⇒ N3, and the N1's in W1[N1/y] are non-overlapping, so we can concatenate the walks that turn all N1's to N3's to form a single walk.
- We know that W2 ⇒ W3 and N2 ⇒ N3, and W2 and N2 don't overlap, so we can concatenate the walks to get this (single) walk.
- Same as for case 2.2 (using Lemma 1).
- This is a normal (single) beta-reduction.
- The concatenation of walks (1) and (3) is a walk because reductions are bottom-up (same as case 2.2).
- Walk (2) followed by beta-reduction (4) is a walk because the final reduction is at the root (so it obeys the "bottom-up" restriction in the definition of a walk).
Now that we've accomplished our three tasks, it remains to show that ⇒* has the diamond property, and to use that fact to prove the original theorem.
In fact, it can be shown that given any relation ~~> that has the diamond property, ~~>* also has the diamond property. That is left as an exercise; we will give an informal argument here.
We want to show that for given a lambda term X0 such that X0 ⇒* X1, and X0 ⇒* X2, there exists an X3 such that X1 ⇒* X3, and X2 ⇒* X3. Pictorially, we have:
X0 // \\ v v W1 Z1 // \\ v v ... ... // \\ v v X1 X2and we want to show:
X0 // \\ v v W1 Z1 // \\ v v ... ... // \\ v v X1 X2 \\ // v v ... ... \\ // \\ // v v X3Since we know that each individual walk has the diamond property, we can "fill in the diamonds" as shown below, creating a sequence of walks from both X1 to X2, and X2 to X3:
X0 // \\ W1 Z1 // \\ // \\ W2 A Z2 //\\ // \\ // \\ W3 B C Z3 //\\//\\ // \\ // \\ ... ... ... ... ... ... ... //\\//\\ // \\ // \\ //\\ X1 X2 \\ ... // ... ... ... ... ... ... ... \\ // X3
Now for the final proof of the Theorem. Recall that we need to show that if (X0 red X1) and (X2 red X2), then there is an X3 such that (X1 red X3) and (X2 red X3). Task 2 showed that (X0 red X1) implies that (X0 ⇒* X1), and similarly for X2; in other words, we can get from X0 to either X1 or X2 using a sequence of walks. Since ⇒* has the diamond property, this means that we can also get from either X1 or X2 to X3 using a sequence of walks, and we have:
- (X0 ⇒* X1) and (X0 ⇒* X2) and (X1 ⇒* X3) and (X2 ⇒* X2).
Using the result of task 2 again, we note that a sequence of walks is also a sequence of beta reductions, so (X1 ⇒* X3) implies (X1 red X3), and similarly for X2, and so we're done!
Source: https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html
0 Response to "Lambda Calculus Draw Parse Tree"
Post a Comment