This is a read-only archive!

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.

September 15, 2009 @ 7:14 PM PDT
Cateogory: Programming

13 Comments

gammer
Quoth gammer on September 16, 2009 @ 7:16 AM PDT

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.

aa
Quoth aa on September 16, 2009 @ 8:03 AM PDT

you don't wanna know bout the ycombinator.

wkw3
Quoth wkw3 on September 16, 2009 @ 8:11 AM PDT

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.

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.

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?

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.

Christoph
Quoth Christoph on September 16, 2009 @ 10:11 AM PDT

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.

Teifion
Quoth Teifion on September 16, 2009 @ 10:38 AM PDT

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.

Brian
Quoth Brian on September 16, 2009 @ 10:53 AM PDT

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

Shane
Quoth Shane on September 16, 2009 @ 11:42 AM PDT

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.

Nick
Quoth Nick on September 16, 2009 @ 12:09 PM PDT

Hah, "The old way." Lisp is the oldest still commonly used programming language, and the original functional language.

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

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

ashika
Quoth ashika on September 16, 2009 @ 12:57 PM PDT

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.

Thomas Eyde
Quoth Thomas Eyde on September 16, 2009 @ 4:21 PM PDT

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

jdz
Quoth jdz on September 16, 2009 @ 6:11 PM PDT

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.

Steve
Quoth Steve on September 17, 2009 @ 11:50 AM PDT

Thomas inadvertently points out the main drawback to test-driven development. In the (very wide) realm of possible cases where the software does do 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.

jeffen
Quoth jeffen on September 17, 2009 @ 8:23 PM PDT

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:

(define (xcons a b) (lambda (select) (select a b)))
(define (xcar x) (x (lambda (a b) a)))
(define (xcdr x) (x (lambda (a b) b)))

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