## 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:

x takes no arguements

Î»x.M maps x to M(x)

MN applies the function M to the arguement N

Example functions:

Î»x.x – the identity function

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

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 )

-> ( 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)MN remove p from the arguements list (already “used”) and put in the first arguement.

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

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

-> (Î»a.M)N c has been replaced by M

-> M a 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 subterm Î»x.N of M by Î»y.N[ c := y ], where y does not occur in x.

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.x is a nf

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

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

more coming soon…