Josh Bohde

Programming With Only Functions

Posted by Josh Bohde

Python's lambda keyword does not get the love it deserves. It can only execute expressions, instead of statements. With this restriction, we can still make something interesting.

A Tiny Computation System

The lambda calculus is a system of computation based on mathematical functions. It is the foundation for functional languages. This contrasts to the Turing machine, which is the foundation for imperative languages. It turns out that, in Python, all we need to implement the lambda calculus is the lambda keyword.

The identity functions would be:

identity = lambda x: x

Encoding

identity isn't very interesting, so let's do some calculations. Since we have only functions, we need some way to encode numbers as functions. Let's start with zero.

zero = lambda f: identity

zero takes a function f, and returns the identity function. For clarity, this expands to:

zero = lambda f: lambda x: x

After zero, we have one:

one = lambda f: lambda x: f(x)

And then, two, three, and four:

two = lambda f: lambda x: f(f(x))
three = lambda f: lambda x: f(f(f(x)))
four = lambda f: lambda x: f(f(f(f(x))))

Do you see the pattern yet? For a given number n, we can encode it as

n = lambda f: lambda x: f(f(f(....f(x)...)))

Such that there are n fs. This is method of encoding numbers is known as Church encoding.

Decoding

In order to turn an encoded number into a Python number, we need to decode it using a function of the form:

decode = lambda num: num(f)(x)

We know that decode(zero) should be 0 and that zero ignores f. Therefore x should be 0. We also know that f(0) should be 1 and f(f(0)) should be 2, and so on. Therefore f should be lambda x: x + 1. Substituting this, we get our definition of decode:

decode = lambda n: n(lambda x: x + 1)(0)

We can check this real quick:

assert decode(zero) == 0
assert decode(one) == 1

Successors

It would be rather tedious if we had to type out every definition of every number we needed. Is there a way we can get the successor of a number from just the definition of the number? Something like the following:

one = succ(zero)

We know a number definition requires two lambdas, so we'll need three in order to accept the original number. Therefore our definition will look like this:

succ = lambda n: lambda f: lambda x: ????

We know from the definition of decode that we can get the value of a number n by calling it it like n(f)(x). In order to get the successor of n, we'll need one more f. Therefore we have:

succ = lambda n: lambda f: lambda x: f(n(f)(x))

For easy testing, let's declare the following helper function:

equals = lambda x, y: decode(x) == decode(y)
assert equals(succ(zero), one)

Now we can easily define more numbers:

two = succ(one)
three = succ(two)
four = succ(three)
five = succ(four)
six = succ(five)

Addition

Now let us define a function plus that implements addition. An example usage:

assert equals(plus(two)(three), five)

If we think about it, succ could have been defined as plus(one). Is there a way we can include a one in the definition fo succ?

succ = lambda n: lambda f: lambda x: one(f)(n(f)(x))

For plus, we'd like to be able to specify numbers besides one, so we'll add another lambda:

plus = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))

Multiplication

When defining plus, we saw that if we have a a number m, m(f)(x) will add the decoded m to x. We also know that one(f)(x) adds 1 to x. Therefore, m(one(f))(x) should be equivalent to m(f)(x). We can use this to define multiplication:

mult = lambda m: lambda n: lambda f: lambda x: m(n(f))(x)
assert equals(mult(two)(three), six)

Exponents

We've started to combine these base functions we have in interesting ways. Since we know that m(n(f)) in the defintion of mult repeats the addition of n a total of m times, and that plus(n) is the addition of n, we can rewrite mult to use fewer lambdas:

mult = lambda m: lambda n: m(plus(n))(zero)

Since using multiplication to define exponents is a similar to using addition to define multiplication, we should be able to adapt this definition of mult for exp:

exp = lambda m: lambda n: n(mult(m))(one)
equals(exp(two)(two), four)

More Encodings

We aren't limited to just natural numbers when using the lambda calculus. We can encode boolean logic and lists, allowing us to write programs with control flow and data structures.