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


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?


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


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


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


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


  • \(\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})\)


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