Lattice

A little visual lambda calculus you can draw. A program is a wired-up diagram of just two operations — λ (make a function) and @ (apply one) — plus variables and wires. Point the ► output at the top of your program, hit Run, and watch it reduce: the active step tints as substitution flows through the diagram.

Inspired by Lingdong Huang’s λ-2D. Pick a preset to see a finished program, or draw your own.

Reading the output

While a program runs, the canvas redraws the current term at each step and the status line underneath tells you where you are:

• step N — how many reductions have happened so far.
• (fn arg) / λ. / • — a compact text form of the current term. Every variable shows as •, each function as λ., and each application as a parenthesised (function argument) pair. It’s the same tree you see drawn above, written on one line.
• the tints — the yellow cells are the redex: the λ and @ about to fire, i.e. the function that’s being called. The blue cells are its argument — the piece that’s about to be copied into the function’s body. Watching yellow consume blue is watching one substitution happen.
• ⇒ = 2 — when the term can’t reduce any further and its shape is a Church numeral or boolean, it’s decoded for you (= 2, = true, = false).
• ⇒ normal form — finished, but the result isn’t a number or boolean (like a bare function).
• · free vars — the term mentions a variable no enclosing λ binds. That’s legal here; it just means the result depends on an unknown input.
• cap reached — 500 steps elapsed without finishing. Reduction is normal-order, so if a term can terminate it will, but some never do — draw Ω, (λx.x x)(λx.x x), to watch one loop forever.

The presets

Load any of these from the presets… menu, then press Run:

• identity — λx.x, the function that hands back whatever it’s given. Already in normal form (0 steps): a look at what a lone function is.
• apply-id — (λx.x)(λy.y), identity applied to identity. One reduction and it collapses to λy.y. The gentlest thing to watch reduce.
• K — λx.λy.x, the constant combinator: a two-argument function that ignores its second argument and returns its first. Normal form as drawn.
• church-2 — λf.λx. f (f x), the number 2 encoded as a function that applies f twice. Already normal form; decodes to = 2. Every Church numeral is “do this n times”.
• succ-1 — succ 1: the successor function applied to the Church numeral 1. This one actually computes — it reduces over a few steps and lands on Church 2, decoding = 2.