### 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 *f _{n,a}*(

*b*) =

*a*↑

^{n}

*b*, then

*f*(

_{0,a}*b*) =

*ab*and

*f*(

_{n+1,a}*b*) =

*f*

_{n,a}^{b}(1). From this we get that the lambda expression

**upify**= λ

*f b*.

*b f*

**1**yields

*f*given

_{n+1,a}*f*, and so

_{n,a}**uparrow**= λ

*n a b*.

*n*

**upify**(

**times**

*a*)

*b.*A similar process yield’s Graham’s Number, given that

*G = f*(4) where

^{64}*f*(

*n*) = 3↑

^{n}3:

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