## HOWTO: Lambda Calculus

Andy’s quickstart guide for Î»-Calculus. This is intended to be useful for the Computing and Complexity coursework \o/.

Î»-terms consist of the following alphabet:

x, y, z, …: (bound) variables

Î»

(,): parentheses

Every term of a statement is a function:

xtakes no arguements

Î»x.MmapsxtoM(x)

MNapplies the functionMto the arguementN

Example functions:

Î»x.x– the identity function

Î»x.Î»y.x– takes one arguement (x), waits for a second arguement (y), and then returnsx.

Comparing C and Î»-Calculus:

C:

int id (int i) {

return i;

}

Î»-Calculus:

Î»x.x

Î»-Calculus functions only take a single arguement. It is possible to simulate multiple arguements by using multiple Î» functions that take a single arguement at a time.

Taking the function *f(x) = x + 2*, you would get the *Î»* expression *Î» x.(x + 2)*; and *f(2)* would be written as *(Î» x.(x + 2))2*.

If for a multi-arguement function, say Î»xy.M, you applied the arguements N and L, you would initiall get (Î»xy.M)(N), and then (Î»xy.M)NL, which translates to mean M[x := N, y := L].

**Reduction** is the process of simplifying an expression. There is no fixed order of reduction and he process can be mechanised. Reduction is non-deterministic

[( 3 * 8 ) – ( 5 + 12 )] ( x+7 )

-> [( 3 * 8 ) – ( 17 )] ( x + 7 )

-> [( 24 ) – ( 17 )]( x + 7 )

-> [7]( x + 7 )

-> ( 7 * x ) + ( 7 * 7 )

-> (7 * x) + ( 49 )

Reducing a Î» is fairly simple, just take the left most variable and replace it throughout that expression with the left most arguement. If you have a sub-expression, deal with that one first before you continue with the main expression.

For example:

(

Î»pca.pca)(Î»xy.x)MN

-> (Î»ca.(Î»xy.x)ca)MNremove p from the arguements list (already “used”) and put in the first arguement.

->(Î»ca.(Î»y.c)a)MNx has been replaced with c (the left most arguement to that expression)

-> (Î»ca.c)MNy has been replaced with a and ignored, so the sub-expression evaluates to c-> (

Î»a.M)Nc has been replaced by M

-> Ma has been replaced by N and ignored.

Alpha-congruence is when M can be turned into N by a sequence of changes in bound variables. For example:

Î»x.x =Î»y.y

and

Î»ab.a =Î»xy.x

As the actual nameing of the bound variables should have no bearing on the outcome of the function. Formally:

A change of bound variables in term M is the replacement of a sub

termÎ»x.Nof M byÎ»y.N[ c := y ], whereydoes not occur inx.

If M and N can be shown to be equal, then we write:

Î» |- M = N

Extensionality is where two functions *f(x)* and *g(x)* are equal for all permissible values of x. For example, a quick sort and a bubble sort are both clearly different algorithms, yet they are extensionally equiivalent.

Incompatable terms are denoted by *(M#N)* and are defined by:

incompatable if Î» + (M = N) is not consistent.

Normal Form: an expression, M, is in normal form if it contains no subterms of the form (*Î»x.R)S*. For example:

Î»x.xis a nf

(Î»xy.x)(Î»x.x)has Î»yx.x as a nf

(Î»x.xx)(Î»x.xx)has no nf

*more coming soon…*