WIXLIB

A Tutorial Introductionto the Lambda CalculusRaul Rojas (Edited by Norman Ramsey)Freie Universität BerlinVersion 2.0, 2015Edit version 2.0-1, March 2018Editor’s note1This tutorial has been lightly edited inthree ways. The original uses a nonstandardabbreviation for Curried functions of multiplearguments; this abbreviation has been eliminated. The original uses a pun in which thecontinuations for selecting elements from pairshappen to agree with the classic representations of the Booleans; this pun has been eliminated. Finally, some typography and Englishhave been lightly adjusted to make the textconform more closely to American idioms.DefinitionThe λ-calculus can be called the smallest universal programming language in the world . The λcalculus consists of a single transformation rule(variable substitution, also called β-conversion)and a single function definition scheme. It wasintroduced in the 1930s by Alonzo Church as away of formalizing the concept of effective computability. The λ-calculus is universal in the sensethat any computable function can be expressedand evaluated using this formalism. It is thusequivalent to Turing machines. However, the λcalculus emphasizes the use of symbolic transformation rules and does not care about the actualmachine implementation. It is an approach morerelated to software than to hardware.AbstractThe central concept in λ-calculus is that of “expression”. A “name” is an identifier which, for ourpurposes, can be any of the letters a, b, c, etc. Anexpression can be just a name or can be a function. Functions use the Greek letter λ to mark thename of the function’s arguments. The “body” ofthe function specifies how the arguments are to berearranged. The identity function, for example, isrepresented by the string (λx.x). The fragment“λx” tell us that the function’s argument is x,which is returned unchanged as “x” by the function.This paper is a concise and painless introduction to the λ-calculus. This formalism was developed by Alonzo Church as a tool for studying themathematical properties of effectively computablefunctions. The formalism became popular andhas provided a strong theoretical foundation forthe family of functional programming languages.This tutorial shows how to perform arithmeticaland logical computations using the λ-calculus andhow to define recursive functions, even though λcalculus functions are unnamed and thus cannotrefer explicitly to themselves.Functions can be applied to other functions. Thefunction A, for example, applied to the functionB, would be written as AB. In this tutorial, capital letters are used to represent functions. In fact, Send corrections or suggestions to rojas@inf.fuberlin.de1

