Church Numerals in Clojure

Wed, 16 Sep 2009 02:14:30 -0700

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.

briancarper.net (λ) (Tag: Lambda Calculus)

Church Numerals in Clojure