Clocked lambda calculus

Jörg Endrullis*, Dimitri Hendriks, Jan Willem Klop, Andrew Polonsky

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

2 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)782-806
Number of pages25
JournalMathematical Structures in Computer Science (MSCS)
Issue number5
Early online date15 Oct 2015
Publication statusPublished - Jun 2017

Bibliographical note

Computing with Lambda-terms. A Special Issue Dedicated to Corrado Böhm for his 90th Birthday


Dive into the research topics of 'Clocked lambda calculus '. Together they form a unique fingerprint.

Cite this