As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.

Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.

To prove such beta-inconvertibilities, we refine the concept of Böhm trees:
we introduce *clocked Böhm trees's* with annotations that convey information of the tempo in which the Böhm trees are produced.
Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms.
An analogous approach pertains to Levy-Longo trees and Berarducci trees.

We illustrate applicability of our refined Böhm trees at the following examples:

- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer a question of Gordon Plotkin:
*Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]*

This paper is an extended version of *Modular Construction of Fixed Point Combinators and Clocked Böhm Trees* (LICS 2010).

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

} }