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.

Published by Paul Crowley

I'm Paul Crowley aka "ciphergoth", a cryptographer and programmer living in Mountain View, California. See also my Twitter feed, my webpages, my blogs on Dreamwidth and Livejournal, and my previous proper blog. Or mail me: paul at ciphergoth.org.

8 thoughts on “Lambda calculus and Graham’s number

  1. These representations are small … but the ones out there are far away. Small (120 bits) … and far away (Graham’s number).

    Whenever I think about really big numbers like this, after I’ve finished boggling at just how eye-wateringly, incomprehensibly vast they are (and Graham’s number is a doozy), I have a shorter boggle at how amazing it is that we can express one in such a concise form. Then I have a boggle that doesn’t really go away quickly about just how many numbers there are that we can’t specify individually in any short form. I mean, I know in theory that there are countably-infinitely many integers, but because that has ‘countable’ in it, I tend to lazily think of counting for a long time, and because I have even less facility with thinking about absurdly long lengths of time than I do with thinking about large numbers, it doesn’t seem so huge. ‘Graham’s number’ concisely specifies one really-pretty-big number. I can even specify things like “Graham’s number minus four’, which I know ends ‘…95383.’ But the number of numbers that can be picked out like that are a really pretty tiny proportion of the numbers. Like, really very small. In fact, I’m fairly convinced that there are, in fact, countably-infinitely more integers than you can specify individually using a finite representation.

    And that is actually quite a lot.

    1. Well, every integer can be individually specified using a finite representation :) but a countably infinite majority of integers have no finite representation shorter than their binary representation, by a counting argument.

      1. Doh! Of course. You’ve put what I was trying to say in to an coherent form.

        It’s so hard to wrap one’s mind around the difference between ‘really, really big … like absolutely ginormous … only bigger than that’ and ‘infinite’. It is a big difference.

  2. The other thing I always think of is how much context one has to assume for a representation to convey a particular number. Ordinary Arabic numerals are perhaps the simplest – I can write, say, “65536” and be confident that almost any numerate person will understand me to mean the number I meant to specify. Scientific notation and exponentials are less widely understood. Knuth’s up-arrow notation even less so. And lambda calculus probably still less so.

    I think “Graham’s number” probably conveys the number in question at least as precisely as your lambda calculus expression, and to a wider audience than the binary lambda calculus representation.

    Hilariously undermining the argument I was trying to make here, though, the string “Graham’s number” has 15 characters, which at a parsimonious 8 bytes a pop gives us … 120 bits.

  3. My Binary Lambda Calculus page moved to https://tromp.github.io/cl/cl.html

    The (alternative) diagram for the above graham is

    ___________________________________________________________________ ___________
    _____|___|___________________________________|___|_ _______________ _|___|_____
    | |___| _________________|___________|_ |___| _|___|___|_____ | |___|
    |___| | ___________ _|_________ | | | | |___| |___|
    | | _____|_____ _|___|_____ | | | |___| |
    | | |___| ___ | |___| | | |___| |
    | | | ___ |___| | | | |
    | | |___| | | | | |
    | |_______| | | | | |
    | |_______| | | | |
    | |___________| | | |
    |_______________________| | | |
    |_______________| | |
    |_______| |
    |_______________|

    1. I have tried editing your comment but I can’t get WordPress to display it properly, so I’ve pasted your diagram into the original post!

      EDIT now moved it into a post of its own.

Leave a Reply to dougclow Cancel reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s