2anything 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 of symbols into anotherstring. This λ-calculus is untyped: any functioncan be applied to any other. The programmer isresponsible for keeping the computations sensible.the y being processed) in the body of the functiondefinition. Fig. 1 shows how the variable y is “absorbed” by the function (red line), and also showswhere it is used as a replacement for x (green line).The result is a reduction, represented by the rightarrow, with the final result y.(λ x.x)y yAn expression is defined recursively as follows:hexpressioni :: hnamei hfunctioni happlicationihfunctioni :: λhnamei.hexpressioni(λ . )y yhapplicationi :: hexpressionihexpressioniAn expression can be surrounded by parenthesisfor clarity, that is, if E is an expression, (E) is thesame expression. Otherwise, the only keywordsused in the language are λ and the dot. In orderto avoid cluttering expressions with parenthesis,we adopt the convention that function applicationassociates from the left, that is, the composite expressionE1 E2 E3 . . . Enis evaluated applying the successive expressions asfollows . . . (E1 E2 )E3 . . . EnAs can be seen from the definition of λexpressions, a well-formed example of a functionis the previously mentioned string, enclosed or notin parentheses:Figure 1: The same reduction shown twice. Thesymbol for the function’s argument is just a placeholder.Since we cannot always have pictures, as in Fig. 1,the notation [y/x] is used to indicate that all occurrences of x are substituted by y in the function’s body. We write, for example, (λx.x)y [y/x]x y. The names of the arguments infunction definitions do not carry any meaning bythemselves. They are just “place holders”, thatis, they are used to indicate how to rearrange thearguments of the function when it is evaluated.Therefore all the strings below represent the samefunction:(λz.z) (λy.y) (λt.t) (λu.u)This kind of purely alphabetical substitution isalso called α-reduction.λx.x (λx.x)We use the equivalence symbol “ ” to indicatethat when A B, A is just a synonym for B. Asexplained above, the name right after the λ is theidentifier of the argument of this function. Theexpression after the point (in this case a single x)is called the “body” of the function’s definition.Functions can be applied to expressions. A simpleexample of an application is(λx.x)yThis is the identity function applied to the variable y. Parentheses help to avoid ambiguity.A function application is evaluated by substituting the “value” of the argument x (in this case1.1Free and bound variablesIf we only had pictures of the plumbing of λexpressions, we would not have to care about thenames of variables. Since we are using letters assymbols, we have to be careful if we repeat them,as shown in this section.In λ-calculus all names are local to definitions (asin most programming languages). In the functionλx.x we say that x is “bound” since its occurrencein the body of the definition is preceded by λx. Aname not preceded by a λ is called a “free variable”. In the expression(λx.x)(λy.yx)

3the x in the body of the first expression from theleft is bound to the first λ. The y in the body ofthe second expression is bound to the second λ,and the following x is free. Bound variables areshown in bold face. It is very important to notice that this x in the second expression is totallyindependent of the x in the first expression. Thiscan be more easily seen if we draw the “plumbing”of the function application and the consequent reduction, as shown in Fig. 2.(λ x.x)(λ y.yx)(λ . )(λ . x) (λ . x)Figure 2: In successive rows: The function application, the “plumbing” of the symbolic expression,and the resulting reduction.A variable hnamei is bound if one of two casesholds: hnamei is bound in λ hname1 i.hexpi if theidentifier hnamei hname1 i or if hnamei isbound in hexpi.(Example: x is bound in (λy.(λx.x))). hnamei is bound in E1 E2 if hnamei is boundin E1 or if it is bound in E2 .(Example: x is bound in (λx.x)x).It should be emphasized that the same identifiercan occur free and bound in the same expression.In the expression(λx.xy)(λy.y)the first y is free in the parenthesized subexpression to the left, but it is bound in the subexpression to the right. Therefore, it occurs free as wellas bound in the whole expression (the bound variables are shown in bold face).1.2In Fig. 2 we see how the symbolic expression (firstrow) can be interpreted as a kind of circuit, wherethe 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 hasno connections with the rest of the expression, itis floating free inside the function definition.Formally, we say that a variable hnamei is free inan expression if one of the following three casesholds: hnamei is free in hnamei.(Example: a is free in a). hnamei is free in λhname1 i.hexpi if the identifier hnamei 6 hname1 i and hnamei is free inhexpi.(Example: y is free in λx.y). hnamei is free in E1 E2 if hnamei is free in E1or if it is free in E2 .(Example: x is free in (λx.x)x).SubstitutionsThe more confusing part of standard λ-calculus,when first approaching it, is the fact that we donot give names to functions. Any time we wantto apply a function, we just write the completefunction’s definition and then proceed to evaluate it. To simplify the notation, however, we willuse capital letters, digits and other symbols (sanserif) as synonyms for some functions. The identity function, for example, can be denoted by theletter I, using it as shorthand 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 thefirst function in parenthesis is independent of thex in the body of the second function (rememberthat the “plumbing” is local). Just to emphasizethe difference we can in fact rewrite the aboveexpression asII (λx.x)(λz.z).

4The identity function applied to itselfII (λx.x)(λz.z)yields thereforewith E. If the substitution would bring a freevariable of E in an expression where this variableoccurs bound, we rename the bound variable before performing the substitution. For example, inthe expression[(λz.z)/x]x λz.z I,that is, the identity function again.(λx.(λy.(x(λx.xy)))) ywe associate the first x with y. In the body(λy.(x(λx.xy)))(λ x.(λ y.xy))yonly the first x is free and can be substituted.Before substituting though, we have to rename thevariable y to avoid mixing its bound with its freeoccurrence:[y/x] (λt.(x(λx.xt))) (λt(y(λx.xt)))yboundinthesubexpression(λ x.(λ y.xy))yIn normal order reduction we reduce always theleft most expression of a series of applications first.We continue until no further reductions are �s2Figure 3: A free variable should not be substitutedin a subexpression where it is bound, otherwise anew “plumbing”, different to the original, wouldbe generated.When performing substitutions, we should becareful to avoid mixing up free occurrences of anidentifier with bound ones. In the expression λx.(λy.xy) ythe function on the left contains a bound y,whereas the y on the right is free. An incorrectsubstitution would mix the two identifiers in theerroneous resultArithmeticA programming language should be capable ofspecifying arithmetical calculations. Numbers canbe represented in the λ-calculus starting fromzero and writing “successor of zero”, that is“suc(zero)”, to represent 1, “suc(suc(zero))” torepresent 2, and so on. Since in λ-calculus wecan only define new functions, numbers will bedefined as functions using the following approach:zero can be defined asλs.(λz.z)This is a function of two arguments s and z. Thefirst natural numbers can be defined as0 λs.λz.z(λy.yy).1 λs.λz.s(z)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.hexpi is applied toE, we substitute all free occurrences of x in hexpi2 λs.λz.s(s(z))3 λs.λz.s(s(s(z)))and so on.The big advantage of defining numbers in this wayis that we can now apply a function f to an argument a any number of times. For example, if