Clocked lambda calculus ^†

One of the best-known methods for discriminating λ-terms with respect to β-convertibility is due to Corrado Böhm. The idea is to compute the infinitary normal form of a λ-term M, the Böhm Tree (BT) of M. If λ-terms M, N have distinct BTs, then M ≠_β N, that is, M and N are not β-convertible. But what if their BTs coincide? For example, all fixed point combinators (FPCs) have the same BT, namely λx.x(x(x(. . .))). We introduce a clocked λ-calculus, an extension of the classical λ-calculus with a unary symbol τ used to witness the β-steps needed in the normalization to the BT. This extension is infinitary strongly normalizing, infinitary confluent and the unique infinitary normal forms constitute enriched BTs, which we call clocked BTs. These are suitable for discriminating a rich class of λ-terms having the same BTs, including the well-known sequence of Böhm's FPCs. We further increase the discrimination power in two directions. First, by a refinement of the calculus: the atomic clocked λ-calculus, where we employ symbols τ_p that also witness the (relative) positions p of the β-steps. Second, by employing a localized version of the (atomic) clocked BTs that has even more discriminating power.