mopdf.com

A Tutorial Introduction to the LambdaCalculusRaul Rojas Freie Universität BerlinVersion 2.0, 2015AbstractThis paper is a concise and painless introduction to the λ-calculus.This formalism was developed by Alonzo Church as a tool for studying the mathematical properties of effectively computable functions.The formalism became popular and has provided a strong theoreticalfoundation for the family of functional programming languages. Thistutorial shows how to perform arithmetical and logical computationsusing the λ-calculus and how to define recursive functions, even thoughλ-calculus functions are unnamed and thus cannot refer explicitly tothemselves.1DefinitionThe λ-calculus can be called the smallest universal programming languagein the world . The λ-calculus consists of a single transformation rule (variable substitution, also called β-conversion) and a single function definition Send corrections or suggestions to [email protected]

2scheme. It was introduced in the 1930s by Alonzo Church as a way of formalizing the concept of effective computability. The λ-calculus is universalin the sense that any computable function can be expressed and evaluatedusing this formalism. It is thus equivalent to Turing machines. However,the λ-calculus emphasizes the use of symbolic transformation rules and doesnot care about the actual machine implementation. It is an approach morerelated to software than to hardware.The central concept in λ-calculus is that of “expression”. A “name” is anidentifier which, for our purposes, can be any of the letters a, b, c, etc. Anexpression can be just a name or can be a function. Functions use the Greekletter λ to mark the name of the function’s arguments. The “body” of thefunction specifies how the arguments are to be rearranged. The identityfunction, for example, is represented by the string (λx.x). The fragment“λx” tell us that the function’s argument is x, which is returned unchangedas “x” by the function.Functions can be applied to other functions. The function A, for example,applied to the function B, would be written as AB. In this tutorial, capitalletters are used to represent functions. In fact, anything of interest in λcalculus is a function. Even numbers or logical values will be representedby functions that can act on one another in order to transform a string ofsymbols into another string. There are no types in λ-calculus: any function can act on any other. The programmer is responsible for keeping thecomputations sensible.An expression is defined recursively as follows: expression : name function application function : λ name . expression application : expression expression An expression can be surrounded by parenthesis for clarity, that is, if E is anexpression, (E) is the same expression. Otherwise, the only keywords used inthe language are λ and the dot. In order to avoid cluttering expressions withparenthesis, we adopt the convention that function application associates

3from the left, that is, the composite expressionE1 E2 E3 . . . Enis evaluated applying the successive expressions as follows . . . (E1 E2 )E3 . . . EnAs can be seen from the definition of λ-expressions, a well-formed example ofa function is the previously mentioned string, enclosed or not in parentheses:λx.x (λx.x)We use the equivalence symbol “ ” to indicate that when A B, A is justa synonym for B. As explained above, the name right after the λ is theidentifier of the argument of this function. The expression after the point (inthis case a single x) is called the “body” of the function’s definition.Functions can be applied to expressions. A simple example of an applicationis(λx.x)yThis is the identity function applied to the variable y. Parenthesis help toavoid ambiguity. Function applications are evaluated by substituting the“value” of the argument x (in this case the y being processed) in the body ofthe function definition. Fig. 1 shows how the variable y is “absorbed” by thefunction (red line), and also shows where it is used as a replacement for x(green line). The result is a reduction, represented by the right arrow, withthe final result y.Since we cannot always have pictures, as in Fig. 1, the notation [y/x] is usedto indicate that all occurrences of x are substituted by y in the function’sbody. We write, for example, (λx.x)y [y/x]x y. The names of thearguments in function definitions do not carry any meaning by themselves.They are just “place holders”, that is, they are used to indicate how torearrange the arguments of the function when it is evaluated. Therefore allthe strings below represent the same function:(λz.z) (λy.y) (λt.t) (λu.u)This kind of purely alphabetical substitution is also called α-reduction.

4(λ x.x)y y(λ . )y yFigure 1: The same reduction shown twice. The symbol for the function’sargument is just a place holder1.1Free and bound variablesIf we only had pictures of the plumbing of λ-expressions, we would not haveto care about the names of variables. Since we are using letters as symbols,we have to be careful if we repeat them, as shown in this section.In λ-calculus all names are local to definitions (like in most programminglanguages). In the function λx.x we say that x is “bound” since its occurrencein the body of the definition is preceded by λx. A name not preceded by aλ is called a “free variable”. In the expression(λx.x)(λy.yx)the x in the body of the first expression from the left is bound to the firstλ. The y in the body of the second expression is bound to the second λ,and the following x is free. Bound variables are shown in bold face. Itis very important to notice that this x in the second expression is totallyindependent of the x in the first expression. This can be more easily seenif we draw the “plumbing” of the function application and the consequentreduction, as shown in Fig. 2.In Fig. 2 we see how the symbolic expression (first row) can be interpretedas a kind of circuit, where the bound argument is moved to a new positioninside the body of the function. The first function (the identity function)“consumes” the second one. The symbol x in the second function has noconnections with the rest of the expression, it is floating free inside the function definition.

