Tromp Diagrams

What is the λ-calculus?

The λ-calculus is a tiny formal language invented by Alonzo Church in the 1930s. It has only three building blocks:

• variables — names like x, y, f
• abstraction — λx. M, an anonymous function taking x and returning M
• application — M N, applying function M to argument N

From these three primitives, plus a single computation rule (β-reduction: replace (λx. M) N by M with N substituted for x), you can build everything: numbers, booleans, pairs, recursion, the whole of computation. The λ-calculus is Turing-complete with one rule and one syntactic form.

Tromp diagrams

John Tromp introduced a remarkable graphical notation that turns abstract λ-terms into something you can look at. Lambdas become horizontal bars; applications become connecting bars; variables are vertical wires plugging into their binder.

The result is that every λ-term has a unique geometric shape — and β-reduction becomes a kind of physical rearrangement of these shapes. The visualizer on this site animates that rearrangement step by step.

A few classic shapes

Each λ-term has its own geometric signature. Click any of these to open it in the visualizer.

Quick taste

Some things to try in the visualizer:

• plus 2 3 — Church addition reduces to 5
• Y — the fixed-point combinator, with its iconic self-replicating shape
• omega — (λx. x x) (λx. x x), an infinite loop
• fst (pair a b) — pairs and projections
• Switch reduction strategies to see how β-reduction order changes things