Böhm Trees, Separability, and What Normal Forms Cannot Distinguish

Two terms are beta-eta equivalent when a chain of reductions and expansions connects them. That relation is finer than the equality a programmer cares about. λx. x and λx. (λy. y) x are beta-eta equivalent, and so are any two terms that differ by a reducible step, but many pairs of terms that behave identically on every argument are not connected by any such chain. The gap between the two is the subject of the deepest part of the untyped theory, and closing it requires a notion of value that is coinductive rather than inductive.

The central object is the Böhm tree. It is an infinite tree extracted from a term by reducing it as far as possible, recording at each node which head variable the term exposes and what its arguments are, and repeating on the arguments. Two terms are equivalent when their trees are equal. For terms with normal forms the trees are finite and the equivalence coincides with beta-eta convertibility. For terms without normal forms the trees are either infinite, when the term exposes structure at every finite depth, or ⊥, when it exposes nothing at all, and in that case the equivalence is strictly coarser than beta-eta convertibility.

The tree, constructed

Take a term in beta normal form. Its Böhm tree is itself: a lambda prefix, then a head variable applied to arguments, then the trees of the arguments. For λx. λy. x y, the tree is a node labelled x with one child, the tree of y.

For a term with no normal form, the construction is a limit. Reduce the term to weak head normal form — a lambda prefix followed by a head variable applied to arguments, if such a form exists — record the prefix and the head, and recurse on the arguments. If at some point a subterm has no weak head normal form, the recursion stops there and the node is ⊥, the undefined tree.

BT(λx. M)      = λx. BT(M)
BT(x M₁ … M_k) = x (BT(M₁)) … (BT(M_k))
BT(M)          = ⊥    if M has no weak head normal form

Three examples fix the idea.

Ω = (λx. x x)(λx. x x) reduces to itself and never exposes a head variable. Its tree is ⊥, the single node with no information. Y = λf. (λx. f (x x))(λx. f (x x)) reduces inside its body to λf. f ((λx. f (x x))(λx. f (x x))), whose weak head form exposes f applied to a term that unfolds the same way; recursing gives λf. f (f (f (…))), an infinite chain of f applications. And Y I, where I = λx. x, reduces to I (Y I) and then back to Y I, so its tree is ⊥ even though the term is not syntactically Ω.

The tree is coinductive: it is defined as the greatest fixed point of the unfolding, not the least. A term has a finite tree exactly when it has a normal form; a term with an infinite tree is a term whose reduction never terminates but which nevertheless exposes structure at every finite depth. The distinction between ⊥ and an infinite tree is the distinction between “no information at any depth” and “information at every finite depth but no finite bound”, and it is the distinction that reduction-based equivalences cannot make.

Why beta-eta is too fine

Consider two terms that a program cannot tell apart: λx. x and λx. (λy. y) x. They are beta-eta equivalent, and their trees are equal. Now consider λx. x (λy. y) and λx. x (λy. (λz. z) y). Also equivalent, also equal trees. So far the tree does not add anything.

The interesting cases are the ones where the trees agree but no reduction connects the terms. Reduction is preserved by the tree construction, so β-convertible terms have equal trees; the converse fails. The clearest witnesses come from the unsolvable end of the spectrum. Ω = (λx. x x)(λx. x x) reduces only to itself, and Y I returns to itself in two steps, where Y is Curry’s fixed-point combinator and I is the identity: Y I → I (Y I) → Y I. Their trees are both ⊥, and they are not β-convertible: Ω reduces to nothing but itself, while Y I reduces only to itself and to I (Y I), so their reducts never meet. Observational equivalence also cannot separate them, since a context that contains either one diverges.

The other source of gaps is the infinite trees. A term that unfolds forever while exposing a head at every finite depth has an infinite tree, and two such terms can have equal trees without being related by any finite sequence of reductions. This is the part of the theory where the coinductive definition earns its place: the equality is a greatest fixed point, so it can identify terms that no inductive reduction argument reaches.

The genuine gap is between terms that are observationally equivalent but not beta-eta equivalent. Observational equivalence is defined by the contexts that can distinguish them: M ≡ N when for every context C[·], C[M] has a normal form if and only if C[N] does. This is the equality a programmer means: two programs are the same when no test can tell them apart. It is coarser than beta-eta equivalence, because a context can only apply a term to arguments and observe whether the result terminates; it cannot inspect the term’s internal reduction history. For terms with normal forms the two notions coincide, and that coincidence is Böhm’s separability theorem rather than a definition.

Böhm’s theorem has two halves, and they answer different questions. The separability half says that two distinct normal forms can always be distinguished by a context: there are arguments and a surrounding term that make one reduce to a fixed constant and the other to a different one. The tree half says that for terms that are solvable — terms that expose a head variable after enough arguments — two terms are observationally equivalent exactly when their Böhm trees are equal, and that this equality coincides with convertibility in the theory obtained from beta-eta by additionally identifying all unsolvable terms with one another. Ω is not solvable, because no number of arguments makes it expose a head. Y is solvable, because Y f exposes f. Identifying the unsolvable terms is what removes the mismatch that Ω and λx. Ω create.

