One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm.
Roughly speaking, the *Böhm tree* of a lambda term is its infinite normal form.
If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible.
But what if their Böhm trees coincide?
For example, all fixed-point combinators have the same Böhm tree, namely
\[ \lambda x. x(x(x(\ldots))) \]

We refine Böhm trees with a *clock* that records how many head reduction steps have been used to rewrite each subterm to head normal form.
We show that *clocked Böhm trees* are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.

We refer to *Discriminating Lambda-Terms Using Clocked Boehm Trees* (LMCS 2014) for an extended journal version of this paper.
In the extended version we improve the precision of the clocks to *atomic clocks*
and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

} }