2.4 Introduction to B-reduction Convention.From now on unless stated otherwise.we identify lambda terms ur to a-equivalence.This means,when we speak of lambda terms being"equal we mean that they are qivalent.Formally,we regard lambda terms as equivalenc We will often use the ordinary equality symbo The process of evaluating lambd "into function nlied to emm of 3-nedar We MNand we call the later term the.We reduc ambda terms by finding a subterm that is a redex,and then replacing that redex by its reduct.We any B-redexes is sai eekeoea0e2eaeaisam 一4 The last term. has no redexes and is thus in normal form.We could reduce the same term differently,by choosing the redexes ina different order (xy(之.2zA.w2一g. As we can see from this example: reducinga redex can create new redexes -reducinga redex can delete some other redexes the number of steps that it takes to reach a normal form can vary,depending on the order in which the redexes are reduced. We can also see that the final result u does not seem to depend on the order in which the redexes are reduced.In fact,this is true in general,as we will prove later. If A and A'are terms such that A-A'and if M'is in normal form.then we say that M evaluates to M' 6
2.4 Introduction to β-reduction Convention. From now on, unless stated otherwise, we identify lambda terms up to α-equivalence. This means, when we speak of lambda terms being “equal”, we mean that they are α-equivalent. Formally, we regard lambda terms as equivalence classes modulo α-equivalence. We will often use the ordinary equality symbol M = N to denote α-equivalence. The process of evaluating lambda terms by “plugging arguments into functions” is called β-reduction. A term of the form (λx.M)N, which consists of a lambda abstraction applied to another term, is called a β-redex. We say that it reduces to M[N/x], and we call the latter term the reduct. We reduce lambda terms by finding a subterm that is a redex, and then replacing that redex by its reduct. We repeat this as many times as we like, or until there are no more redexes left to reduce. A lambda term without any β-redexes is said to be in β-normal form. For example, the lambda term (λx.y)((λz.zz)(λw.w)) can be reduced as follows. Here, we underline each redex just before reducing it: (λx.y)((λz.zz)(λw.w)) →β (λx.y)((λw.w)(λw.w)) →β (λx.y)(λw.w) →β y. The last term, y, has no redexes and is thus in normal form. We could reduce the same term differently, by choosing the redexes in a different order: (λx.y)((λz.zz)(λw.w)) →β y. As we can see from this example: - reducing a redex can create new redexes, - reducing a redex can delete some other redexes, - the number of steps that it takes to reach a normal form can vary, depending on the order in which the redexes are reduced. We can also see that the final result, y, does not seem to depend on the order in which the redexes are reduced. In fact, this is true in general, as we will prove later. If M and M0 are terms such that M → β M0 , and if M0 is in normal form, then we say that M evaluates to M0 . 16
(Ar.zz)(Av-VWW) → This example aso shows that the size of a lambda temdot deresedn reach a normal form. that doc 2.5 Formal defi nitions of B-reduction and B-equivalence The concept ofreduction can be defined formally as follows Definition.We define single-step B-reduction to be the smallest relationon terms satisfying: ( Az.MON→MN M→+g" (cong1) MN→aAN (cong2) N→ay MN→aMN () M-8 M Ar.M-8 Xr.M Thus,MM'iff Mis obtained from M by reducing a single B-redex of M. Definition.We write MM if M reduces to inzero more steps e the rene xive transitive closure of-,1.e.,the Finally,Bqivalence is obtained by allowing reduction steps as well as inverse reduction steps,i.e.,by makings symmetric: Definition.We write M=M'if M can be transformed into M'by is defined to be the reflexive symmetric transitive closure ofie.,the smallest equivalence relation containing-a. 1
Not every term evaluates to something; some terms can be reduces forever without rachine a normal form. The following is an example: (λx.xx)(λy.yyy) →β (λy.yyy)(λy.yyy) →β (λy.yyy)(λy.yyy)(λy.yyy) →β . . . This example also shows that the size of a lambda term need not decrease during reduction; it can increase, or remain the same. The term (λx.xx)(λx.xx), which we encountered in Section 1, is another example of a lambda term that does not reach a normal form. 2.5 Formal definitions of β-reduction and β-equivalence The concept of β-reduction can be defined formally as follows: Definition. We define single-step β-reduction to be the smallest relation →β on terms satisfying: (β) (λx.M)N →β M[N/x] (cong1) M →β M0 MN →β M0N (cong2) N →β N0 MN →β MN0 (ξ) M →β M0 λx.M →β λx.M0 Thus, M →β M0 iff M0 is obtained from M by reducing a single β-redex of M. Definition. We write M → β M0 if M reduces to M0 in zero or more steps. Formally, → β is defined to be the reflexive transitive closure of →β, i.e., the smallest reflexive transitive relation containing →β. Finally, β-equivalence is obtained by allowing reduction steps as well as inverse reduction steps, i.e., by making →β symmetric: Definition. We write M =β M0 if M can be transformed into M0 by zero or more reduction steps and/or inverse reduction steps. Formally, =β is defined to be the reflexive symmetric transitive closure of →β, i.e., the smallest equivalence relation containing →β. 17
Exercise 4.This definition of B-equivalence is slightly different from the one given in class.Prove that they are in fact the same 3 Programming in the untyped lambda calculus One of the amazing facts about the untyped lambda calculus is that we can use it to encode data,such as booleans and natural numbers,as well as programs that We will often have occasion to give names to particular lambda terms;we will usually use boldface letters for such names. 3.1 Booleans We begin by defining two lambda terms to encode the truth values"true"and “false Let and be the.Verify the following: Note that T and F are normal form possible ways of er 8
Exercise 4. This definition of β-equivalence is slightly different from the one given in class. Prove that they are in fact the same. 3 Programming in the untyped lambda calculus One of the amazing facts about the untyped lambda calculus is that we can use it to encode data, such as booleans and natural numbers, as well as programs that operate on the data. This can be done purely within the lambda calculus, without adding any additional syntax or axioms. We will often have occasion to give names to particular lambda terms; we will usually use boldface letters for such names. 3.1 Booleans We begin by defining two lambda terms to encode the truth values “true” and “false”: T = λxy.x F = λxy.y Let and be the term λab.abF. Verify the following: and TT → β T and TF → β F and FT → β F and FF → β F Note that T and F are normal forms, so we can really say that a term such as and TT evaluates to T. We say that and encodes the boolean function “and”. It is understood that this coding is with respect to the particular coding of “true” and “false”. We don’t claim that and MN evaluates to anything meaningful if M or N are terms other than T and F. Incidentially, there is nothing unique about the term λab.abF. It is one of many possible ways of encoding the “and” function. Another possibility is λab.bab. Exercise 5. Find lambda terms or and not that encode the boolean functions “or” and “not”. Can you find more than one term? 18
Ar.z.This term behaves like an n-specin for all lambda termsM,N. 3.2 Natural numbers If f and are lambda terms,and na natural number,writefor the term first few chureh numerals 0=Afr.I =f红.fr is d bneemsgooaRanwdo term as F;thus,whe The successor function can be defined as follows:suce =Anfr.f(nfr).What does this term compute when applied to a numeral? sucen (anfr.f(nfr))(Afr.fnz) →aAfz.f(fx.fx)fr) does multiplication nf.n(m 9
Moreover, we define the term if then else = λx.x. This term behaves like an “if-then-else” function — specifically, we have if then else TMN → β M if then else FMN → β N for all lambda terms M, N. 3.2 Natural numbers If f and x are lambda terms, and n > 0 a natural number, write f nx for the term f(f(. . .(fx). . .)), where f occurs n times. For each natural number n, we define a lambda term n, called the nth Church numeral, as n = λfx.f nx. Here are the first few Church numerals: 0 = λfx.x 1 = λfx.fx 2 = λfx.f(fx) 3 = λfx.f(f(fx)) . . . This particular way of encoding the natural numbers is due to Alonzo Church, who was also the inventor of the lambda calculus. Note that 0 is in fact the same term as F; thus, when interpreting a lambda term, we should know ahead of time whether to interpret the result as a boolean or a numeral. The successor function can be defined as follows: succ = λnfx.f(nfx). What does this term compute when applied to a numeral? succ n = (λnfx.f(nfx))(λfx.f nx) →β λfx.f((λfx.f nx)fx) →β λfx.f(f nx) = λfx.f n+1x = n + 1 Thus, we have proved that the term succ does indeed encode the successor function, when applied to a numeral. Here are possible definitions of addition and multiplication: add = λnmfx.nf(mfx) mult = λnmf.n(mf). 19
Exercise 6.(a)Manually evaluate the lambda terms add 23and mult 23. (b)Prove that add元元-*an+元，for all natural numbersn,m. (c)Prove that mult元m→g·m,for all natural numbersn,m. bda term. Mm..k→gfn1,,nk. This defini akes sto be an"“encoding tion.The definition generalizes easily to boolean functions.or functions of other datatypes. Often handy is the function iszero from natural numbers to booleans,which is defined by ,ifn≠0 Convince yourself that the following term is a representation of this function: iszero =Anzy.n(Xz.y)z. Exereise7.Find lambda terms that representeach of the following functions (a)fn)-(n+3)2. ()()e n (c)exp(n,m)=nm, (d)pred(n)=n-1. Note:part (d)is not eas In fact.Church believed for a while that it was imt sible.until his student Kleene found a solution.(In fact.Kleene said he found We have seen how to encode some simple boolean and arithmetic functions.How- ever,we do not yet havea systematic method of constructing such functions.What
Exercise 6. (a) Manually evaluate the lambda terms add 2 3 and mult 2 3. (b) Prove that add n m → β n + m, for all natural numbers n, m. (c) Prove that mult n m → β n · m, for all natural numbers n, m. Definition. Suppose f : N k → N is a k-ary function on the natural numbers, and that M is a lambda term. We say that M (numeralwise) represents f if for all n1, . . . , nk ∈ N, M n1 . . . nk → β f(n1, . . . , nk). This definition makes explicit what it means to be an “encoding”. We can say, for instance, that the term add = λnmfx.nf(mfx) represents the addition function. The definition generalizes easily to boolean functions, or functions of other datatypes. Often handy is the function iszero from natural numbers to booleans, which is defined by iszero (0) = true iszero (n) = false, if n 6= 0. Convince yourself that the following term is a representation of this function: iszero = λnxy.n(λz.y)x. Exercise 7. Find lambda terms that represent each of the following functions: (a) f(n) = (n + 3)2 , (b) f(n) = true if n is even, false if n is odd, (c) exp (n, m) = n m, (d) pred (n) = n − 1. Note: part (d) is not easy. In fact, Church believed for a while that it was impossible, until his student Kleene found a solution. (In fact, Kleene said he found the solution while having his wisdom teeth pulled, so his trick for defining the predecessor function is sometimes referred to as the “wisdom teeth trick”.) We have seen how to encode some simple boolean and arithmetic functions. However, we do not yet have a systematic method of constructing such functions. What 20