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

Example

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¶

Definition

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¶

Definition

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¶

Definition

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

Example¶

(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

\(\alpha\)-conversion¶

Definition

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.

Example:¶

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

Example¶

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

This is a function that always returns a constant \(\pi\) (3.1415…)

from numpy import pi
def f(x):
  return pi

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

\[ (\lambda \pi. \pi) \]

This is the identity function, returning the argument.

from numpy import pi
def f(pi):
  return pi

\(\beta\)-Reduction¶

Definition

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] \]

\(\eta\)-Reduction¶

Definition

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¶

Definition

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¶

Encoding¶

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

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

Decoding¶

We only are interested in decoding expressions in normal forms.

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

Computation¶

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

Encode an instance as an expression \(e_0 = \mathbf{Enc}(\mathrm{instance})\).
Perform \(\alpha,\beta,\eta\) rewriting to arrive at a normal form of \(e_0\).
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}^* \]