One of the first posts I made on this blog was Lambda calculus and Graham’s number, which set out how to express the insanely large number known as Graham’s Number precisely and concisely using lambda calculus.

A week ago, Reddit user u/KtoProd asked: if I wanted to get a Graham’s Number tattoo, how should I represent it? u/FavoriteColorFlavor linked to my lambda calculus post. But in a cool twist, they suggested that rather than writing these things in the usual way, they use a John Tromp lambda calculus diagram. I got into the discussion and started working with the diagrams a bit, and they really are a great way to work with lambda calculus expressions; it was a pleasure to understand how the diagram relates to what I originally wrote, and manipulate it a bit for clarity.

The bars at the top are lambdas, the joining horizontal lines are applications, and the vertical lines are variables. There are three groups; the rightmost group represents the number 2, and the middle one the number 3; with beta reduction the two lambdas in the leftmost group will consume these rightmost groups and use them to build other small numbers needed here, like 4 (2^{2}) and 64 (4^{3}). The three is also used to make the two 3s either side of the arrows. Tromp’s page about these diagrams has lots of examples.

I’m obviously biased, but this is my favourite of the suggestions in that discussion. If u/KtoProd does get it as a tattoo I hope I can share a picture with you all!

Update 2020-02-24: I’ve added the ability to generate these diagrams to my Python lambda calculus toy. After installation, try `./trylambda demofiles/draw.olc`

.

##
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.
View more posts

This is pretty, but I’m finding it hard to understand how the diagram corresponds to the expression. It looks like a vertical line changes in what it signifies every time it intersects with an application line? So, e.g., the expression for 2 (https://tromp.github.io/img/cl/2.gif, λf.λx.f(f x)), the leftmost vertical line represents f at the top but the result of the whole expression at the bottom? I’m really not sure.

Yes that’s right, the line changes what it signifies with each application line, to represent the new combined expression.

If the number is so large it’s impossible to evaluate or write down even an approximation, isn’t the expression kind of dead?