5(λ x.x)(λ y.yx)(λ . )(λ . x) (λ . x)Figure 2: In successive rows: The function application, the “plumbing” ofthe symbolic expression, and the resulting reductionFormally, we say that a variable name is free in an expression if one ofthe following three cases holds: name is free in name .(Example: a is free in a). name is free in λ name1 . exp if the identifier name 6 name1 and name is free in exp .(Example: y is free in λx.y). name is free in E1 E2 if name is free in E1 or if it is free in E2 .(Example: x is free in (λx.x)x).A variable name is bound if one of two cases holds: name is bound in λ name1 . exp if the identifier name name1 or if name is bound in exp .(Example: x is bound in (λy.(λx.x))). name is bound in E1 E2 if name is bound in E1 or if it is boundin E2 .(Example: x is bound in (λx.x)x).

6It should be emphasized that the same identifier can occur free and boundin the same expression. In the expression(λx.xy)(λy.y)the first y is free in the parenthesized subexpression to the left, but it isbound in the subexpression to the right. Therefore, it occurs free as well asbound in the whole expression (the bound variables are shown in bold face).1.2SubstitutionsThe more confusing part of standard λ-calculus, when first approaching it,isthe fact that we do not give names to functions. Any time we want to applya function, we just write the complete function’s definition and then proceedto evaluate it. To simplify the notation, however, we will use capital letters,digits and other symbols (san serif) as synonyms for some functions. Theidentity function, for example, can be denoted by the letter I, using it asshorthand for (λx.x).The identity function applied to itself is the applicationII (λx.x)(λx.x).In this expression, the first x in the body of the first function in parenthesisis independent of the x in the body of the second function (remember thatthe “plumbing” is local). Just to emphasize the difference we can in factrewrite the above expression asII (λx.x)(λz.z).The identity function applied to itselfII (λx.x)(λz.z)yields therefore[(λz.z)/x]x λz.z I,that is, the identity function again.

7(λ x.(λ y.xy))yyboundinthesubexpression(λ x.(λ Figure 3: A free variable should not be substituted in a subexpression whereit is bound, otherwise a new “plumbing”, different to the original, would begeneratedWhen performing substitutions, we should be careful to avoid mixing up freeoccurrences of an identifier with bound ones. In the expression λx.(λy.xy) ythe function on the left contains a bound y, whereas the y on the right isfree. An incorrect substitution would mix the two identifiers in the erroneousresult(λy.yy).Simply by renaming the bound y to t we obtain λx.(λt.xt) y (λt.yt)which is a completely different result but nevertheless the correct one.Therefore, if the function λx. exp is applied to E, we substitute all freeoccurrences of x in exp with E. If the substitution would bring a freevariable of E in an expression where this variable occurs bound, we rename

8the bound variable before performing the substitution. For example, in theexpression(λx.(λy.(x(λx.xy)))) ywe associate the first x with y. In the body(λy.(x(λx.xy)))only the first x is free and can be substituted. Before substituting though,we have to rename the variable y to avoid mixing its bound with its freeoccurrence:[y/x] (λt.(x(λx.xt))) (λt(y(λx.xt)))In normal order reduction we try to reduce always the left most expression ofa series of applications. We continue until no further reductions are possible.2ArithmeticA programming language should be capable of specifying arithmetical calculations. Numbers can be represented in the λ-calculus starting from zero andwriting “successor of zero”, that is “suc(zero)”, to represent 1, “suc(suc(zero))”to represent 2, and so on. Since in λ-calculus we can only define new functions, numbers will be defined as functions using the following approach: zerocan be defined asλs.(λz.z)This is a function of two arguments s and z. We will abbreviate such expressions with more than one argument asλsz.zIt is understood here that s is the first argument to be substituted during theevaluation and z the second. Using this notation, the first natural numberscan be defined as0123 λsz.zλsz.s(z)λsz.s(s(z))λsz.s(s(s(z)))