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 x. f 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 around 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.