Lambda Calculus

Lambda Expressions

The following expressions and any expression derived from them are lambda terms.

Variables

We assume there is an infinite set of variables which we usually write as $ x $, $ y $, and $ z $. Every variable is a lambda term.

Applications

Where $ M $ and $ N $ are lambda terms, then the juxtaposition of them surrounded by round brackets is:

$ (M \ N) $

We say $ M $ is applied to $ N $: $ M $ is considered a function and $ N $ its input.

Abstractions

Where $ x $ is a variable and $ M $ is a lambda term then the following is also a lambda term:

$ ( \lambda x . M ) $

Free and Bound Variables

In a given lambda term, a variable is either bound or free, as defined below. Note that it may be necessary to perform $ \alpha $ substitution to avoid confusion between the bound variables of two terms.

Free

$ F(x) = \{ x \} $

$ F(( M \ N )) = F(M) \cup F(N) $

$ F( \lambda x . M ) = F(M) \setminus \{ x \} $

Bound

$ B(x) = \{ \} $

$ B(( M \ N )) = B(M) \cup B(N) $

$ B( \lambda x . M ) = B(M) \cup \{ x \} $

Substitutions

$ \alpha $ Reduction

$ \lambda x . M $ $ \rightarrow_\alpha $ $ \lambda y . M[x/y] $

where $ M[x/y] $ means replace all free occurances of $ x $ with $ y $.

$ \beta $ Reduction

$ ( ( \lambda x . M ) \ N) $ $ \rightarrow_\beta $ $ M[x/N] $

where $ M[x/N] $ means replace all free occurances of $ x $ with $ N $.