The Clock

birds, and the fondness relation  In Raymond Smullyan's To Mock a Mockingbird the combinators live as birds in a forest. To call A to B — to apply one to the other — is to call out the name B to the bird A, which answers with the name of some bird AB. A bird A is said to be fond of a bird x when calling x to it returns x itself: A x = x. In this dialect the Fixed-Point Theorem reads as a fact of natural history — every bird is fond of at least one bird — and a fixed-point combinator is a Sage bird (Smullyan writes Θ): a single bird that, called to any bird x, names a bird that x is fond of, since x(Θ x) = Θ x. The forest has a small founding population. The Mockingbird M repeats what it hears, M x = x x; the Lark L obeys L x y = x(y y); the Bluebird B composes, B x y z = x(y z); the Kestrel K x y = x and the Starling S x y z = x z(y z) are the two from which, with the Identity bird I, every other bird can be derived.

head normal form, and the tree of them  A λ-term is solvable when it has a head normal form — when it reduces to λx₁…xₙ. y M₁…Mₖ, an abstraction over a variable y (the head) applied to arguments. The head is the one stable thing a computation commits to first; everything else can still change. The Böhm tree BT(M) records exactly this, recursively: head-reduce M to its head normal form, write down the head, and hang beneath it the Böhm trees of the arguments M₁, …, Mₖ — descending forever if the term never stops producing heads. A term with no head normal form at all (an unsolvable term, like Ω) contributes nothing, a bare ⊥. The Böhm tree is the term's eventual skeleton, the part of its behaviour that survives all further reduction.

why this silences the usual instrument  The reason the shared tree matters is that the Böhm tree is normally decisive. Böhm's separation theorem (1968) says that two terms with different Böhm trees can always be pulled apart by some context — fed to a surrounding term that sends one to true and the other to false — and this “Böhm-out” technique is the engine behind the standard models, where two terms are equal precisely when their Böhm trees agree (up to the infinite η-expansions that D_∞ also identifies). For ordinary terms, the tree is the verdict. But separation only separates trees that differ, and the combinators' trees do not differ. The single most powerful instrument for distinguishing λ-terms returns, for this family, no reading at all. If the combinators are genuinely distinct — and they are — the difference must live in something the tree throws away.

putting a clock on the tree  The Böhm tree records which heads appear and forgets when. Restore the timing and you have the instrument the modern theory turns on: the clocked Böhm tree of Endrullis, Hendriks and Klop, in which every node carries the number of head-reduction steps it cost to expose. The bare tree of a fixed-point combinator is the featureless spine f, f, f, …; its clock is the sequence of waits between one f and the next. That sequence is not featureless at all. It is a genuine invariant of the term — coarse enough to ignore the cosmetic choices of bound-variable names, fine enough to register a real difference in the rhythm of computation — and on this family it speaks where the tree was silent.

a third equality, between the two we knew  The clock is not merely a trick for this family; it occupies a precise place in the order of distinctions. Plain β-convertibility is the finest relation — interconvertible terms are identical for every purpose — and Böhm-tree equality is among the coarsest, identifying everything with the same eventual skeleton. The clocked tree sits strictly between them: convertible terms always have the same clock, terms with the same clock always have the same tree, and both implications can fail in reverse. So the clock catches differences the tree misses — enough to split the entire Böhm sequence, proving it has no duplicates — without claiming to decide convertibility outright, for there are combinators that keep the same simple clock yet remain inconvertible. For those the theory sharpens the instrument further, to an atomic clock that times individual reduction events, and reaches still finer with Lévy–Longo and Berarducci trees, which remember more of what ordinary Böhm trees discard about non-terminating subterms. The discrimination of the family is a ladder of ever-finer clocks, climbing toward convertibility without ever quite arriving.

how many fixed points?  Begin with a question that sounds too simple to be open. The Fixed-Point Theorem hands every λ-term at least one fixed point. How many are there? The fixed-point property conjectures a stark dichotomy: every term has either exactly one fixed point or infinitely many — never two, never seventeen. It is known to hold in two important cases — when the term has a fixed point in normal form (Intrigila and Statman, 2000), and when open fixed points are allowed (Manzonetto, Polonsky, Saurin and Simonsen, 2019) — and it is known to fail in every sensible λ-theory, where some term can be made to have an intermediate count. But for closed terms in the pure calculus the general question — can a λ-term have a finite number of fixed points greater than one? — remains, after all this time, unanswered.

breeding faster than discriminating  The asymmetry runs deeper than two famous problems. Postfixing the Owl is only the simplest way to breed combinators; working in the infinitary λ-calculus, Endrullis and Klop exhibit infinitely many other generation schemes, modular building blocks that assemble new fixed-point combinators at will. Creation is cheap. The cost is always the same: having made a new combinator, one must prove it is new — prove it β-inconvertible with every combinator already in hand — and that is exactly the discrimination problem, where, as Intrigila remarked, the techniques are remarkably few. Even the most natural follow-up to the previous movement is open: the standard Böhm sequence from Curry's Y is proven duplicate-free by its clocks, but whether the sequence Z, Z δ, Z δ², … begun from an arbitrary combinator Z ever repeats is not known. The family grows faster than we can sort it, and the clock — the finest instrument we have — runs out before the questions do.

the recognition question  We have a generator that breeds combinators, a clock that distinguishes them, and a frontier of open problems. The most basic computational question remains: is there an algorithm that, handed a closed λ-term, decides whether it is a fixed-point combinator? Membership in the family is a Π-shaped condition — Y F =β F(Y F) must hold for every F — and conditions of that shape are rarely decidable. Here they are provably not, and the reason is a theorem at the foundation of the subject's undecidability.

even the look-alikes escape enumeration  The undecidability is not an artefact of the strict fixed-point equation; it survives loosening. Call a term a non-standard fixed-point combinator if it merely has the same Böhm tree as one — the spine λf.f^ω — whether or not it satisfies the equation. Every genuine combinator is non-standard, but not conversely: there are strictly non-standard combinators, terms that unfold into f(f(f(…))) and yet fail to be fixed-point combinators at all — the tree, once more, underdetermining the term. And the set of these look-alikes is not even recursively enumerable; one cannot so much as list the terms that share the combinators' tree. So the family is hemmed by undecidability on every side: infinite, bred by a single Owl, rigid enough that a clean clock separates its members, and yet impossible to recognise, impossible to enumerate even in its loosest form. The most surveyed term in the λ-calculus heads a population that admits no census.