Separability

The theorem that gives the technique its name is a construction. Two distinct normal forms can always be separated: there is a context that maps one to a term with a normal form and the other to a term with none, or maps them to distinct normal forms. The proof builds the context out of the structure of the trees.

Böhm’s original argument uses a discriminator: given two distinct normal forms M and N, construct a sequence of arguments and a context such that applying it to M yields one Church numeral and applying it to N yields another. The construction is by induction on the point where the trees differ, and it relies on the fact that a head variable can be forced to take a specific argument by supplying an argument that selects it.

The consequence is that beta-eta equivalence is maximal among the congruences that keep distinct normal forms distinct: any congruence that identifies two distinct normal forms identifies everything, and the calculus collapses to a single equivalence class. In the terminology of the field, the equational theory of beta-eta equivalence is Hilbert–Post complete.

Separability fails exactly for the unsolvable terms, and the failure has a clean characterisation: a term is unsolvable precisely when no context separates it from Ω. Y I and Ω are the standard pair. Neither has a head normal form, so any context that contains one of them and tries to reduce it diverges, and no pair of arguments can make either expose a head. They are not beta-convertible, yet their Böhm trees are both ⊥. So tree equality is strictly coarser than beta-eta convertibility, and the difference is concentrated on the terms that never expose a head. The theory that matches the trees is beta-eta plus the axiom identifying every unsolvable term with Ω; in that theory the tree is a complete invariant, which is the content of the tree theorem.

What the tree computes

Böhm trees are not merely a technical device for a theorem. They are a semantics, and the semantics is the one that makes the untyped calculus a language of partial functions.

A term denotes a tree, and application is an operation on trees: applying a tree to an argument substitutes the argument’s tree for the head variable and continues. The operation is continuous with respect to the information ordering, where ⊥ is the least element and a tree with more structure is greater. Continuity is what makes the fixed-point construction work: Y is a fixed-point operator on the tree domain, and Y f is the least fixed point of the operation t ↦ f t, which is exactly the infinite unfolding when f is a lambda that uses its argument.

That is the sense in which the tree is the value of the term. Two terms with the same tree denote the same partial function, and the tree records the function’s behaviour at every finite amount of information. A term whose tree is ⊥ denotes the everywhere-undefined function; a term whose tree is an infinite chain denotes a function defined at every finite depth but not by any finite term.

The cost of this semantics is that it is not the semantics of beta reduction. Reduction is an operational relation on terms, and the tree is a denotation that quotients by observational equivalence, and it is strictly coarser than beta-eta convertibility on the unsolvable terms, where it identifies terms that no finite chain of reductions relates. Implementations live in the operational world, so they observe the finer distinction: a compiler that rewrites Y I to Ω performs a transformation the tree semantics justifies and that no beta-eta step licenses.

The limits, and why they matter

Three limits define the boundary of the theory.

Undecidability. Tree equality is not decidable. The trees are infinite, and comparing two of them requires deciding equality of infinite objects, which reduces to the halting problem for the terms that generate them. The theory gives a characterisation of observational equivalence, not an algorithm for it. Practical tools approximate: a type checker compares normal forms when it can compute them, and rejects or loops when it cannot.

The unsolvable terms. The tree semantics equates all terms that never expose a head, so Ω and Y I denote the same object while no reduction relates them. That identification is a modelling choice: it is what makes the semantics match the observational behaviour of the calculus, and it is what a proof about reduction must undo if it wants to distinguish the two terms. The two views are not interchangeable, and theorems proved about one do not transfer to the other without a lemma connecting them.

The limits of axiomatisation. The theory of beta-eta convertibility is recursively enumerable: enumerate derivations and the conversion M = N will eventually be found when it holds. Observational equivalence on the full untyped calculus is not recursively enumerable, so no effective axiom system generates it, finite or otherwise. That is a stronger statement than undecidability of the equality problem, and it is what makes the tree semantics necessary: the semantics characterises the equivalence in a way that no proof system can enumerate. Typed calculi escape because strong normalisation makes every well-typed term have a finite tree, at which point convertibility and observational equivalence coincide and become decidable.

The practical consequence for anyone building on the calculus is that “two terms are equal” has at least three meanings, and they are not interchangeable. Beta-eta convertibility is the finest: it relates two terms only when a chain of reductions and expansions connects them, and it is decidable on normalising fragments. Böhm tree equality is coarser, because it also identifies all unsolvable terms, and it is the equality that matches the observational behaviour of terms that have an infinite tree. Observational equivalence, understood as indistinguishability by all contexts, is the semantic notion that the tree is designed to capture, and it is undecidable in general. The reduction machinery of the abstract machines computes the first, the fixed-point construction of the recursion combinators generates the infinite trees that make the second and third diverge from it, and the translation of bracket abstraction is the tool that lets a tree be built from a variable-free term. Each of those mechanisms is a different answer to the same question: what does a term mean when it does not reduce to anything.