Transcription of A Tutorial Introduction to the Lambda Calculus
1 A Tutorial Introduction to the Lambda CalculusRa ul Rojas FU Berlin, WS-97/98 AbstractThis paper is a short and painless Introduction to the Calculus . Originallydeveloped in order to study some mathematical properties of effectively com-putable functions, this formalism has provided a strong theoretical foundationfor the family of functional programming languages. We show how to performsome arithmetical computations using the Calculus and how to define recur-sive functions, even though functions in Calculus are not given names and thuscannot refer explicitly to DefinitionThe Calculus can be called thesmallest universal programming language of theworld. The Calculus consists of a single transformation rule (variable substitution)and a single function definition scheme. It was introduced in the 1930s by AlonzoChurch as a way of formalizing the concept of effective computability.
2 The calculusis universal in the sense that any computable function can be expressed and evaluatedusing this formalism. It is thus equivalent to Turing machines. However, the calculusemphasizes the use of transformation rules and does not care about the actual machineimplementing them. It is an approach more related to software than to central concept in Calculus is the expression . A name , also called a variable , is an identifier which, for our purposes, can be any of the lettersa,b,c,..An expression is defined recursively as follows:<expression>:=<name>|<function>|<application> <function>:= <name>.<expression> <application>:=<expression> <expression>An expression can be surrounded with parenthesis for clarity, that is, ifEis anexpression, (E) is the same expression. The only keywords used in the language are and the dot. In order to avoid cluttering expressions with parenthesis, we adopt theconvention that function application associates from the left, that is, the Send corrections or suggestions to evaluated applying the expressions as follows:(.)
3 ((E1E2)E3)..En)As can be seen from the definition of expressions given above, a single identifieris a expression. An example of a function is the following: expression defines the identity function. The name after the is the identifierof the argument of this function. The expression after the point (in this case a singlex) is called the body of the can be applied to expressions. An example of an application is( )yThis is the identity function applied toy. Parenthesis are used for clarity in order toavoid ambiguity. Function applications are evaluated by substituting the value of theargumentx(in this casey) in the body of the function definition, ( )y= [y/x]x=yIn this transformation the notation [y/x] is used to indicate that all occurrences ofxare substituted byyin the expression to the names of the arguments in function definitions do not carry any meaning bythemselves.
4 They are just place holders , that is, they are used to indicate how torearrange the arguments of the function when it is evaluated. Therefore( ) ( ) ( ) ( )and so forth. We use the symbol to indicate that whenA B,Ais just asynonym Free and bound variablesIn Calculus all names are local to definitions. In the function say thatxis bound since its occurrence in the body of the definition is preceded by x. A namenot preceded by a is called a free variable . In the expression( )the variablexis bound andyis free. In the expression( )( )thexin the body of the first expression from the left is bound to the first . Theyin the body of the second expression is bound to the second and thexis free. Itis very important to notice that thexin the second expression is totally independentof thexin the first we say that a variable<name>is free in an expression if one of thefollowing three cases holds:2 <name>is free in<name>.
5 <name>is free in <name1> . <exp>if the identifier<name>6=<name1>and<name>is free in<exp>. <name>is free inE1E2if<name>is free inE1or if it is free 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>. <name>is bound inE1E2if<name>is bound inE1or if it is bound should be emphasized that the same identifier can occur free and bound in thesame expression. In the expression( )( )the firstyis free in the parenthesized subexpression to the left. It is bound in thesubexpression to the right. It occurs therefore free as well as bound in the SubstitutionsThe more confusing part of standard Calculus , when first approaching it, is the factthat we do not give names to functions. Any time we want to apply a function, wewrite the whole function definition and then procede to evaluate it.
6 To simplify thenotation, however, we will use capital letters, digits and other symbols as synonymsfor some function definitions. The identity function, for example, can be denoted withIwhich is a synonym for ( ).The identity function applied to itself is the applicationII ( )( )In this expression the firstxin the body of the first expression in parenthesis isindependent of thexin the body of the second expression. We can in fact rewrite theabove expression asII ( )( )The identity function applied to itselfII ( )( )yields therefore[ ]x= Ithat is, the identity function should be careful when performing substitutions to avoid mixing up free oc-currences of an identifier with bound ones. In the expression( x.( ))y3the function to the left contains a boundy, whereas theyat the right is free. Anincorrect substitution would mix the two identifiers in the erroneous result( )Simply by renaming the boundytotwe obtain( x.)
7 ( ))y= ( )which is a completely different result but nevertheless the correct , if the function x. <exp>is applied toE, we substitute allfreeoccur-rences ofxin<exp>withE. If the substitution would bring a free variable ofEinan expression where this variable occurs bound, we rename the bound variable beforeperforming the substitution. For example, in the expression( x.( y.(x( ))))ywe associate the argumentxwithy. In the body( y.(x( )))only the firstxis free and can be substituted. Before substituting though, we haveto rename the variableyto avoid mixing its bound with is free occurrence:[y/x]( t.(x( ))) = ( t.(y( )))In normal order reduction we try to reduce always the left most expression of aseries of applications. We continue until no further reductions are ArithmeticWe expect from a programming language that it should be capable of doing arith-metical calculations. Numbers can be represented in Lambda Calculus starting fromzero and writing suc(zero) to represent 1, suc(suc(zero)) to represent 2, and soon.
8 In the Lambda Calculus we can only define new functions. Numbers will be definedas functions using the following approach: zero can be defined as s.( )This is a function of two argumentssandz. We will abbreviate such expressionswith more than one argument as is understood here thatsis the first argument to be substituted during the evalu-ation andzthe second. Using this notation, the first natural numbers can be definedas1 (z)2 (s(z))3 (s(s(z)))and so first interesting function is the successor function. This can be defined asS (wyx)The successor function applied to our representation for zero yieldsS0 ( (wyx))( )In the body of the first expression we substitute all occurrences ofwwith ( ) andthis yields (( )yx) = (( )x) = (x) 1 That is, we obtain the representation of the number1(remember that variable namesare dummies ).Successor applied to 1 yields:S1 ( (wyx))( (z)) = (( (z))yx) = (y(x)) 2 Notice that the only purpose of applying the number ( (z)) to the argumentsyandxis to rename the variables used in the definition of our AdditionAddition can be obtained immediately by noting that the bodyszof our definitionof the number 1, for example, can be interpreted as the application of the functionsonz.
9 If we want to add say 2 and 3, we just apply the successor function two timesto us try the following in order to compute 2+3:2S3 ( (sz))( (wyx))( (u(uv)))The first expression on the right side is a 2, the second is the successor function, thethird is a 3 (we have renamed the variables for clarity). The expression above reducesto( ((wy)x))(( ((wy)x))( (u(uv)))) SS3 The reader can verify thatSS3reduces toS4= MultiplicationThe multiplication of two numbersxandycan be computed using the followingfunction:( (yz))The product of2by2is then:( (yz))22which reduces to( (2z))The reader can verify that by further reducing this expression, we can obtain theexpected ConditionalsWe introduce the following two functions which we call the values true T false F first function takes two arguments and returns the first one, the second functionreturns the second of two Logical operationsIt is now possible to define logical operations using this representation of the AND function of two arguments can be defined as ( ) OR function of two arguments can be defined as ( )y of one argument can be defined as ( )( ) negation function applied to true is T ( )( )( )which reduces toTFT ( )( )( ) = ( ) Fthat is, the truth value false.
10 A conditional testIt is very convenient in a programming language to have a function which is true ifa number is zero and false otherwise. The following functionZcomplies with thisrequirementZ FTo understand how this function works, note that0fa ( )fa=athat is, the functionfapplied zero times to the argumentayieldsa. On the otherhand,Fapplied to any argument yields the identity functionFa ( )a= I6We can now test if the functionZworks correctly. The function applied to zero yieldsZ0 ( F)0=0F F= F=TbecauseFapplied0times to yields . The functionZapplied to any other numberNyieldsZN ( F)N=NF FThe functionFis then appliedNtimes to . ButFapplied to anything is the identity,so that the above expression reduces for any numberNgreater than zero toIF= The predecessor functionWe can now define the predecessor function combining some of the functions intro-duced above.