This material is from
A Tutorial Introduction to the Lambda Calculus
Raul Rojas
The link is: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

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. November 14, 2023.

My home page

CONTENTS

There are two keywords

Name or variable

Recursive definition of expressions

Note

Parentheses

Function application associates from the left

Functions do not have names

Free and bound variables

There are two keywords

To be defined: the keywords LAMBDA and DOT.

λ (lambda)

. (dot)

Name or variable

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, …

Recursive definition of expressions

To be defined: EXPRESSION, FUNCTION, and APPLICATION.

Note

In a function, ‘λ <name>’ (before the dot) is called the head and the <expression> after the dot is the body.

Parentheses

An expression can be surrounded with parentheses for clarity: if E is an expression (E) is an expression.

Function application associates from the left

That is, E₁E₂E₃ … E_n is the same as (… ((E₁E₂)E₃) … E_n)

Functions do not have names

To simplify notation capital letters, digits, and other symbols may be used as synonyms for some function definitions.

Function evaluation

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.

Substitution

If a function (λ <name>.<expression₁>) applied to an expression (<expression₂>) the application is λ <name>.<expression₁><expression₂>.

Substitution rule

SUBSTITUTE <expression₂> for all occurrences of the <name> in <expression₁>.

Or, substitute all instances of the name in the head expression by the expression to which the function is applied.

Identity function

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 …

Free and bound variables

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

(λx.xy)

the variable x is bound and y is free. 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 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 λ <name₁ > . <exp> if the identifier <name> ≠ <name₁ > and <name> is free in <exp>.

§ λ <name> is free in E₁E₂ if <name> is free in E₁ or if it is free in E₂.

A variable <name> is bound if one of two cases holds:

§ λ <name> is bound in λ <name₁ > . <exp> if the identifier <name>=<name₁ > or if <name> is bound in <exp>.

§ λ <name> is bound in E₁E₂ if <name> is bound in E₁ or if it is bound in E₂.

It should be emphasized that the same identifier can occur free and bound in the same expression. In the expression

(λx.xy)(λy.y)

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.

More on substitution

(λx.(λy.xy))y

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

(λx.(λy.xy))t

(λy.ty)

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

(λx.(λt.xt))y

(λt.yt)

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

(λx.(λy.(x(λx.xy))))y

we associate the argument 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 is free occurrence:

(λt.(x(λx.xt)))

to get

(λ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.

Arithmetic

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)

Then

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

and

S1 º (λwyx.y(wyx))(λsz.s(z)) º λyx.y((λsz.s(z))yx) º λyx.y((λz.z)yx) º λyx.y((y)x) º 2

and

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

Some formulas

Note that Sn = n + 1 but

nS = SS…S (n times)

Therefore S and n do not commute

Addition

Therefore

nSm = n + m

But nSm ≠ n(m+1) because of l ® r evaluation.

Multiplication

1 x 3 = 3 = SSS0

2 x 3 = 3 + 3 = 3+ SSS0 = SSSSSS0

3 x 3 = 3 + 3 + 3 = SSSSSSSSS0

i.e.

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

Suppose

μ = (λxyz.x(yz))

then

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

Conditionals

Consider

T = λxy.x and F= λxy.y,

then

TAB = A and FAB = B

and

TA = A and FA = I (identity)

Logical operations

Let

& = λxy.xyF		(‘and’: a function of two arguments),
or = λxy.xTy		(logical ‘or’: a function of two arguments), and
— = λx.xFT		(‘negation: a function of one argument).

Then

— T = F and — F = T

Conditional

Let Z = IF—F

Then

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.

Predecessor

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.

Equality

(λxy.Z(xPy)) = 0 then x >= y.

(λxy.&(Z(xPy))(Z(yPx))) = 0 then x = y.

Recursion

Consider the ‘recursion’ operator

Y º (λy.(λx.y(xx))(λx.y(xx)))

It has the property that for a function R

YR = R(YR).

Consider

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.