Definition. Assume given an nn e set of variables Let be an aphabet d*he the set of strings (finite s nces)over the aphabet A.The set of lambda terms is the smallest subset AAsuch that: 。Whenever z∈V then r∈ ·Whenever M,N∈A then(MIN)∈A. ·WheneverzEV and M∈A then(u.MeA Comparing the two equivalent definitions,we see that the Backus-Naur Form is a convenient notation because:(1)the definiti n of the alphabet can be left im net met a-symbols tor d syn the setsand In the future.we will aays present syntactic BNF style. The following are some examples of lambda terms (xz.z)((Az.(rz))(Xy.(wy)))(Xf.(Xz.(f(fz)))) Note that in the definition of lambda terms,we have built in enough mandatory parentheses to ensure that every be uniquely decomposed int s.ea orms a and lambda abstractions respectively () n( nbdo de of the more traditional f(.This allows us to economize more efficiently on the .We omit outermost parentheses.For instance.we write MN instead of(MN). Applications associate to the left:thus,MNP means (MN)P.This is ch mear The body of a lambda abstraction (the part after the dot)extends as far to the right as possible.In particular,Ar.MN means Az.(MN).and not 入r.MN
Definition. Assume given an infinite set V of variables. Let A be an alphabet consisting of the elements of V, and the special symbols “(”, “)”, “λ”, and “.”. Let A∗ be the set of strings (finite sequences) over the alphabet A. The set of lambda terms is the smallest subset Λ ⊆ A∗ such that: • Whenever x ∈ V then x ∈ Λ. • Whenever M, N ∈ Λ then (MN) ∈ Λ. • Whenever x ∈ V and M ∈ Λ then (λx.M) ∈ Λ. Comparing the two equivalent definitions, we see that the Backus-Naur Form is a convenient notation because: (1) the definition of the alphabet can be left implicit, (2) the use of distinct meta-symbols for different syntactic classes (x, y, z for variables and M, N for terms) eliminates the need to explicitly quantify over the sets V and Λ. In the future, we will always present syntactic definitions in the BNF style. The following are some examples of lambda terms: (λx.x) ((λx.(xx))(λy.(yy))) (λf.(λx.(f(fx)))) Note that in the definition of lambda terms, we have built in enough mandatory parentheses to ensure that every term M ∈ Λ can be uniquely decomposed into subterms. This means, each term M ∈ Λ is of precisely one of the forms x, (MN), (λx.M). Terms of these three forms are called variables, applications, and lambda abstractions, respectively. We use the notation (MN), rather than M(N), to denote the application of a function M to an argument N. Thus, in the lambda calculus, we write (fx) instead of the more traditional f(x). This allows us to economize more efficiently on the use of parentheses. To avoid having to write an excessive number of parentheses, we establish the following conventions for writing lambda terms: Convention. • We omit outermost parentheses. For instance, we write MN instead of (MN). • Applications associate to the left; thus, MNP means (MN)P. This is convenient when applying a function to a number of arguments, as in fxyz, which means ((fx)y)z. • The body of a lambda abstraction (the part after the dot) extends as far to the right as possible. In particular, λx.MN means λx.(MN), and not (λx.M)N. 11
Multiple lambda abstractions can be contracted,thusMwill abbre- viate Ar.Ay.Az.M It is important to note that this convention is only for notational convenience:it does not affect the"official"definition of lambda terms. Exereise 3.(a)Write the following terms with as few parenthesis as possible. without changing the meaning or structure of the terms: (0(c.(Ag.(Az.(x2y2》 (ii)(((ab)(cd))((ef)(ah))). (im）(.(Ay.(r)(a.)z))(A.w (b)Restore all the dropped par (i Trr (i）z.(rXy.Vrr)z. 2.2 Free and bound variables,a-equivalence In our informal discussion of lambda terms.we have already pointed out that the termsand which differ only in the name of their bound variable,are We will say that such terms are o-equivalent,and we write mbol fo gr is called ad that the subte sthe scope of the binder.A variable occurrence that is not bound is free.Thus,for example,in the term M=(Xr.ry)(Ay-yz), r is bound,but is free.The variable y has both a free and a bound occurrence The set of free variables of M is 12
• Multiple lambda abstractions can be contracted; thus λxyz.M will abbreviate λx.λy.λz.M. It is important to note that this convention is only for notational convenience; it does not affect the “official” definition of lambda terms. Exercise 3. (a) Write the following terms with as few parenthesis as possible, without changing the meaning or structure of the terms: (i) (λx.(λy.(λz.((xz)(yz))))), (ii) (((ab)(cd))((ef)(gh))), (iii) (λx.((λy.(yx))(λv.v)z)u)(λw.w). (b) Restore all the dropped parentheses in the following terms, without changing the meaning or structure of the terms: (i) xxxx, (ii) λx.xλy.y, (iii) λx.(xλy.yxx)x. 2.2 Free and bound variables, α-equivalence In our informal discussion of lambda terms, we have already pointed out that the terms λx.x and λy.y, which differ only in the name of their bound variable, are essentially the same. We will say that such terms are α-equivalent, and we write M =α N. In the rare event that we want to say that two terms are precisely equal, symbol for symbol, we say that M and N are identical and we write M ≡ N. We reserve “=” as a generic symbol used for different purposes. An occurrence of a variable x inside a term of the form λx.N is said to be bound. The corresponding λx is called a binder, and we say that the subterm N is the scope of the binder. A variable occurrence that is not bound is free. Thus, for example, in the term M ≡ (λx.xy)(λy.yz), x is bound, but z is free. The variable y has both a free and a bound occurrence. The set of free variables of M is {y, z}. 12
FV(r) FV(MN) FV(Az.AM)=FV(M)八{z. This definition is an example ofa definition by recursion on terms.In other words. in defining FV(M).we assume that we have already defined FV(N)for all We will often encounter such recursive definitions,as well as Before we can formally define,we need to define what it means yareM.Rer ng Is follows: x{/红} ifx≠ .M (Miu/))(N(u/)). (Az.M)u/)=Az.(M(u/)). ifx≠z Note that this kind of renaming replaces all occurrences ofz by y.whether free. bound.or binding.We will only apply it in cases where does not already occur Finally,we are in a position to formally define what it means for two terms to be the same up to renaming of bound variables Ar.M =a Ay.(M(y/)) Recall that n lambda te (re( a)and ()Thus,by definition,a-equivalence is the smallest relation on lambda terms satisfying the six rules in Table 1. It is easy to prove by induction that any lambda term is o quivalent to another term in which the names of all bound variables are distinct from each other and from any free variables.Thus,when we manipulate lambda terms in theory and 3
More generally, the set of free variables of a term M is denoted FV (M), and it is defined formally as follows: FV (x) = {x}, FV (MN) = FV (M) ∪ FV (N), FV (λx.M) = FV (M) \ {x}. This definition is an example of a definition by recursion on terms. In other words, in defining FV (M), we assume that we have already defined FV (N) for all subterms of M. We will often encounter such recursive definitions, as well as inductive proofs. Before we can formally define α-equivalence, we need to define what it means to rename a variable in a term. If x, y are variables, and M is a term, we write M{y/x} for the result of renaming x as y in M. Renaming is formally defined as follows: x{y/x} ≡ y, z{y/x} ≡ z, if x 6= z, (MN){y/x} ≡ (M{y/x})(N{y/x}), (λx.M){y/x} ≡ λy.(M{y/x}), (λz.M){y/x} ≡ λz.(M{y/x}), if x 6= z. Note that this kind of renaming replaces all occurrences of x by y, whether free, bound, or binding. We will only apply it in cases where y does not already occur in M. Finally, we are in a position to formally define what it means for two terms to be “the same up to renaming of bound variables”: Definition. We define α-equivalence to be the smallest congruence relation =α on lambda terms, such that for all terms M and all variables y that do not occur in M, λx.M =α λy.(M{y/x}). Recall that a relation on lambda terms is an equivalence relation if it satisfies rules (refl), (symm), and (trans). It is a congruence if it also satisfies rules (cong) and (ξ). Thus, by definition, α-equivalence is the smallest relation on lambda terms satisfying the six rules in Table 1. It is easy to prove by induction that any lambda term is α-equivalent to another term in which the names of all bound variables are distinct from each other and from any free variables. Thus, when we manipulate lambda terms in theory and 13
(e0 M=M (cong) M=M N=N MN-MN M- (smm） M-N T=/ (9 1rM=人r (trans)M=NN=P ud (a) M=P x.M=y.(M{y/万 Table 1:The rules for alpha-equivalence variable comention. and bound variables and c standard math. e2aaesaopnaeeeoaop6hae r'dr ∑101 limr一xe2 int succ(int x){return x+1; 2.3 Substitution trivial operation,called ion,which allows us to replace a variable by We will witeor the resut ofreplacing by NnM The ostitution is complicated by two circumstances 1.We should only replace free variables.This is because the names of bound variables are considered immaterial,and should not affect the result of a substitution.Ihus,zx(入ry.r)N/xisN(入xy.x).and not N（(入xy.N):
(refl) M = M (symm) M = N N = M (trans) M = N N = P M = P (cong) M = M0 N = N0 MN = M0N0 (ξ) M = M0 λx.M = λx.M0 (α) y 6∈ M λx.M = λy.(M{y/x}) Table 1: The rules for alpha-equivalence in practice, we can (and will) always assume without loss of generality that bound variables have been renamed to be distinct. This convention is called Barendregt’s variable convention. As a remark, the notions of free and bound variables and α-equivalence are of course not particular to the lambda calculus; they appear in many standard mathematical notations, as well as in computer science. Here are four examples where the variable x is bound. R 1 0 x 2 dx P10 x=1 1 x limx→∞ e −x int succ(int x) { return x+1; } 2.3 Substitution In the previous section, we defined a renaming operation, which allowed us to replace a variable by another variable in a lambda term. Now we turn to a less trivial operation, called substitution, which allows us to replace a variable by a lambda term. We will write M[N/x] for the result of replacing x by N in M. The definition of substitution is complicated by two circumstances: 1. We should only replace free variables. This is because the names of bound variables are considered immaterial, and should not affect the result of a substitution. Thus, x(λxy.x)[N/x] is N(λxy.x), and not N(λxy.N). 14
and bound in M.What should be the result of substituting for in M? If we do this naively,we get M[N/]=(AI.Vz)[N/y]=Ar.Nz=Az.(Xz.). n for the fac that the that was bound in was not the"sameas the one that wa free in N.The proper thing to do is to rename the bound variable before the MIN/yl=('.)IN/yl =Ar'.N'=.(z.z) srename a bound vari the new name of the bound variable that is currently unused is calle fresh.The reason we stipulated that the set is infinite was to make sure a fresh variable is always available when we need one. EN, ifx≠， A.MNa三d. MIN/z)(PIN/z)). (Av-M)IN/]=v.(MIN/z). ifx≠y and yFV(ON (Ay.M)[N/]=v/.(M(v/y)[N/])..yEFV(N),and y'fresh. n the la way to solve this problem is to declare all lambda terms to be identified up to a-equivalence,an d to prove tha substitution is in fact w ll-defined modulo equivalence.Ano ywould specify which se:fo Mor N
2. We need to avoid unintended “capture” of free variables. Consider for example the term M ≡ λx.yx, and let N ≡ λz.xz. Note that x is free in N and bound in M. What should be the result of substituting N for y in M? If we do this naively, we get M[N/y] = (λx.yx)[N/y] = λx.Nx = λx.(λz.xz)x. However, this is not what we intended, since the variable x was free in N, and during the substitution, it got bound. We need to account for the fact that the x that was bound in M was not the “same” x as the one that was free in N. The proper thing to do is to rename the bound variable before the substitution: M[N/y] = (λx0 .yx 0 )[N/y] = λx0 .Nx 0 = λx0 .(λz.xz)x 0 . Thus, the operation of substitution forces us to sometimes rename a bound variable. In this case, it is best to pick a variable from V that has not been used yet as the new name of the bound variable. A variable that is currently unused is called fresh. The reason we stipulated that the set V is infinite was to make sure a fresh variable is always available when we need one. Definition. The (capture-avoiding) substitution of N for free occurrences of x in M, in symbols M[N/x], is defined as follows: x[N/x] ≡ N, y[N/x] ≡ y, if x 6= y, (MP)[N/x] ≡ (M[N/x])(P[N/x]), (λx.M)[N/x] ≡ λx.M, (λy.M)[N/x] ≡ λy.(M[N/x]), if x 6= y and y 6∈ FV (N), (λy.M)[N/x] ≡ λy0 .(M{y 0/y}[N/x]), if x 6= y, y ∈ FV (N), and y 0 fresh. This definition has one technical flaw: in the last clause, we did not specify which fresh variable to pick, and thus, technically, substitution is not well-defined. One way to solve this problem is to declare all lambda terms to be identified up to α-equivalence, and to prove that substitution is in fact well-defined modulo α- equivalence. Another way would be to specify which variable y 0 to choose: for instance, assume that there is a well-ordering on the set V of variables, and stipulate that y 0 should be chosen to be the least variable that does not occur in either M or N. 15