{:check ["true"], :rank ["encoding" "arithmetics" "summary"]}

Index

Arithmetics in $\lambda$-Calculus

The problem $\mathbf{P}$

We need to encode the following values and operators as $\lambda$-calculus expressions.

Integers: 0, 1, 2, ...

Addition: $x+y$

Multiplication: $x\times y$

Exponentiation: $x^y$

Any valid integer arithmetics: $34 * (31 + 89^7)$

The solution

$\lambda$-Calculus will reduce the expression to a normal form which represents the answer as an integer value.

Encoding

Integers

Encoding zero

box

The encoding of zero is given as: $$\mathbf{Encode}(0) = \lambda s.\lambda z. z$$

We will simply write it as $0 = \lambda s.\lambda z. z$ It represents a function with two arguments (with currying): It simply returns the second argument.

The intuition is that the first argument $s$ is a function that is applied to the second argument $z$ zero times.

Encoding $n$

box

Now, we can generalize the encoding of zero to other positive integers. They will be functions with two arguments applying the first argument repeatedly.

$1 = \lambda s.\lambda z.(s\ z)$

$2 = \lambda s.\lambda z.(s\ (s\ z))$

$3 = \lambda s.\lambda z.(s\ (s\ (s\ z))$

$\vdots$

Arithmetics

Arithmetic Operations

Now, we are ready to represent the arithmetic operations in $\lambda$-calculus.

Successor

The definition:
The successor function returns the next integer. It can be expressed in Python as:
```
def successor(n):
    return n + 1
```
In $\lambda$-calculus, the encoding for the successor function is given as:

$$S = \lambda n.\lambda f.\lambda x.(f\ ((n\ f)\ x))$$

Given an integer expression, $n$, we claim that $(S\ n)$ evaluates to the integer expression for $n+1$.
It helps to get some intuition behind the definition of $S$.

The input of $S$ is a number $n$ given as $n(f,x) = \underbrace{f f f \dots f}_{n\ \mathrm{times}} (x)$.

So, the action of $S$ can be explained as:

$$\begin{eqnarray} && S(n, f, x) \ &=& f(n(f,x)) \ &=& f(\underbrace{f f f \dots f}_{n\ \mathrm{times}}(x)) &=& (n+1)(f, x) \end{eqnarray}$$

Therefore, $$ (S\ n) = (n+1) $$

Addition

The definition:

The addition $m+n$ can be implemented using repeated application of the successor function $m$-times to the number $n$.
def add(m, n):
    result = n
    for i in range(m):
        result = successor(result)
    return result

We can express it as a $\lambda$-calculus expression:

$$ + = \lambda m.\lambda n.(m\ S\ n)$$
The intuition:

Observe that $(m f x) = (\underbrace{f\dots f}_{m\ \mathrm{times}} x)$. Therefore, with $f = S$ and $x = n$, we have: $$ \begin{eqnarray} (m S n) &=& (\underbrace{S\dots S}_{m\ \mathrm{times}} n) \\ &=& n + \underbrace{1 + 1 \dots+1}_{m\ \mathrm{times}} \\ &=& n + m \end{eqnarray} $$

Multiplication

The definition:

Let's first express multiplication using additions.

def multiply(m, n):
    result = 0
    for i in range(m):
        result = add(result, n)
    return result

Encoding multiplication in $\lambda$-calculus:

We observe that multiply(m,n) is applying the function $\lambda$x.add(n,x) to 0 repeatedly $m$ times.

$$\times = \lambda m.\lambda n.m(\lambda x. nSx)0$$ where recall $0 = \lambda f.\lambda z.z$.

Exponentiation

The definition:

The exponentiation procedure can be expressed in terms of multiplication:

$$ m^n = \underbrace{m\times m\times m\times \dots \times m}_{n\ \mathrm{times}} \times 1 $$
This can be expressed in $\lambda$-calculus:

$$ m^n = (n\ (\lambda x. (\times\ m\ x))\ 1) $$ where $1 = \lambda f.\lambda z.(f\ z)$

As a proper $\lambda$-calculus expression, we define:

$$ \exp = \lambda m.\lambda n.(n\ (\lambda x. (\times\ m\ x))\ 1) $$

Summary

box

$\lambda$-calculus can be used to express integers and basic arithmetic operations.

Any integer arithmetic problems (e.g. $10 \times (3 + 423)^{42}$) can be encoded into a $\lambda$-calculus expression.

Using the rewrite rules, the resulting normal form is the answer.