# ✓ 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:

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

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

## 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:

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.

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

```
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:

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

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

```
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:

## \(\eta\)-Reduction¶

Definition

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

## Expression reduction¶

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

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

## 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:

### Decoding¶

We only are interested in decoding expressions in normal forms.

### 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: