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:


int id (int i) {

return i;




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


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


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

Leave a Reply