# ✓ 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)$
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


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

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}^*$