Lambda Diagrams

A few days ago, partly inspired by Dave Keenan's To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction, I discovered an interesting way to denote lambda terms.

Lambda Diagrams are a graphical notation for closed lambda terms, in which abstractions (lambdas) are represented by horizontal lines, variables by vertical lines emanating down from their binding lambda, and applications by horizontal links connecting the leftmost variables and extending the leftmost one down. In the alternative style, the final extension is omitted, and applications link the nearest deepest variables, for a more stylistic, if less uniform, look.

The following table shows diagrams of identity, the booleans, the standard combinators, some Church numerals, and Omega.

term	definition	diagram	alternative
I	λx.x
K/true	λx.λy.x
false	λx.λy.y
S	λx.λy.λz.(x z)(y z)
Y	λf.(λx.x x)(λx.f(x x))
2	λf.λx.f(f x)
3	λf.λx.f(f(f x))
4	λf.λx.f(f(f(f x)))
Ω	(λx.x x)(λx.x x)

Curiously, the alternative Omega diagram somewhat resembles an (upside-down) Omega.

As an example of a significantly more complex term, here (in alternative style) is the prime number sieve from John's Lambda Calculus and Combinatory Logic Playground:

which reduces to an infinite list of booleans that starts out as

In terms of pixels, a diagram's width is one less than 4 times the number of variables (vertical lines), and its height is one more than twice the maximum number of nested abstractions and applications (one less for alternaitve diagrams with multiple variables).

The size of the binary encoding of a term is closely related to the graphical complexity: it is exactly twice the number of lines plus the number of (4-way) intersections.

Open terms could be partially represented by letting free variables stick out on top, but their identity would be lost.