## Church Numerals in Clojure

Church Numerals are a way of encoding natural numbers using lambda expressions. A number `n`

is represented by a function that composes another function `f`

around its argument `x`

, `n`

times. So:

```
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
...
```

These can be implemented very easily in Lisps and other languages with first-class functions. In Clojure, this would be:

```
0 ≡ (fn [f] (fn [x] x))
1 ≡ (fn [f] (fn [x] (f x)))
2 ≡ (fn [f] (fn [x] (f (f x))))
...
```

The insane thing is that you can do arithmetic on these things using nothing but more anonymous functions. It's lambdas all the way down.

Once you understand this, your brain will explode, and hopefully little bits of it will land next to the remnants of my own brain to keep it company.

So based on the Wikipedia article, here are some functions that convert numbers to and from Church encoding, and then some functions to do basic arithmetic on Church numerals. I understand this down to `exp`

(via lots of pencil and paper expansions) but I gave up understanding at `pred`

.

```
(defn church
"Convert a natural number to a Church numeral."
[n]
(loop [n n, acc (fn [f] (fn [x] x))]
(if (zero? n)
acc
(recur (dec n)
(fn [f]
(fn [x]
(f ((acc f) x))))))))
(defn unchurch
"Convert a Church numeral to a plain integer."
[n]
((n inc) 0))
(def plus
(fn [m]
(fn [n]
(fn [f]
(fn [x]
((m f) ((n f) x)))))))
(def mult
(fn [m]
(fn [n]
(fn [f]
(n (m f))))))
(def exp
(fn [m]
(fn [n]
(n m))))
(defn pred [n]
(fn [f]
(fn [x]
(((n (fn [g]
(fn [h]
(h (g f)))))
(fn [u] x))
(fn [u] u)))))
(def sub
(fn [m]
(fn [n]
((n pred) m))))
(def is-zero?
(fn [n]
((n (fn [x] 'FALSE)) 'TRUE)))
```

And this somehow actually works:

```
user> (unchurch (fn [f] (fn [x] (f (f (f (f (f (f (f x))))))))))
7
user> (unchurch (church 7))
7
user> (unchurch ((plus (church 2)) (church 3)))
5
user> (unchurch ((mult (church 2)) (church 3)))
6
user> (unchurch ((exp (church 2)) (church 3)))
8
user> (unchurch ((sub (church 7)) (church 3)))
4
user> (is-zero? (church 0))
TRUE
user> (is-zero? (church 7))
FALSE
```

This is the kind of thing I wish I'd studied more in college. I covered some cool stuff, some small amount of theory of computation and whatnot, but not nearly enough of this. Not enough functional programming, not enough Lispy goodness.

A lot of people say all programmers should learn assembler language so you understand what's happening at a low level. But shouldn't it be just as important to learn lambda calculus? It's another kind of low level, a very important one at that.

## 13 Comments

My God, its full of stars!

Seriously thos, this functional code thing might be cool for some of you, but I dont understand a word of it and I dont want to.

If this is the kind of stuff we can expect to see in Clojure and all thems fancy new languages and lambda languages, I say to hell with it. I prefer the old way.

you don't wanna know bout the ycombinator.

Hah, "The old way." Lisp is the oldest still commonly used programming language, and the original functional language. It's also fun in ways that imperative languages are not.

I've always thought that you should learn assembler to understand how the hardware wants to work, and you should learn Lisp (or any functional language) to learn how the software wants to work. It's just such an elegant design, that it just seems right.

This book goes through much the same exercise that you did, by building up the integers with nested functions. It also covers many other interesting topic in computation. It's a good read, that will take many reads to finish.

I dont think that it is really necessary to know Assembler anymore, at least no "real" assembler, because x86 is meanwhile really a mess of things you probably never need directly.

Anyway, it is also possible (and quite a challenge) to generate church numbers with x86 assembly - I did this, posted about it (put the link into the Homepage-URL of this answer for anybody interested).

But actually, Church Numbers are of no real practical interest, as far as I know, and even in tcs, they are not really used for anything, because you will already get problems when using the typed lambda calculus - which is what, afaik, vitally all current research is about, because it has a lot of applications in formal program verification.

@gammer: Formal Program Verification is btw a reason for functional programming, it is much uglier to verify imperative code. And I think program verification is the future. Software gets more complicated, and bugfixing gets more expensive. So there will be a necessity for parts of the software one can rely on - which can only be achieved by formal program verification.

Btw: It would be great if this blog had some possibility to subscribe to comments, either via RSS or via E-Mail-Notifications.

I have one question and one question only about this.

Where would it be of use? I don't care how obscure a program, I'm just interested to know where it'd be of use.

@Teifion It's useful academically. Lambda calculus was used to solve some of the most important questions in computer science.

Playing with these kinds of problems is also useful as mental exercise to get you thinking in terms of first-class anonymous functions, recursion etc. Those things are used in real programs in lots of ways.

Church numerals are not so useful practically, as far as I know.

For those asking for practical reasons to bother with such things, I'd say the church numerals allow one to realize what's absolutely required in a programming language versus what is merely an implementation detail. Consider another example from Lisp. Let's say we have a baby lisp that has lambdas and we want to build cons cells and lists. How can we do such a thing? SICP shows one way to do this.

(def cons [a b] (fn [x] (if x a b)))

(def car [c] (c true))

(def cdr [c] (c nil))

We can make the lists out of lambdas. This shows that one can get cons cells and lists "for free" in a language that only has lambdas. Similarly, one can get numerals in such a language. Now, in any serious implementation of a language, you might never do such a thing because it wouldn't be efficient, but the power is there, and I think that's an important realization for any computer scientist. With lambdas, we can build lists, numbers, trees, and objects--that's a pretty incredible building material.

Well, I guess you and I have different definitions of 'commonly'.

And technically Fortran is a bit older (and likely more used).

if you like this, you might enjoy some more mainstream analytical philosophy. Frege and Wittgenstein, in particular, offer similar brain destroying insight into the foundations of math and language.

Learn TDD to understand what the software want to do. If it doesn't do the right thing, nothing else matters.

The power of Lambda Calculus is in the number of concepts involved in writing programs. And the number is very small. Thus it is viable to reason about program correctness, instead of doing TDD, which will never prove your program is correct. Go check out http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1305.html for more on this.

And, as Mr. Dijkstra has pointed out, paraphrased: testing can only reveal the presence of bugs, not their absence.

Thomas inadvertently points out the main drawback to test-driven development. In the (very wide) realm of possible cases where the software

doesdo the right thing, what then? What about architecture, future expansion, modularity, code reuse... TDD doesn't help at all here. All it is useful for is sanity checking. Important, but not the be-all-end-all he makes it out to be.SICP offers a better example of functions as structures than the one extracted by Shane. IIRC, a footnote on the same page goes like this:

No ifs or related machinery, just as in Church numerals.