Notes on λ Calculus - Church Encoding

$\lambda$ calculus can express numbers, arithmetic on numbers, booleans, logical operations and even list. Alonzo Church who invented $\lambda$ calculus, first encoded numbers and other structures in this way, so we call it Church Encoding.

Currying

At the beginning, I will briefly talk about curry function. In practical programming languages, a function could take many arguments. While the curry function cloud take only one argument. If we have multiply arguments for a function, then we build a nested functions: each of them takes one argument and return another function, until the actual function body.

For example, a function takes two arguments $x$ and $y$ and add it, we may have a curry function:

$$ \lambda x. \lambda y. x + y $$

we can also express it non-currying which are equivalent

$$ \lambda x y. x + y $$

Curry function has its advantages. It makes function cloud easily compose. Another exmple for the add function, we can obtain a $increase$ function just pass 1 as $x$ to curry add function above without actual evaluation:

$$ inc = (\lambda x. \lambda y. x + y)(1) = \lambda y. 1 + y $$

In the followings about Church Encoding, we will see curry function frequently.

Numbers

Mathematically say, we can define natural number $\mathbf{N}$ as a set:

0 is in $\mathbf{N}$, and if $n$ is in $\mathbf{N}$, then $n+1$ is in $\mathbf{N}$.

You can see this is a recursive structure, where zero is base case, and other numbers can be reduced to base case.

In $\lambda$ calculus, it is very similar to define numbers.
Firstly we define zero as base case, then define the successor to zero is one, and in the same manner we can define all natural numbers.

Zero can be defined as:

$$ \lambda f. \lambda z. z $$

To make intuitive understanding, I will translate that into JavaScript code simultaneously:

var zero = function(f) {
    return function(z) {
        return z;
    };
};

But why we need to define zero like this?

Intuiviely, we can imagine $f$ in the first function as some operations we need to do (here is higher-order function, again), and the inner function takes a argument $z$, but not applied to $f$, that means $f$ do zero times to $z$.

Similarly, we can define $one$ as a combination of functions that do one times to $z$, that is:

$$ \lambda f. \lambda z. f(z) $$

And $two$ as:

$$ \lambda f. \lambda z. f(f(z)) $$

And $three$ as:

$$ \lambda f. \lambda z. f(f(f(z))) $$

And so on.

We can see that a number in Church Encoding is always a function that takes one argument and return a function also takes one argument, or simpliy say a curry function that takes two arguments.

But it’s unnecessary to define all natural numbers in this way, we can define a $successor$ function to generate these numbers:

$$ Succ = \lambda n. \lambda f. \lambda z. (n f) (f z) $$

So apply our $Succ$ to $zero$, we can obtain $one$ as:

$$ (\lambda n. \lambda f. \lambda z. (n f) (f z)) (\lambda f. \lambda z. z) = \lambda f. \lambda z. f(z) $$

and we can obtain $two$ by apply $Succ$ to $one$:

$$ (\lambda n. \lambda f. \lambda z. (n f) (f z)) (\lambda f. \lambda z. f(z)) $$

$$ = \lambda f. \lambda z ((\lambda z.fz) (f z)) $$

$$ = \lambda f. \lambda z. f(f(z)) $$

Since we have shown zero in JavaScript and other numbers are nearly the same, so now let’s see how to represent Succ in JavaScript:

var Succ = function(n) {
    return function(f) {
        return function(z) {
            return (n(f))(f(z));
        };
    };
};

Now you may ask, how to print a such Church Encoded number in JavaScript. Well, firstly we need an auxiliary function as argument $f$ which is what we want to do on these abstract numbers, that is to transform them into JavaScript primitive numbers by defining an inc function:

var inc = function(z) { return z + 1; };

Since we have already see that a Church encoded number takes two arguments, so secondly, we need an other argument that is an initial value, 0.

So, to print 0 we write as:

console.log(zero(inc)(0)); // 0

And to print 1, 2 and 3 we write:

console.log(Succ(zero)(inc)(0)); // => 1
console.log(Succ(Succ(zero))(inc)(0)); // => 2
console.log(Succ(Succ(Succ(zero)))(inc)(0)); // => 3

Arithmetic

After defined numbers, now we will deal with addition and multiplication operations.

In Church-Encoding, addition function is a curry function that takes four arguments $n$, $m$, $f$, and $z$, to add $n$ and $m$.

$$ \lambda n. \lambda m. \lambda f. \lambda z. (n f) ((m f) z) $$

In the body of this add function, it applies $n$ and $m$ with $f$ seperately, that express the meaning of $add$, then applies the result with $z$.

For example, we want to add 1 and 2:

$$ (\lambda n. \lambda m. \lambda f. \lambda z. (n f) ((m f) z)) (\lambda f. \lambda z. f(z)) (\lambda f. \lambda z. f(f(z))) $$

$$ = \lambda f. \lambda z. (\lambda z. f(z)) ((\lambda z. f(f(z))) z) $$

$$ = \lambda f. \lambda z. (\lambda z. f(z)) (f(f(z))) $$

$$ = \lambda f. \lambda z. f(f(f(z))) $$

After some substitutions, we get number three in Church-Encoding.

To multiply $n$ by $m$, we define multiplication function:

$$ \lambda n. \lambda m. \lambda f. \lambda z. (m (n f)) z $$

For example, 2 multiply 3 is:

$$ (\lambda n. \lambda m. \lambda f. \lambda z. (m (n f)) z) (\lambda f. \lambda z. f(f(z))) (\lambda f. \lambda z. f(f(f(z)))) $$

$$ = \lambda f. \lambda z. [(\lambda f. \lambda z. f(f(f(z)))) ((\lambda f. \lambda z. f(f(z))) f)] z $$

$$ = \lambda f. \lambda z. [(\lambda f. \lambda z. f(f(f(z)))) (\lambda z. f(f(z)))] z $$

$$ = \lambda f. \lambda z. [\lambda z. (\lambda z. f(f(z))) (\lambda z. f(f(z))) (\lambda z. f(f(z))) z] z $$

$$ = \lambda f. \lambda z. [\lambda z. (\lambda z. f(f(z))) (\lambda z. f(f(z))) f(f(z))] z $$

$$ = \lambda f. \lambda z. [\lambda z. (\lambda z. f(f(z))) f(f(f(f(z))))] z $$

$$ = \lambda f. \lambda z. [\lambda z. f(f(f(f(f(f(z))))))] z $$

$$ = \lambda f. \lambda z. f(f(f(f(f(f(z)))))) $$

Well, it looks complicating, let’s verify it in JavaScript:)

The definition of addition and multiplication is:

var add = function(n) {
    return function(m) {
        return function(f) {
            return function(z) {
                return (n(f))((m(f))(z));
            };
        };
    };
};

var mul = function(n) {
    return function(m) {
        return function(f) {
            return function(z) {
                return (m(n(f)))(z);
            };
        };
    };
};

and we use previously defined Succ function two generate some numbers, as well as inc function,

var one = Succ(zero);
var two = Succ(one);
var three = Succ(two);

Now, let’s play with it:

console.log(add(one)(two)(inc)(0)); // => 3

console.log(mul(two)(three)(inc)(0)); // => 6

Further Reading

In the Chapter 6 of The Little Schmer, the authors talk about Church Numbers in another way, and more easier to understand.