Clocked lambda calculus

One of the best-known methods for discriminating lambda-terms with respect to beta-convertibility is due to Corrado Bohm. The idea is to compute the infinitary normal form of a lambda-term M, the Bohm Tree (BT) of M. If lambda-terms M, N have distinct BTs, then M not equal(beta) N, that is, M and N are not beta-convertible. But what if their BTs coincide? For example, all fixed point combinators (FPCs) have the same BT, namely lambda x. x(x(x(...))). We introduce a clocked lambda-calculus, an extension of the classical lambda-calculus with a unary symbol tau used to witness the beta-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 lambda-terms having the same BTs, including the well-known sequence of Bohm's FPCs. We further increase the discrimination power in two directions. First, by a refinement of the calculus: the atomic clocked lambda-calculus, where we employ symbols tau(p) that also witness the (relative) positions p of the beta-steps. Second, by employing a localized version of the (atomic) clocked BTs that has even more discriminating power.