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 im￾plicit, (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 func￾tion 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