Clocked lambda calculus

摘要

One of the best-known methods for discriminating λ-terms with respect to β-convertibility isrndue to Corrado Boehm. The idea is to compute the infinitary normal form of a λ-term M, thernBoehm Tree (BT) of M. If λ-terms M, N have distinct BTs, then M u0003=β N, that is, M and Nrnare not β-convertible. But what if their BTs coincide? For example, all fixed pointrncombinators (FPCs) have the same BT, namely λx.x(x(x(. . .))).rnWe introduce a clocked λ-calculus, an extension of the classical λ-calculus with a unaryrnsymbol τ used to witness the β-steps needed in the normalization to the BT. This extensionrnis infinitary strongly normalizing, infinitary confluent and the unique infinitary normal formsrnconstitute enriched BTs, which we call clocked BTs. These are suitable for discriminating arnrich class of λ-terms having the same BTs, including the well-known sequence of Boehm’srnFPCs.rnWe further increase the discrimination power in two directions. First, by a refinement of therncalculus: the atomic clocked λ-calculus, where we employ symbols τp that also witness thern(relative) positions p of the β-steps. Second, by employing a localized version of the (atomic)rnclocked BTs that has even more discriminating power.