of extensionaliry,and we have already encountered it in Section 1.1.Formally,the extensionality rule is the following: ( In the presence of the axioms (5)(cong)and (B)it can be easily seen that MA= M'A is true for all terms A ifand only if M=M',where is a fresh variable. Therefore,we can replace the extensionality rule by the following equivalent,but simpler rule: (em ereFV(M.业 marked ab and thus extensionality implies thatM.This last equation is called the -law (eta-law): (n)M=Ar.Mr.where r FV(M). In fact,(and (ex)are equivalent in the presence of the other axioms of the lambda calculu We hav dy see and (imply可 transitivity M=M'Thus (ert)holds and rules of the lambda are not -quivalent,although they are clearly quivalent.Wewill prove that a Ay.ry in Corollary 4.5 below. Single-step n-reduction is the smallest relation-satisfving (c ()and the following axiom(which is the same as the w,directed right to Ieft): (n)Ar.Mrn M,wherer FV(M) Single-step B-reduction uction mul l-step B-reductior an,as well as
of extensionality, and we have already encountered it in Section 1.1. Formally, the extensionality rule is the following: (ext∀) ∀A.MA = M0A M = M0 . In the presence of the axioms (ξ), (cong), and (β), it can be easily seen that MA = M0A is true for all terms A if and only if Mx = M0x, where x is a fresh variable. Therefore, we can replace the extensionality rule by the following equivalent, but simpler rule: (ext) Mx = M0x, where x 6∈ FV (M, M0 ) M = M0 . Note that we can apply the extensionality rule in particular to the case where M0 = λx.Mx, where x is not free in M. As we have remarked above, Mx =β M0x, and thus extensionality implies that M = λx.Mx. This last equation is called the η-law (eta-law): (η) M = λx.Mx, where x 6∈ FV (M). In fact, (η) and (ext) are equivalent in the presence of the other axioms of the lambda calculus. We have already seen that (ext) and (β) imply (η). Conversely, assume (η), and assume that Mx = M0x, for some terms M and M0 not containing x freely. Then by (ξ), we have λx.Mx = λx.M0x, hence by (η) and transitivity, M = M0 . Thus (ext) holds. We note that the η-law does not follow from the axioms and rules of the lambda calculus that we have considered so far. In particular, the terms x and λy.xy are not β-equivalent, although they are clearly η-equivalent. We will prove that x 6=β λy.xy in Corollary 4.5 below. Single-step η-reduction is the smallest relation →η satisfying (cong1), (cong2), (ξ), and the following axiom (which is the same as the η-law, directed right to left): (η) λx.Mx →η M, where x 6∈ FV (M). Single-step βη-reduction →βη is defined as the union of the single-step β- and η-reductions, i.e., M →βη M0 iff M →β M0 or M →η M0 . Multi-step η- reduction → η, multi-step βη-reduction → βη, as well as η-equivalence =η and βη-equivalence =βη are defined in the obvious way as we did for β-reduction and equivalence. We also get the evident notions of η-normal form, βη-normal form, etc. 26
4.2 Statement of the Church-Rosser Theorem,and some con- sequences In pictures,the theorem states that the following diagram can always be com- pleted: Corollary 4.1.If M=a N then there exists some Z with M,N-a Z.Similarly or知. Proof Please refer to Figure I for an illustration of this proof Recall that se that M=3 N.Then 8 M: e prove the exis sts a term Z'such that M-a Z'and Mn-18 Z'.Further. we know tha either N case A 84 The to 7 and N identical. If N is a B-normal form and N =8 M,then M-B N,and Pody Cooll4 ereome曲MN一9.五BaNr日 normal form,thus N =2
4.2 Statement of the Church-Rosser Theorem, and some consequences Theorem (Church and Rosser, 1936). Let → denote either → β or → βη. Suppose M, N, and P are lambda terms such that M → N and M → P. Then there exists a lambda term Z such that N → Z and P → Z. In pictures, the theorem states that the following diagram can always be completed: M ? ? ? ? ? P N Z This property is called the Church-Rosser property, or confluence. Before we prove the Church-Rosser Theorem, let us highlight some of its consequences. Corollary 4.1. If M =β N then there exists some Z with M, N → β Z. Similarly for βη. Proof. Please refer to Figure 1 for an illustration of this proof. Recall that =β is the reflexive symmetric transitive closure of →β. Suppose that M =β N. Then there exist n > 0 and terms M0, . . . , Mn such that M = M0, N = Mn, and for all i = 1 . . . n, either Mi−1 →β Mi or Mi →β Mi−1. We prove the claim by induction on n. For n = 0, we have M = N and there is nothing to show. Suppose the claim has been proven for n−1. Then by induction hypothesis, there exists a term Z 0 such that M → β Z 0 and Mn−1 → β Z 0 . Further, we know that either N →β Mn−1 or Mn−1 →β N. In case N →β Mn−1, then N → β Z 0 , and we are done. In case Mn−1 →β N, we apply the Church-Rosser Theorem to Mn−1, Z 0 , and N to obtain a term Z such that Z 0 → β Z and N → β Z. Since M → β Z 0 → β Z, we are done. The proof in the case of βη-reduction is identical. Corollary 4.2. If N is a β-normal form and N =β M, then M → β N, and similarly for βη. Proof. By Corollary 4.1, there exists some Z with M, N → β Z. But N is a normal form, thus N =α Z. 27
Figure 1:The proofof Corollary 4.1 y Corollaryehave bt sinesfo have M=a N. n4N=水en xikrorkoi honea6mSaa Proof Suppose that M =a N.and that one of them has a B-normal form.Say aoag2 that M has a normal form乙.Then N=a乙，hence N一aZby for instanc ■ Pof The emhmal forms and they are not equivalent.It follows by Corollary 4.3 thaty.y 28
M5 ? ? ? ? ? M6 ? ? ? ? ? M7 M3 ? ? ? ? ? M4 M2 M0 ? ? ? ? ? M1 Z 00 Z 0 Z Figure 1: The proof of Corollary 4.1 Corollary 4.3. If M and N are β-normal forms such that M =β N, then M =α N, and similarly for βη. Proof. By Corollary 4.2, we have M → β N, but since M is a normal form, we have M =α N. Corollary 4.4. If M =β N, then neither or both have a β-normal form. Similarly for βη. Proof. Suppose that M =β N, and that one of them has a β-normal form. Say, for instance, that M has a normal form Z. Then N =β Z, hence N → β Z by Corollary 4.2. Corollary 4.5. The terms x and λy.xy are not β-equivalent. In particular, the η-rule does not follow from the β-rule. Proof. The terms x and λy.xy are both β-normal forms, and they are not α- equivalent. It follows by Corollary 4.3 that x 6=β λy.xy. 28
Preliminary remarks on the proof of the Church-R Consider any binary relation-on a set.and let-be its reflexitive transitive closure.Consider the following three properties of such relations: (a (b) (c) Each of these properties states that for all M.N.P.if the solid arrows exist,then there exists Zsuch that the dotted arrows exist.The only difference between(a). (b).and (c)is the difference between where-and-are used. es品)cde A naive attemnt to pr First.prove that the relation satisfies prop use an inductive argument to conclude that it also satisfies pro Unfortunately,this does not work:the reason is that in general,property (b)does not imply property(a)!An example ofa relation that satisfies property(b)but not wn in Figure other words,a proof of property (b)is no e to prove property (a) On the other hand,property (c).the diamond property,does imply property(a) the proo in Figure s not satisfy property (c).so again To summarize,we are faced with the following dilemma: B-reduction satisfies property (b).but property(b)does not imply property .Property(c)implies property (a)but -reduction does not satisfy property (c. On the other hand,it seems hopeless to prove property (a)directly.In the next
4.3 Preliminary remarks on the proof of the Church-Rosser Theorem Consider any binary relation → on a set, and let → be its reflexitive transitive closure. Consider the following three properties of such relations: (a) M ? ? ? ? ? P N Z (b) M ? ? ? ? ? P N Z (c) M ? ? ? ? ? P N Z Each of these properties states that for all M, N, P, if the solid arrows exist, then there exists Z such that the dotted arrows exist. The only difference between (a), (b), and (c) is the difference between where → and → are used. Property (a) is the Church-Rosser property. Property (c) is called the diamond property (because the diagram is shaped like a diamond). A naive attempt to prove the Church-Rosser Theorem might proceed as follows: First, prove that the relation →β satisfies property (b) (this is relatively easy to prove); then use an inductive argument to conclude that it also satisfies property (a). Unfortunately, this does not work: the reason is that in general, property (b) does not imply property (a)! An example of a relation that satisfies property (b) but not property (a) is shown in Figure 2. In other words, a proof of property (b) is not sufficient in order to prove property (a). On the other hand, property (c), the diamond property, does imply property (a). This is very easy to prove by induction, and the proof is illustrated in Figure 3. But unfortunately, β-reduction does not satisfy property (c), so again we are stuck. To summarize, we are faced with the following dilemma: • β-reduction satisfies property (b), but property (b) does not imply property (a). • Property (c) implies property (a), but β-reduction does not satisfy property (c). On the other hand, it seems hopeless to prove property (a) directly. In the next 29
Figure 2:An example of a relation that satisfies property (b),but not property (a) Figure3:Proofthat property(c)implies property (a
• @ @ @ @ • ~ ~ ~ ~ @ @ @ @ • @ @ @ @ • ~ ~ ~ ~ • ~ ~ ~ ~ @ @ @ @ • ~ ~ ~ ~ • @ @ @ @ • ~ ~ ~ ~ @ @ @ @ • @ @ @ @ • ~ ~ ~ ~ • ~ ~ ~ ~ @ @ @ @ • ~ ~ ~ ~ • @ @ @ @ • ~ ~ ~ ~ @ @ @ @ • @ @ @ @ • ~ ~ ~ ~ • ~ ~ ~ ~ @ @ @ @ • ~ ~ ~ ~ • @ @ @ @ • ~ ~ ~ ~ @ @ @ @ • @ @ @ @ • • : : : : : : • . . . . . . . . . Figure 2: An example of a relation that satisfies property (b), but not property (a) • ? ? ? • ? ? ? • ? ? ? • • • • • • • • • • • • • • • • • Figure 3: Proof that property (c) implies property (a) 30