Luis Ziliani

Luis Ziliani

Arithmetic with Lambda Calculus

6 min
May 2 2008
6 min
May 2 2008

One simple way to make arithmetic expressions in lambda calculus, is just to extend the calculus with the arithmetic rules:

(λx.(λy. x+y)) 2 3 → (λy. 2+y) 3 → 2+3 = 5

But that's pretty easy for us, and (as you problably have already noticed) we like to complicate what's easy. So let's try to make the sum with the base lambda calculus. Why? Because it's fun!

First of all, a bit of notation: let's say that we can write the expression (λx.(λy. T)) (i.e. the function that takes a parameter and returns the function that takes another parameter and returns the generalized term T) as λx y. T

Secondly, I highly recomend you to follow the examples in paper, trying to see why one step lead to another.

In the beginning there was a Beta reduction... But He (Alonso Church) says "Let there be the numerals", and the numerals appears:

0: (λf x.x)

1: (λf x. f x)

2: (λf x. f (f x))


N: (λf x.f (... f (f x))

This is just a way of doing this. You can say "for me, the 0 is (λx.x), the 1 is (λx y. y), ...". Or "for me, all this stuff is pure crap. Got a life, you punk!". I choose this way for one simple reason: it is in the wikipedia, and it looks good and easy to use.

So the numerals are functions. Why? What's the meaning of that? Let's try to answer. The 1 is saying "given two parameters, we apply the first one to the second one". And the N says: "given two parameters, we apply N times the first one to the second one". So it's looks like a for loop expression in a normal programming language. In order to answer to the first question, let's show how to sum:

SUM: (λn1 n2 f x. n1 f (n2 f x))

Note: because all the numerals takes two parameters, it is expected that the Sum function returns some numeral that also takes two numbers. That's why we receive the two numerals (n1 and n2) and the two parameters every numeral needs (f and x). Let's make a simple sum:

SUM 2 1: (λn1 n2 f x. n1 f (n2 f x)) (λf x. f (f x)) (λf x. f x) → we replace n1 by the first numeral: (λn2 f x. (λf x. f (f x)) f (n2 f x)) (λf x. f x) → we replace n2 by the second numeral → (λf x. (λf x. f (f x)) f ((λf x. f x) f x))

This is a mess of f and x, so let's try to make a difference between them. I will put gay colors in it.

f x. (λf x. f (f x)) f ((λf x. f x) f x))

We can reduce the orange numeral with the fucsia variables:

f x. (λf x. f (f x)) f ((λf x. f x) f x)) → (λf x. (λf x. f (f x)) f ((λx. f x) x)) → (λf x. (λf x. f (f x)) f (f x))

Now we can reduce the green numeral with the fucsia f (we have to change f by f), and then we can replace the green x by the fucsia (f x) expression:

f x. (λf x. f (f x)) f (f x)) → (λf x. (λx. f (f x)) (f x)) → (λf x. f (f (f x)))

And now everything is girly fucsia! And what does this expression means? The numeral 3 of course!

If you want to play more with this arithmetic way of computations, you can try to define the other functions (multipication, predecesor, etc). Or you can take a look at