This material is from
A Tutorial Introduction
to the Lambda Calculus
There is not original and is not presented as such; the document is for my use; I Anil Mitra may want to change that in the future. Note: I recognize that this material is specialized and tailored to programming languages. April 26, 2015.
To be defined: the keywords LAMBDA and DOT.
To be defined: the NAME or VARIABLE (identifier)
A ‘name’, also called a ‘variable’ is an identifier which can be any letter a, b, c, …
To be defined: EXPRESSION, FUNCTION, and APPLICATION.
<expression> := <name> | <function> | <application>
<function> := λ <name>.<expression>
<application> := <expression><expression>
In a function, ‘λ <name>’ (before the dot) is called the head and the <expression> after the dot is the body.
An expression can be surrounded with parentheses for clarity: if E is an expression (E) is an expression.
That is, E1E2E3 … En is the same as (… ((E1E2)E3) … En)
To simplify notation capital letters, digits, and other symbols may be used as synonyms for some function definitions.
How do we evaluate functions? The term ‘evaluation’ comes from the terminology f(x) in which given an x, the function is evaluated according to the rule f.
However, in the λ calculus functions do not have names. A function applied to an expression may be simplified by SUBSTITUTION (below). This is the only rule for ‘evaluation’ of functions in the λ calculus.
From the recursive definition a single identifier (variable or name, e.g. x) is an expression. Therefore λx.x is an expression.
If a function (λ <name>.<expression1>) applied to an expression (<expression2>) the application is λ <name>.<expression1><expression2>.
SUBSTITUTE <expression2> for all occurrences of the <name> in <expression1>.
Or, substitute all instances of the name in the head expression by the expression to which the function is applied.
If the function λx.x is applied to y, the result is λx.xy or (λx.x)y for clarity. From the substitution rule the function REDUCES to y. Therefore λx.x is (called) the IDENTITY function denoted by I which is a synonym for (λx.x).
Applying the identity function two times:
II = (λx.x) (λx.x) = (λx.x) (λy.y) = (λy.y) = I
Note that the names of the arguments in function definitions are placeholders and do not have meaning by themselves:
λx.x º λy.y º λz.z º λt.t …
In λ calculus all names are local to definitions. In the function λx.x we say that x is ‘bound’ since its occurrence in the body of the definition is preceded by λx. A name not preceded by a λ is called a ‘free variable’. In the expression
the variable x is bound and y is free. In the expression
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 x is free. It is very important to notice that the x in the second expression is totally independent of the x in the first expression.
Formally we say that a variable <name> is free in an expression if one of the following three cases holds:
§ λ <name> is free in <name>.
§ λ <name> is free in λ <name1 > . <exp> if the identifier <name> ≠ <name1 > and <name> is free in <exp>.
§ λ <name> is free in E1E2 if <name> is free in E1 or if it is free in E2.
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>.
§ λ <name> is bound in E1E2 if <name> is bound in E1 or if it is bound in E2.
It should be emphasized that the same identifier can occur free and bound in the same expression. In the expression
the first y is free in the parenthesized sub expression to the left. It is bound in the sub expression to the right. It occurs therefore free as well as bound in the whole expression.
The y in the inner parentheses is bound while the outer y is free. Therefore replacing x by y in the inner expression results in the incorrect result (λy.yy). To obtain the correct result rename the free y as t to get
which is correct. However, since in the original expression y was free we might want it to be free in the final expression. So we would then replace the inner y by t to get
which is also correct but may be more convenient.
Therefore, if the function λx. <expression> is applied to E, we substitute all free occurrences of x in <expression> with E. If the substitution would bring a free variable of E in an expression where this variable occurs bound, we rename the bound variable before performing the substitution. For example, in the expression
we associate the argument x with y. In the body
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 is free occurrence:
(λx.(λt.(x(λx.xt))))y = [y ® x](λt.(x(λx.xt))) = (λt.(y(λx.xt)))
In normal order reduction we try to reduce always the left most expression of a series of applications. We continue until no further reductions are possible.
Define 0 (zero) as λs.(λz.z) which has two arguments s and z and is abbreviated λsz.z with the understanding that s is the first and z the second argument to be substituted in the evaluation (any reduction). Using this notation define:
0 º λsz.z
1 º λsz.s(z)
2 º λsz.s(s(z))
3 º λsz.s(s(s(z)))
Define the successor function
S º λwyx.y(wyx)
S0 º (λwyx.y(wyx))(λsz.z) º (λyx.y((λsz.z)yx)) º λyx.y((λsz.z)yx) º λyx.y((λz.z)x) º λyx.y(x) º 1
S1 º (λwyx.y(wyx))(λsz.s(z)) º λyx.y((λsz.s(z))yx) º λyx.y((λz.z)yx) º λyx.y((y)x) º 2
S2 º (λwyx.y(wyx))(λsz.s(s(z))) º λyx.y((λsz.s(s(z)))yx) º λyx.y(y(y)x) º λyx.y(y(y(x))) = 3
Note that Sn = n + 1 but
nS = SS…S (n times)
Therefore S and n do not commute
nSm = n + m
But nSm ≠ n(m+1) because of l ® r evaluation.
1 x 3 = 3 = SSS0
2 x 3 = 3 + 3 = 3+ SSS0 = SSSSSS0
3 x 3 = 3 + 3 + 3 = SSSSSSSSS0
n x m = ((n' x m') S) 0
where n' and m' are natural numbers so (n' x m') S means S applied n' x m' times.
Suppose we had a multiplication operator M. Then
nMm = ((n' x m') S) 0
μ = (λxyz.x(yz))
nμm=(n'S0)μ(m'S0) … reductions … = ((n' x m') S) 0
Therefore one candidate for M is μ, i.e. one M is
M = (λxyz.x(yz))
Note that for any function f
0fa = a
T = λxy.x and F= λxy.y,
TAB = A and FAB = B
TA = A and FA = I (identity)
— T = F and — F = T
Let Z = IF—F
Z0 = IF—F0 = 0F—F = —F = T
but, for N not zero
ZN = IF—FN = NF—F = (FFF… n times … F)—F
and since F applied to anything is the identity this results in
ZN = F
That is, ZN is T or F as N is zero or another natural number.
The predecessor P, if there is one, would be the ‘inverse’ of S:
PS = I.
If π is a pair (a,b) it can be represented by λz.zab or Iab. Then πT = a and πF = b.
If a function Φ is such that given a pair of numbers π = (r,r-1) then Φπ = (r+1,r) it can generate the predecessor of n by application to (0,0) or I00 n times and selecting the second number. In the case of 0, however, the predecessor would be 0. That is, this procedure results in 0 ® 0 but otherwise n ® n-1.
The following is one such function:
Φ º (λpz.z(S(pT))(pT)).
Thus, applying Φ n times:
P = (λn.nΦ(λz.z00)F
and selecting the second member of the result (pair) gives the predecessor.
(λxy.Z(xPy)) = 0 then x >= y.
(λxy.&(Z(xPy))(Z(yPx))) = 0 then x = y.
Consider the ‘recursion’ operator
Y º (λy.(λx.y(xx))(λx.y(xx)))
It has the property that for a function R
YR = R(YR).
R º (λrn.Zn0(nS(r(Pn)))).
It then follows that
YRn = nS(YR(n-1)).
Thus, noting that YR0 = 0,
YR3 = 3S(YR2) = 3S(2S(YR1)) = 3S(2S(1SYR0)) = 6.