Church Encoding in Python
If we define true and false with the following combinators (in Python):
TRUE = lambda a: lambda b: (a) FALSE = lambda a: lambda b: (b)
then if-then-else can be implemented simply by applying a predicate to two arguments: the then/true case and the else/false case.
For example:
(TRUE)(True)(False) == True (FALSE)(True)(False) == False
Now if we define:
AND = lambda a: lambda b: (a)(b)(a) OR = lambda a: lambda b: (a)(a)(b) NOT = lambda a: lambda b: lambda c: (a)(c)(b)
we can do boolean logic with only reference to function application.
For example:
(AND)(TRUE)(FALSE) == (FALSE)
This is a little hard to verify in Python so we can use our if-then-else trick:
(AND)(TRUE)(FALSE)(True)(False) == False
Our definition of TRUE and FALSE is known as the Church encoding of the booleans.
We can also Church-encode a pair, or cons, and define car and cdr appropriately:
CONS = lambda a: lambda b: lambda c: (c)(a)(b) CAR = lambda a: (a)(TRUE) CDR = lambda a: (a)(FALSE)
If the definitions of CAR and CDR seem odd, note that the magic is really in CONS.
(CAR)((CONS)(1)(2)) == 1 (CDR)((CONS)(1)(2)) == 2
But this means CONS makes a nice way of deferring our (True)(False) trick to "unchurch" Church-encoded booleans into Python booleans:
UNCHURCH_BOOLEAN = (CONS)(True)(False)
Now we can say:
(UNCHURCH_BOOLEAN)((NOT)(TRUE)) == False (UNCHURCH_BOOLEAN)((OR)(TRUE)(FALSE)) == True
The natural numbers can also be Church-encoded:
ZERO = FALSE SUCC = lambda a: lambda b: lambda c: (b)((a)(b)(c))
We can then define:
ONE = (SUCC)(ZERO) TWO = (SUCC)(ONE) THREE = (SUCC)(TWO) FOUR = (SUCC)(THREE)
and so on. Here's a little Python function for "churching" numbers:
def church_number(n): return SUCC(church_number(n - 1)) if n else FALSE
We can define addition, multiplication and exponentiation as follows:
PLUS = lambda a: lambda b: lambda c: lambda d: (a)(c)((b)(c)(d)) MULT = lambda a: lambda b: lambda c: (b)((a)(c)) EXP = lambda a: lambda b: (b)(a)
Of course, what would be nice is if we had an easy way to unchurch our Church-encoded numbers so we could see if these work. Well, it turns out that's easy to do:
UNCHURCH_NUMBER = lambda a: (a)(lambda b: b + 1)(0)
So
(UNCHURCH_NUMBER)(ZERO) == 0 (UNCHURCH_NUMBER)(ONE) == 1 (UNCHURCH_NUMBER)(TWO) == 2
and so on.
(UNCHURCH_NUMBER)((PLUS)(THREE)(TWO)) == 5 (UNCHURCH_NUMBER)((MULT)(THREE)(TWO)) == 6 (UNCHURCH_NUMBER)((EXP)(THREE)(TWO)) == 9
Comments (14)
James Tauber on Nov. 26, 2008:
Dave, I take that as a compliment.
Bill Mill on Nov. 26, 2008:
You're missing a paren in "(FALSE)(True(False) == False"
James Tauber on Nov. 26, 2008:
Thanks Bill -- fixed.
Steve on Nov. 26, 2008:
I think you also forgot a return for church_number.
James Tauber on Nov. 26, 2008:
I could say I added these errors deliberately to keep people on their toes but I'd be lying. Thanks Steve.
Marty Alchin on Nov. 26, 2008:
I really wish somebody would explain why this kind of stuff is important. I'm not doubting that it is important for certain applications, but I have no idea what those applications are, much less whether I'll ever run into them.
Regardless, I'll definitely keep this stuff in mind if I ever enter an obfuscated Python contest. :)
James Tauber on Nov. 26, 2008:
If you're content with the engineering or craft side of things, Marty, this sort of stuff probably isn't important. But if you're interested in computational theory, the mathematical foundations of computing, the computational foundations of mathematics or just what these guys Turing, Gödel, Curry and Church got up to all those years ago, this stuff is pretty core.
James Tauber on Nov. 26, 2008:
Plus, for some people, there's a certain beauty in seeing how arithmetic and boolean logic (and, in fact, all that is computable) can be built out of the single fundamental notion of applying functions, not to other objects but simply applying functions to other functions.
Eric Florenzano on Nov. 26, 2008:
Awww man I was going to post basically this exact same thing...you beat me to it. Good writeup, though! I like how you use "church" as a verb. There needs to be much more churching in this world, if you ask me :)
James Tauber on Nov. 26, 2008:
Well, Eric, I was fully expecting you to post something like this but then you said you didn't have anything to post so I figured you weren't going to.
It was a fun post to do — it was only during researching it that I worked out how to write the church and unchurch number functions and realised the role that cons could play in unchurching booleans.
Julien Oster on Nov. 26, 2008:
Let's add a Y combinator for strict languages, shall we? This gives us recursive functions without them having to reference themselves by name:
Y_ = lambda x: lambda f: lambda n: f(x(x)(f))(n)
Y = Y_(Y_)
Don't forget ISZERO, to check if a church number is zero:
ISZERO = lambda n: n(lambda x: FALSE)(TRUE)
and you have SUCC, giving the next number, but let's add PRED, giving the previous one (it's a little more complicated than SUCC):
PRED = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f))) (lambda u: x) (lambda u: u)
Put it all together and you can write a faculty function:
facf = lambda q: lambda n: (ISZERO(n)(lambda x: ONE)(lambda m: MULT(n)(q(m)))(PRED(n)))
fac_ = Y(facf)
... let's replace all functions by their definition:
fac = (lambda x: lambda f: lambda n: f(x(x)(f))(n))(lambda x: lambda f: lambda n: f(x(x)(f))(n))(lambda q: lambda n: ((lambda n: n(lambda x: lambda x: lambda y: y)(lambda x: lambda y: x))(n)(lambda x: lambda f: lambda x: f(x))(lambda m: (lambda m: lambda n: lambda f: m(n(f)))(n)(q(m)))((lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f))) (lambda u: x) (lambda u: u))(n))))
... followed by some eta reduction to make it shorter and renaming the bound variables just for the hell of it:
fac = ((lambda p: p(p)(lambda q: lambda n: ((n(lambda e: lambda e:
lambda a: a)(lambda i: lambda l: i))(lambda d: lambda c: lambda d: c(d))
(lambda m: (lambda m: lambda z: m(n(z)))(q(m)))((lambda c: lambda x:
n(lambda g: lambda h: h(g(c)))(lambda u: x)(lambda u: u))))))
(lambda s: lambda q: lambda w: q(s(s)(q))(w)))
That's it. A fully working faculty function consisting entirely of just single-argumented lambdas and single-argumented calls to their bound variables.
James Tauber on Nov. 26, 2008:
Awesome Julien!
Ertugrul Söylemez on Feb. 8, 2009:
It's interesting to see that I'm not the only one, who abuses Python for functional programming. =)
However, you left away something very important: Church lists: <http://blog.ertes.de/2009/01/reinterpretation-of-python-lists.html>. ;)
Last Modified: Nov. 26, 2008
Author: James Tauber
Dave K on Nov. 26, 2008:
This officially makes you the nerdiest feed I read.