0=1 n!=n.(n-1l.ifn≠0. The encoding of such functions in the lambda calculus is the subject of the next section.It is related to the concept of a fixpoint. 3.3 Fixpoints and recursive functions Supposefisafunction.We say( has ints 0 and 1 whe 1 has The lambda calculus contrasts with arithmetic in that every lambda term has a fixpoint.This is perhaps the first surprising fact about the lambda calculus we learn in this course. Theorem 3.1.In the untyped lambda calculus.every term F has afixpoint. N- OF AAF =(Ary.v())AF 8 F(A ◇ The termused in the proof is called Tring'sfixpoint combinator. f().This covers equations with an arbitrary right-hand side whose eft hand side is.From the above theorem,we know that we can always solve such equations in the lambda calculus. 21
we need is a mechanism for defining more complicated functions from simple ones. Consider for example the factorial function, defined by: 0! = 1 n! = n · (n − 1)!, if n 6= 0. The encoding of such functions in the lambda calculus is the subject of the next section. It is related to the concept of a fixpoint. 3.3 Fixpoints and recursive functions Suppose f is a function. We say that x is a fixpoint of f if f(x) = x. In arithmetic and calculus, some functions have fixpoints, while others don’t. For instance, f(x) = x 2 has two fixpoints 0 and 1, whereas f(x) = x + 1 has no fixpoints. Some functions have infinitely many fixpoints, notably f(x) = x. We apply the notion of fixpoints to the lambda calculus. If F and N are lambda terms, we say that N is a fixpoint of F if F N =β N. The lambda calculus contrasts with arithmetic in that every lambda term has a fixpoint. This is perhaps the first surprising fact about the lambda calculus we learn in this course. Theorem 3.1. In the untyped lambda calculus, every term F has a fixpoint. Proof. Let A = λxy.y(xxy), and define Θ = AA. Now suppose F is any lambda term, and let N = ΘF. We claim that N is a fixpoint of F. This is shown by the following calculation: N = ΘF = AAF = (λxy.y(xxy))AF → β F(AAF) = F(ΘF) = F N. The term Θ used in the proof is called Turing’s fixpoint combinator. The importance of fixpoints lies in the fact that they allow us to solve equations. After all, finding a fixpoint for f is the same thing as solving the equation x = f(x). This covers equations with an arbitrary right-hand side, whose lefthand side is x. From the above theorem, we know that we can always solve such equations in the lambda calculus. 21
To see how to apply this idea,consider the question from the last section,namely fact n if then_else(iszero n)(I)(mult n(fact(pred n))) Here we have used various abbreviations for lambda terms that were introduced in and the right- fact Xn.if then-else (iszero n)(1)(mult n(fact (pred n))) fact (Af.An.if_then_else (iszero n)(1(mult n(f(pred n))))fact Let us temporarily write Ffor the term Af.Xn.if-then-else (iszero n)(T)(mult n(f(predn))) Then the last equation becomes fact=Ffact,which is a fixpoint equation.We can solve it up to B-equivalence,by letting act二f.if then.lse (iszero①mult n(f(pred Note that fact has disappeared from the right-hand side.The right-hand side is a represen factorial function.(A lambda term is calle fact 2→ →a if then else(iszero2(①(muh2(fact(pred) a if then_else(F)(1)(mult 2(fact(pred 2)) 8 mu ct(pred 2)) a mult 2(F fast T →mult2 mult I(act) mul else (isz
To see how to apply this idea, consider the question from the last section, namely, how to define the factorial function. The most natural definition of the factorial function is recursive, and we can write it in the lambda calculus as follows: fact n = if then else (iszero n)(1)(mult n(fact(pred n))) Here we have used various abbreviationsfor lambda terms that were introduced in the previous section. The evident problem with a recursive definition such as this one is that the term to be defined, fact, appears both on the left- and the right-hand side. In other words, to find fact requires solving an equation! We now apply our newfound knowledge of how to solve fixpoint equations in the lambda calculus. We start by rewriting the problem slightly: fact = λn. if then else (iszero n)(1)(mult n(fact(pred n))) fact = (λf.λn. if then else (iszero n)(1)(mult n(f(pred n))))fact Let us temporarily write F for the term λf.λn. if then else (iszero n)(1)(mult n(f(pred n))). Then the last equation becomes fact = F fact, which is a fixpoint equation. We can solve it up to β-equivalence, by letting fact = ΘF = Θ(λf.λn. if then else (iszero n)(1)(mult n(f(pred n)))) Note that fact has disappeared from the right-hand side. The right-hand side is a closed lambda term that represents the factorial function. (A lambda term is called closed if it contains no free variables). To see how this definition works in practice, let us evaluate fact 2. Recall from the proof of Theorem 3.1 that ΘF → β F(ΘF), therefore fact → β F fact. fact 2 → β F fact 2 → β if then else (iszero 2)(1)(mult 2(fact(pred 2))) → β if then else (F)(1)(mult 2(fact(pred 2))) → β mult 2(fact(pred 2)) → β mult 2(fact 1) → β mult 2(F fact 1) → β . . . → β mult 2(mult 1(fact 0)) → β mult 2(mult 1(F fact 0)) → β mult 2(mult 1(if then else (iszero 0)(1)(mult 2(fact(pred 2))))) → β mult 2(mult 1(if then else (T)(1)(mult 2(fact(pred 2))))) 22
二2h2maT可 nul3 nd f atter of simple induction to prove that fact-a元，for any n. Exereise 8.Write a lambda term that represents the Fibonacci function,defined by f(0)=1,f(1)=1.f(n+2)=f(n+1)+f(n),forn≥2 te the che Exereise 10.We have remarked at the beginning of this section that the number- theoretic function f()=+1 does not have a fixpoint.On the other hand,the em 3 1.He r,which represents th ow can you reconcile the two sta noint combinator for the lambda calculu fixpoint combinator,is the term Y=Xf.(Xr.f(x))(xz.f(r)). s indeed a fixpoint combinator,ie.,that YF is a fixpoint of oforDehafeet the (c)Can you find another fixpoint combinator,besides Curry's and Turing's? 3.4 Other datatypes:pairs,tuples,lists,trees,etc. So far,we have discussed lambda terms that represented functionson boolean I nu ber s.H ly possible to e e genera ople with 23
→ β mult 2(mult 1 1) → β 2 Note that this calculation, while messy, is completely mechanical. You can easily convince yourself that fact 3 reduces to mult 3(fact 2), and therefore, by the above calculation, to mult 3 2, and finally to 6. It is now a matter of a simple induction to prove that fact n → β n!, for any n. Exercise 8. Write a lambda term that represents the Fibonacci function, defined by f(0) = 1, f(1) = 1, f(n + 2) = f(n + 1) + f(n), for n > 2 Exercise 9. Write a lambda term that represents the characteristic function of the prime numbers, i.e., f(n) = true if n is prime, and false otherwise. Exercise 10. We have remarked at the beginning of this section that the numbertheoretic function f(x) = x + 1 does not have a fixpoint. On the other hand, the lambda term F = λx.succ x, which represents the same function, does have a fixpoint by Theorem 3.1. How can you reconcile the two statements? Exercise 11. The first fixpoint combinator for the lambda calculus was discovered by Curry. Curry’s fixpoint combinator, which is also called the paradoxical fixpoint combinator, is the term Y = λf.(λx.f(xx))(λx.f(xx)). (a) Prove that this is indeed a fixpoint combinator, i.e., that YF is a fixpoint of F, for any term F. (b) Turing’s fixpoint combinator not only satisfies ΘF =β F(ΘF), but also ΘF → β F(ΘF). We used this fact in evaluating fact 2. Does an analogous property hold for Y? Does this affect the outcome of the evaluation of fact 2? (c) Can you find another fixpoint combinator, besides Curry’s and Turing’s? 3.4 Other datatypes: pairs, tuples, lists, trees, etc. So far, we have discussed lambda terms that represented functions on booleans and natural numbers. However, it is easily possible to encode more general data structures in the untyped lambda calculus. Pairs and tuples are of interest to everybody. The examples of lists and trees are primarily interesting to people with 23
experience in a list-processing language such as LISPor PROLOG:you can safely ignore these examples if you want to. Pairs.If Mand N are lambda terms,we define the pair(M,N)to be the lambda 男e9de The terms left and right are called the left and right projections Tuples.The encoding of pairs easily extends to arbitrary n-tuples.If M..M are terms,we define the n-tuple()as the lambda termM and we define the ith projection=Ap.p(Ar...n).Then n(M1,,Mn〉*gM,for all1≤i≤n. Lists.A list is different from a tuple,because its length is not necessarily fixed rst element (th for the list whose head is and whose So.for instance the ist of the first three numbers can be written as 1::(2::(3::nil)).We usually omit the here it is understood that"::"associates to the right.Note that every addlist I=I(ht.add h(addlist ))(0) Of course.this is a recursive definition.and must be translated into an actual lambdaterm by the method of Section3.3.In the definition of addlist,I andt are r.I you are very diligent,y ou can calculate th addlist(:2亚：2：3：亚：：nil) binary digits o and 1.Of course.with this encoding we would have to care fully redesign our basic functions,such as successor,addition,and multiplication
experience in a list-processing language such as LISP or PROLOG; you can safely ignore these examples if you want to. Pairs. If M and N are lambda terms, we define the pair hM, Ni to be the lambda term λz.zMN. We also define two terms left = λp.p(λxy.x) and right = λp.p(λxy.y). We observe the following: lefthM, Ni → β M righthM, Ni → β N The terms left and right are called the left and right projections. Tuples. The encoding of pairs easily extends to arbitrary n-tuples. If M1, . . . , Mn are terms, we define the n-tuple hM1, . . . , Mni as the lambda term λz.zM1 . . . Mn, and we define the ith projection π n i = λp.p(λx1 . . . xn.xi). Then π n i hM1, . . . , Mni → β Mi , for all 1 6 i 6 n. Lists. A list is different from a tuple, because its length is not necessarily fixed. A list is either empty (“nil”), or else it consists of a first element (the “head”) followed by another list (the “tail”). We write nil for the empty list, and H :: T for the list whose head is H and whose tail is T. So, for instance, the list of the first three numbers can be written as 1 :: (2 :: (3 :: nil)). We usually omit the parentheses, where it is understood that ”::” associates to the right. Note that every list ends in nil . In the lambda calculus, we can define nil = λxy.y and H :: T = λxy.xHT. Here is a lambda term that adds a list of numbers: addlist l = l(λh t. add h(addlist t))(0). Of course, this is a recursive definition, and must be translated into an actual lambda term by the method of Section 3.3. In the definition of addlist , l and t are lists of numbers, and h is a number. If you are very diligent, you can calculate the sum of last weekend’s Canadian lottery results by evaluating the term addlist(4 :: 22 :: 24 :: 32 :: 42 :: 43 :: nil). Note that lists enable us to give am alternative encoding of the natural numbers: We can encode a natural number as a list of booleans, which we interpret as the binary digits 0 and 1. Of course, with this encoding, we would have to carefully redesign our basic functions, such as successor, addition, and multiplication. 24
numerals write leaf (for a leaf labeled N.and node (R)for a node with left subtree and right subtree R.We can encode trees as lambda terms.for instance as follows leaf(n）=入xu.xn. node(L.R)=入cu.vLR e (m addtree=(nn)(Ir.add(addtree 1)(addtree)) Exercise 12.This is a voluntary programming exercise. (a)Writea lambda term that calculates the length of a list. (b)Write a lambda term that calculates the depth(i.e,the nesting level)of a tree.You may need to define a function max that calculates the maximum of two numbers. (e)Wefmbs You maymna term less at compares two numbers. 4 The Church-Rosser Theorem 4.1 Extensionality,-equivalence,and n-reduction In the untyped lambda calculus,any term can be applied to another term.There- fore,any term can be rega rded as a u der a term M,not containing se,and M'define"the sme function Should M andMbe considered equivalent as terms? t to accent the le that "if v and M 25
However, if done properly, such an encoding would be a lot more efficient (in terms of number of β-reductions to be performed) than the encoding by Church numerals. Trees. A binary tree is a data structure that can be one of two things: either a leaf, labeled by a natural number, or a node, which has a left and a right subtree. We write leaf(N) for a leaf labeled N, and node (L, R) for a node with left subtree L and right subtree R. We can encode trees as lambda terms, for instance as follows: leaf(n) = λxy.xn, node (L, R) = λxy.yLR As an illustration, here is a program (i.e., a lambda term) that adds all the numbers at the leafs of a given tree. addtree t = t(λn.n)(λl r. add (addtree l)(addtree r)). Exercise 12. This is a voluntary programming exercise. (a) Write a lambda term that calculates the length of a list. (b) Write a lambda term that calculates the depth (i.e., the nesting level) of a tree. You may need to define a function max that calculates the maximum of two numbers. (c) Write a lambda term that sorts a list of numbers. You may assume given a term less that compares two numbers. 4 The Church-Rosser Theorem 4.1 Extensionality, η-equivalence, and η-reduction In the untyped lambda calculus, any term can be applied to another term. Therefore, any term can be regarded as a function. Consider a term M, not containing the variable x, and consider the term M0 = λx.Mx. Then for any argument A, we have MA =β M0A. So in this sense, M and M0 define “the same function”. Should M and M0 be considered equivalent as terms? The answer depends on whether we want to accept the principle that “if M and M0 define the same function, then M and M0 are equal”. This is called the principle 25