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 $.