✓ Evaluation of LC Expressions

LC expressions are strings. LC is a string rewriting system with simple rules that will transform expressions to simpler expressions whenever possible. The string rewriting of LC expressions is known as evaluation.

Free And Bound Variables

Variable occurrence

Let \(e\) be an expression. A variable occurrence is a name at a specific position in \(e\) that does not follow \(\lambda\).


Consider \(e = (x\ \lambda x.x)\).

There are two variable occurrences, both of the name \(x\). To distinguish the two occurrences, we will use subscripts:

\(e = (x_1\ \lambda x.x_2)\)

Free occurrences


Let \(\mathrm{Var}(e)\) be the variable occurrences in \(e\). We define the free occurrences \(\mathrm{Free}(e)\) by induction as follows:

  • \(\mathrm{Free}(x) = \{x\}\)

  • \(\mathrm{Free}(\lambda x.e) = \mathrm{Free}(e) - \{x\}\). Namely, any free occurrences of \(x\) in \(e\) is not considered free in \(\lambda x.e\).

  • \(\mathrm{Free}(e_1\ e_2) = \mathrm{Free}(e_1)\cup\mathrm{Free}(e_2)\)

Bound occurrences


The bound occurrences of \(e\) is given by:

\[\mathrm{Bound}(e) = \mathrm{Var}(e) - \mathrm{Free}(e)\]

Some examples

Base cases

  • \(\mathrm{Free}(y) = \{y\}\)

  • \(\mathrm{Free}(x) = \{x\}\)

  • \(\mathrm{Free}(z) = \{z\}\)

Function application

  • \(\mathrm{Free}((x\ y)) = \mathrm{Free}(x) \cup \mathrm{Free}(y) = \{x\}\cup\{y\} = \{x, y\}\)

Function abstraction

  • \(\mathrm{Free}(\lambda z. z) = \mathrm{Var}(z) - \{z\} = \emptyset\)

  • \(\mathrm{Free}(z_1\ \lambda z. z_2) = \mathrm{Free}(z_1)\cup\mathrm{Free}(\lambda z. z_2) = \{z_1\}\cup\emptyset = \{z_1\}\)

Note: since there are two occurrences of \(z\), we need to distinguish them by the subscripts \(z_1\) and \(z_2\). Only the first occurrence \(z_1\) is free.

  • \(\mathrm{Free}((x\ y)\ (z_1\ \lambda z.z_2)) = \{x,y\}\cup\{z_1\} = \{x, y, z_1\}\)

  • \(\mathrm{Free}(\lambda y.((x\ y)\ (z_1\ \lambda z.z_2))) = \mathrm{Free}((x\ y)\ (z_1\ \lambda z.z_2)) - \{y\} = \{x, z_1\}\)

  • \(\mathrm{Free}(\lambda x.\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) = \mathrm{Free}(\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) - \{x\} = \{z_1\}\)

  • \(\mathrm{Free}(x\ \lambda x.\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) = ?\)

Note: There are two occurrences of \(x\), so we need to disambiguate them.

\[\begin{split} \begin{eqnarray} && \mathrm{Free}((x_1\ (\lambda x.\lambda y.(x_2\ y)\ (z_1\ \lambda z.z_2)))) \\ &=& \mathrm{Free}(x_1)\cup\mathrm{Free}(\lambda x.\lambda y.(x_2\ y)\ (z_1\ \lambda z.z_2)) \\ &=& \{x_1\} \cup \{z_1\} \\ &=& \{x_1, z_1\} \end{eqnarray} \end{split}\]

Thus the first \(x\) and the first \(z\) are free.

Variable substitution


Consider an expression \(e\) containining some variable \(x\). We can perform substitution of all free occurrences of \(x\) in \(e\) by some other expression \(e'\). The resulting expressions is written as \(e[x/e']\).


