Lambda calculus and Graham’s number

Very big numbers like Graham’s Number are often expressed with lengthy, clumsy, semi formal explanations. But it’s concise and convenient to express such numbers precisely in the pure lambda calculus, using Church numerals. Starting with Knuth’s up-arrow, if we define fn,a(b) = anb, then f0,a(b) = ab and fn+1,a(b) = fn,ab(1). From this we get that the lambda expression upify = λf b. b f 1 yields fn+1,a given fn,a, and so uparrow = λn a b. n upify (times a) b. A similar process yield’s Graham’s Number, given that G = f64(4) where f(n) = 3↑n3:

1 = λf xf x
2 = λf x. f (f x)
3 = λf x. f (f (f x))
4 = 2 2
64 = 3 4

times = λa b f. a (b f)
upify = λf b. b f 1
uparrow = λn a b. n upify (times a) b
grahamf = λn. uparrow n 3 3
graham = 64 grahamf 4

Putting it all together:

graham = (λc2 c3.(λc4. c3 c4 n. n f b. b f x. x)) (λb f. c3 (b f)) c3) c4) (c2 c2)) (λf x. f (f x)) (λf x. f (f (f x)))

In John Tromp’s “binary lambda calculus”, this expression takes up  120 bits—exactly as many bits, as Doug Clow points out below, as the string “Graham’s Number” in Unicode. Don’t try evaluating this in your favourite lambda calculus interpreter unless you’re very, very patient.

Updated 2020-02-20:  I blogged about a beautiful way to see this as a picture.

Welcome to my new blog!

When I first went to set up a blog, I wanted something I had the option of hacking on myself, based on a decent programming language and decent toolkit.  Being a Pythonista, I looked for something Django based, and settled on Byteflow. I set it up and started blogging.

This turns out to have been very much the wrong choice. There’s been one commit against Byteflow since September 2011, I’ve had trouble every time I’ve needed to upgrade, and I was overrun with spam until the last upgrade when comments broke. So this time I’m going the other way—choosing the awful, PHP-based WordPress, which is also by far the most popular platform for blogging in the world, and hosting it on instead of trying to host it myself, which should mean it stays up to date with security and anti-spam measures.

Let’s hope this leads to better and more productive conversations. Thanks for joining me!