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\).