Clocked lambda calculus†. (15th October 2015)

• Record Type: Journal Article
• Authors: ENDRULLIS, JÖRG; HENDRIKS, DIMITRI; KLOP, JAN WILLEM; POLONSKY, ANDREW
• Is Part Of: Mathematical structures in computer science. Volume 27:Number 5(2017)
• Page Start: 782
• Page End: 806
• Publication Date: 2015-10-15
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129515000389
• Languages: English
• ISSNs: 0960-1295

Abstract

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.