1.2 The lambda calculus The lambda calculus is a theory of functions as formulas.It is a system for ma nipulating functions as expressions well-know l oressions are made up from variables num bers(L,2,3,.,and operators(“+",“-”,“x”etc.An expression such as+y add,or the that somet results explicitly.So for instance.we write A=(+)×2 and not let w=x+y,then let u=22,then let A=wx u The latter notation would be tiring and cumbersome to manipulate. Let f be the function2.Then consider A=f(5) in the lambda calculus we just write A-(x.x2)5 The expression r.stands for the function that mans r to r2 (as on osed to the group terms. It is understood that the called a bound variable. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions ie functions whose inputs and or outputs are themselves xr.f(f()). 6
1.2 The lambda calculus The lambda calculus is a theory of functions as formulas. It is a system for manipulating functions as expressions. Let us begin by looking at another well-known language of expressions, namely arithmetic. Arithmetic expressions are made up from variables (x, y, z . . .), numbers (1, 2, 3, . . .), and operators (“+”, “−”, “×” etc.). An expression such as x+y stands for the result of an addition (as opposed to an instruction to add, or the statement that something is being added). The great advantage of this language is that expressions can be nested without any need to mention the intermediate results explicitly. So for instance, we write A = (x + y) × z 2 , and not let w = x + y, then let u = z 2 , then let A = w × u. The latter notation would be tiring and cumbersome to manipulate. The lambda calculus extends the idea of an expression language to include functions. Where we normally write Let f be the function x 7→ x 2 . Then consider A = f(5), in the lambda calculus we just write A = (λx.x2 )(5). The expression λx.x2 stands for the function that maps x to x 2 (as opposed to the statement that x is being mapped to x 2 ). As in arithmetic, we use parentheses to group terms. It is understood that the variable x is a local variable in the term λx.x2 . Thus, it does not make any difference if we write λy.y2 instead. A local variable is also called a bound variable. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions, i.e., functions whose inputs and/or outputs are themselves functions. An example is the operation f 7→ f ◦ f in mathematics, which takes a function f and maps it to f ◦ f, the composition of f with itself. In the lambda calculus, f ◦ f is written as λx.f(f(x)), 6
and the operation that mapsftoffis writtenas Xf.Xr.f(f(z)). The evaluation of highe -order functions can get somewhat complex;as an exam ple,consider the following expression: ((Xf.xr.f(f(z)))(Ay.y2))(5) Convince yourself that this evaluates to 625.Another example is given in the following exercise: Exercise 1.Evaluate the lambda-expression （(af.z.fff))(Ag.Awg(g())(Az.z+1)）O) We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs.typed lambda-calculi We have already mentioned that when considerir ns as rules”,isno always necessary to know the domain and codomain of a function ahead of time The simplest example is the identity functionf which can have any set ain and c main are that we encountered above.One can check that o maps any function f:X to a function(f):.In this case,we say that the type of g is (X→X)→(X一X). By being fle mains and codoma s,we are able to manipulate func po d e we can take r=f,and we get f(f)=(Ar.)(f)=f. As another example,letw=Ar.r()
and the operation that maps f to f ◦ f is written as λf.λx.f(f(x)). The evaluation of higher-order functions can get somewhat complex; as an example, consider the following expression: (λf.λx.f(f(x)))(λy.y2 ) (5) Convince yourself that this evaluates to 625. Another example is given in the following exercise: Exercise 1. Evaluate the lambda-expression (λf.λx.f(f(f(x)))) (λg.λy.g(g(y))) (λz.z + 1) (0). We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs. typed lambda-calculi We have already mentioned that, when considering “functions as rules”, is not always necessary to know the domain and codomain of a function ahead of time. The simplest example is the identity function f = λx.x, which can have any set X as its domain and codomain, as long as domain and codomain are equal. We say that f has the type X → X. Another example is the function g = λf.λx.f(f(x)) that we encountered above. One can check that g maps any function f : X → X to a function g(f) : X → X. In this case, we say that the type of g is (X → X) → (X → X). By being flexible about domains and codomains, we are able to manipulate functions in ways that would not be possible in ordinary mathematics. For instance, if f = λx.x is the identity function, then we have f(x) = x for any x. In particular, we can take x = f, and we get f(f) = (λx.x)(f) = f. Note that the equation f(f) = f never makes sense in ordinary mathematics, since it is not possible (for set-theoretic reasons) for a function to be included in its own domain. As another example, let ω = λx.x(x). 7
Exercise 2.What is w(w)? We have several options regarding types in the lambda calculus .Untyped lambda calculus.In the untyped lambda calculus,we never specify his gives us maxim argument that it does not understand app Simply-tvped lambda calculus.In the simply-typed lambda calculus.we always completely specify the type of every expression.This is very simila to the situation in set theory.We e never allow the pplication of a runctio s the identity function .Polymorphically typed lambda calculus.This is an intermediate situation ance,that a term has a type of the form As we will see.each of these alternatives has dramatically different properties from the others. 1.4 Lambda calculus and computability In the 1930's,several people were interested in the question:what does it mean for a functionf:NNto be compuable?An informal definition of computability s that the should be a pencil-and-paper me thod allowing a trained erson t Tne concept or a penc the following definitions of computability: ers attempt ed pap 1.Turing defined an idealized computer we now call a Tiring machine,and
Exercise 2. What is ω(ω)? We have several options regarding types in the lambda calculus. • Untyped lambda calculus. In the untyped lambda calculus, we neverspecify the type of any expression. Thus we never specify the domain or codomain of any function. This gives us maximal flexibility. It is also very unsafe, because we might run into situations where we try to apply a function to an argument that it does not understand. • Simply-typed lambda calculus. In the simply-typed lambda calculus, we always completely specify the type of every expression. This is very similar to the situation in set theory. We never allow the application of a function to an argument unless the type of the argument is the same as the domain of the function. Thus, terms such as f(f) are ruled out, even if f is the identity function. • Polymorphically typed lambda calculus. This is an intermediate situation, where we may specify, for instance, that a term has a type of the form X → X for all X, without actually specifying X. As we will see, each of these alternatives has dramatically different properties from the others. 1.4 Lambda calculus and computability In the 1930’s, several people were interested in the question: what does it mean for a function f : N → N to be computable? An informal definition of computability is that there should be a pencil-and-paper method allowing a trained person to calculate f(n), for any given n. The concept of a pencil-and-paper method is not so easy to formalize. Three different researchers attempted to do so, resulting in the following definitions of computability: 1. Turing defined an idealized computer we now call a Turing machine, and postulated that a function is computable (in the intuitive sense) if and only if it can be computed by such a machine. 2. Godel ¨ defined the class of general recursive functions as the smallest set of functions containing all the constant functions, the successor function, and 8
closed und is general recursive. 3.Church defined an idealized programming language called the lambda cal an be written as a lar a term It was proved by Church,Kleene.Rosser,and Turing that all three computational of computable fun ns Whe mode notioof comutability isaquestion tht ao benseredbecause thereisn 1.5 Connections to computer science The lambda calculus is a very idealized programming language:arguably.it is the Because or Its simpl hining and proving properties of program Many real-world programming languages can be regarded as extensions of the input/output,side effects da calculus provide a a le for stu h extensions,in isolation and jointly,to see how the a well-formed rogram will n CPeiesofpoeramaminglanguae(SLc The lambda calculus is also a tool used in compiler construction,see e.g.[8.9]. 1.6 Connections to logic In the 19th and early 20th centuries,there was a philosophical dispute among t what a proof is.The 0-9 ists such as that it is sufficient to derive a contradiction from the assumption that it doesn't exist
closed under certain operations (such as compositions and recursion). He postulated that a function is computable (in the intuitive sense) if and only if it is general recursive. 3. Church defined an idealized programming language called the lambda calculus, and postulated that a function is computable (in the intuitive sense) if and only if it can be written as a lambda term. It was proved by Church, Kleene, Rosser, and Turing that all three computational models were equivalent to each other, i.e., each model defines the same class of computable functions. Whether or not they are equivalent to the “intuitive” notion of computability is a question that cannot be answered, because there is no formal definition of “intuitive computability”. The assertion that they are in fact equivalent to intuitive computability is known as the Church-Turing thesis. 1.5 Connections to computer science The lambda calculus is a very idealized programming language; arguably, it is the simplest possible programming language that is Turing complete. Because of its simplicity, it is a useful tool for defining and proving properties of programs. Many real-world programming languages can be regarded as extensions of the lambda calculus. This is true for all functional programming languages, a class that includes Lisp, Scheme, Haskell, and ML. Such languages combine the lambda calculus with additional features, such as data types, input/output, side effects, udpateable memory, object orientated features, etc. The lambda calculus provides a vehicle for studying such extensions, in isolation and jointly, to see how they will affect each other, and to prove properties of programming language (such as: a well-formed program will not crash). The lambda calculus is also a tool used in compiler construction, see e.g. [8, 9]. 1.6 Connections to logic In the 19th and early 20th centuries, there was a philosophical dispute among mathematicians about what a proof is. The so-called constructivists, such as Brower and Heyting, believed that to prove that a mathematical object exists, one must be able to construct it explicitly. Classical logicians, such as Hilbert, held that it is sufficient to derive a contradiction from the assumption that it doesn’t exist. 9
Ironically,one of the better-known examples of a proof that isn't constructive is Brower's proof of his rem,wh h states that every continuou give anyinformation on the ocaion of the on and does n The connection between lambda calculu us and constructive logics is via the"proof must be a"construction ie.a program.The lambda calculus is a notation for such programs.and it can also be used as a notion for(constuctive)proofs. For the most part.constructivism has not prevailed as a philosophy in main mathematics.However.there has been renewed interest in constructivism in the second half of the 20th century.The reason is that constructive proofs give more information thanc lassical on s,and in articular,they allow one o compute so math for in ion) computer algebra systems 1.7 Connections to mathematics e given meaning such models are constructed u sing methods from algebra.partially ordered sets.topology,category theory.and other areas of mathematics 2 The untyped lambda calculus 2.1 Syntax The lambda calculus is a formal language.The expressions of the language are called fambda termts,and we will give rules for manipulating them iables d noted by.et Lambda terms:M.N::=(MN)|(Ar.M) The above Backus-Naur Form (BNF)is a convenient abbreviation for the follow ing equivalent,more traditionally mathematical definition:
Ironically, one of the better-known examples of a proof that isn’t constructive is Brower’s proof of his own fixpoint theorem, which states that every continuous function on the unit disc has a fixpoint. The proof is by contradiction and does not give any information on the location of the fixpoint. The connection between lambda calculus and constructive logicsis via the “proofsas-programs” paradigm. To a constructivist, a proof (of an existence statement) must be a “construction”, i.e., a program. The lambda calculus is a notation for such programs, and it can also be used as a notion for (constuctive) proofs. For the most part, constructivism has not prevailed as a philosophy in mainstream mathematics. However, there has been renewed interest in constructivism in the second half of the 20th century. The reason is that constructive proofs give more information than classical ones, and in particular, they allow one to compute solutions to problems (as opposed to merely knowing the existence of a solution). The resulting algorithms can be useful in computational mathematics, for instance in computer algebra systems. 1.7 Connections to mathematics One way to study the lambda calculus is to give mathematical models of it, i.e., to provide spaces in which lambda terms can be given meaning. Such models are constructed using methods from algebra, partially ordered sets, topology, category theory, and other areas of mathematics. 2 The untyped lambda calculus 2.1 Syntax The lambda calculus is a formal language. The expressions of the language are called lambda terms, and we will give rules for manipulating them. Definition. Assume given an infinite set V of variables, denoted by x, y, z etc. The set of lambda terms is given by the following Backus-Naur Form: Lambda terms: M, N ::= x (MN) (λx.M) The above Backus-Naur Form (BNF) is a convenient abbreviation for the following equivalent, more traditionally mathematical definition: 10