(1)\[\begin{eqnarray} && (x\ \lambda x.\lambda y.(x\ y)\ (\underbrace{z}_{\mathrm{free}}\ \lambda z.\underbrace{z}_{\mathrm{bound}})) [z/(u\ v)] \\ &=& (x\ \lambda x.\lambda y.(x\ y)\ ((u\ v)\ \lambda z.z_2)) \end{eqnarray}\]

Reduction rules of Lambda Calculus

  • \(\alpha\)-conversion: changing bound variable

  • \(\beta\)-reduction: applying functions to their arguments

  • \(\eta\)-reduction: function equivalence



Given a function expression \(\lambda x.e\), if \(z\not\in\mathrm{Free}(e)\), we have:

\[ \lambda x.e = \lambda z.e[x/z] \]

The \(\alpha\)-conversion is also known as parameter renaming. It states that a function declaration is invariant to the name of its parameter as long as the parameter does not interfer with existing variables of the function’s body.


Consider the following function abstraction.

\[ \lambda x.x \]
def f(x):
  return x

We can change the parameter name to some other name without changing the function. This type of equivalence is ensured by the \(\alpha\)-conversion.

\[\begin{split} \begin{eqnarray} && \lambda x.x \\ &=& \lambda z. x[x/z] \\ &=& \lambda z. z \end{eqnarray} \end{split}\]
def f(z):
  return z


But we must be careful that the parameter renaming does not shadow existing variables in the function body. Now consider another function abstraction:

\[ (\lambda x. \pi) \]
from numpy import pi
def f(x):
  return pi

A careless parameter renaming can change the function that is being defined.

\[ (\lambda \pi. \pi) \]
from numpy import pi
def f(pi):
  return pi



Consider function application \(((\lambda x. \mathrm{body})\ e_2)\).

If we have \(\mathrm{Var}(e_2)\cap\mathrm{Bound}(\mathrm{body}) = \emptyset\), then we can perform the following transformation:

\[ ((\lambda x.\mathrm{body})\ e_2) \rightarrow \mathrm{body}[x/e_2] \]



For any expression \(e\), we have:

\[ (\lambda x.(e\ x)) \rightarrow e \]

Expression reduction

We process expressions by applying the rewrite rules (\(\alpha\)-conversion, \(\beta\)- and \(\eta\)-reductions) successively during the reduction process.

\[ e_0 \underset{\alpha}{\longrightarrow} e_1 \underset{\beta}{\longrightarrow} e_2 \underset{\eta}{\longrightarrow} e_3 \underset{\beta}{\longrightarrow} \dots \]

We say that \(e'\) is reduced from \(e\) if there is some way to rewrite \(e\) to \(e'\) using zero or more rewritings.

\[ e \Longrightarrow e' \]

Normal form


An expression \(e\) is in normal form if no more reductions (\(\beta\) or \(\eta\)) can be applied. Namely, all function applications have been applied.

Given \(e\), its normal form, written \(e^*\), is an expression such that:

  • \(e^*\) is in normal form and

  • \(e\Rightarrow e^*\).

We denote all normal form lambda calculus expressions as \(\mathbf{LC}^*\).

Computation using LC


Given a problem \(\mathbf{P}\), we encode the instances as LC expressions:

\[ \mathbf{Enc}: \mathbf{P} \to\mathbf{LC} \]


We only are interested in decoding expressions in normal forms.

\[ \mathbf{Dec}:\mathbf{LC}^*\to\mathbf{sol}(\mathbf{P}) \]


To implement an algorithm using Lambda Calculus, we need to take the following steps:

  1. Encode an instance as an expression \(e_0 = \mathbf{Enc}(\mathrm{instance})\).

  2. Perform \(\alpha,\beta,\eta\) rewriting to arrive at a normal form of \(e_0\).

  3. Decode the result \(e_0^*\) to recover the solution \(\mathbf{Dec}(e^*_0)\).

Thus, the crucial step in LC-based computation is the step of finding a normal form of an expression:

\[ \mathrm{compute} : \mathbf{LC} \to \mathbf{LC}^* \]