✓ Integer arithmetics in LC¶

About integer arithmetics¶

Some questions¶

Let’s first examine what integer arithmetics is.

Q1: What is 42?
Q2: What is 10?

Q3: What is 42 + 10?

A TM approach¶

A1: Encode 42 into a binary string encode(42) = 000101010
A2: Encode 10 into a binary string encode(10) = 000001010

Then addition can be implemented as a bit-manipulation function.

A Turing Machine that performs bit-addition of two numbers.

Source: https://stackoverflow.com/questions/59045832/turing-machine-for-addition-and-comparison-of-binary-numbers

The challenge¶

How do we represent numbers (e.g. 10 or 42) as LC expressions?
How do we trigger computation so we can obtain the result of arbitrary arithemtic operations?

Encoding integers using LC expressions¶

We will count by the number of times a function is applied to some input.

\[ x \underbrace{\to (f x) \to (f (f x)) \dots \to (f (f \dots (f x)))}_{\mathrm{count}} \]

General integer encoding¶

A whole number \(n\geq 0\) is actually a function with two inputs:

\[ n(f, x) = \underbrace{f(f(\dots f}_{n}(x))) \]

This needs to be done in LC.

Encoding 0¶

The encoding for 0 is a function that accepts two parameters \(f\) and \(x\), but applies \(f\) zero times to \(x\). Thus, the result is just \(x\).

\[ 0 = \lambda f.(\lambda x. x) \]

Encoding 1, 2, 3, \(\dots\)¶

It’s easy to see:

\(1 = \lambda f.\lambda x.(f x)\)
\(2 = \lambda f.\lambda x.(f (f x))\)
\(\vdots\)

Encoding arithemtics¶

Now, we need to figure out how to represent integer arithmetics such as m+n, m*n, m^n as functions expressed in LC.

Successor¶

We start with the successor function \(S(n) = n + 1\).

Let’s take a look at the parts:

\(n\) is a function with two parameters: \(n(f,x)\)
\((n+1)\) needs to be a function with two parameters:

Therefore, \(S\) needs to be defined as \(S(n, f, x) = \dots\).

\[ S = \lambda n.\lambda f.\lambda x.(f (n f x)) \]

Note, \((S n)\) applies \(f\) \(n+1\)-times to the input \(x\). Thus, \((S n) = n+1\).

Computing the successor¶

Question: How do we compute the successor of 1?

Answer:

We need to encode the instance successor(1) into a LC expression:

\[ (S\ 1) = (\underbrace{\lambda n.\lambda f.\lambda x.(f (n f x))}_{S}\ \underbrace{(\lambda f.\lambda x.(f\ x))}_{1} \]

Then apply \(\alpha\), \(\beta\) and \(\eta\) rewrite rules to derive a normal form.

The normal form of \((S\ 1)\)¶

S1 = (λn.λf.λx.(f ((n f) x))) (λf.λx.(f x))
   = (λw.λy.λx.(y ((w y) x))) (λs.λz.(s z))  [parameter renaming]
   = λy.λx.(y ((w y) x))[w/(λs.λz.(s z))]
   = λy.λx.(y (((λs.λz.(s z)) y) x))
   = λy.λx.(y ((λz.(y z)) x))
   = λy.λx.(y (y x))
   = 2

Addition¶

Building addition in Python¶

Let’s express the number encodings and the successor function in Python.

def repeat(n, f, x):
    for i in range(n):
        x = f(x)
    return x

def succ(n):
    return n + 1

We can express addition using these functions.

def addition(m, n):
    return repeat(m, succ, n)

addition(5, 6)

Building addition in LC¶

repeat is \(n\).
succ is \(S\) as defined.

Now, we can define addition as a LC expression:

\[ + = \lambda m.\lambda n.\lambda f.\lambda x.(m\ S\ n) \]

Multiplication¶

Observe: \(m\times n = 0 + \underbrace{n + n + \dots + n}_{m}\)

Multiplication can be expressed as \(m\) repeated applications of addition of \(n\) to 0.

A function that adds \(n\) to its input¶

\[ h = \lambda x.(n\ S\ x) \]

Defining multiplication¶

\[\begin{split} \begin{eqnarray} \times &=& \lambda m.\lambda n.(m\ h\ 0) \\ &=& \lambda m.\lambda n.(m\ (\lambda x.(n\ S\ x)\ 0) \end{eqnarray} \end{split}\]

Exponentiation¶

Can you define \(\mathrm{power} = \lambda m.\lambda n.\dots\)?

Boolean logic¶

Truth values¶

\(\mathbf{True} = \lambda x.\lambda y.x\)
\(\mathbf{False} = \lambda x.\lambda y.y\)

Operators¶

\(\mathbf{and} = \lambda x.\lambda y.(x\ y\ \mathbf{False})\)
\(\mathbf{or} = \lambda x.\lambda y.(x\ \mathbf{True}\ y)\)
\(\mathbf{not} = \lambda x.(x\ \mathbf{False}\ \mathbf{True})\)

If-else¶

Can you define \(\mathbf{ifelse} = \lambda \mathrm{cond}.\lambda x.\lambda y.\dots\)?