Clocked lambda calculus

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

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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)
Volume27
Issue number5
DOIs
Publication statusPublished - 1 Jun 2017

Fingerprint

Dive into the research topics of 'Clocked lambda calculus <sup>†</sup>'. Together they form a unique fingerprint.

Cite this