Clocked lambda calculus

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

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

Lambda Calculus
Calculus
Term
Normal Form
Fixed point
Unary
Normalization
Discrimination
Refinement
Distinct

Cite this

Endrullis, Jörg ; Hendriks, Dimitri ; Klop, Jan Willem ; Polonsky, Andrew. / Clocked lambda calculus . In: Mathematical Structures in Computer Science (MSCS). 2017 ; Vol. 27, No. 5. pp. 782-806.
@article{b7693a9c43954d27b1cab675192919f7,
title = "Clocked lambda calculus †",
abstract = "One of the best-known methods for discriminating λ-terms with respect to β-convertibility is due to Corrado B{\"o}hm. The idea is to compute the infinitary normal form of a λ-term M, the B{\"o}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{\"o}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.",
author = "J{\"o}rg Endrullis and Dimitri Hendriks and Klop, {Jan Willem} and Andrew Polonsky",
year = "2017",
month = "6",
day = "1",
doi = "10.1017/S0960129515000389",
language = "English",
volume = "27",
pages = "782--806",
journal = "Mathematical Structures in Computer Science (MSCS)",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "5",

}

Clocked lambda calculus . / Endrullis, Jörg; Hendriks, Dimitri; Klop, Jan Willem; Polonsky, Andrew.

In: Mathematical Structures in Computer Science (MSCS), Vol. 27, No. 5, 01.06.2017, p. 782-806.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Clocked lambda calculus †

AU - Endrullis, Jörg

AU - Hendriks, Dimitri

AU - Klop, Jan Willem

AU - Polonsky, Andrew

PY - 2017/6/1

Y1 - 2017/6/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84944112198&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84944112198&partnerID=8YFLogxK

U2 - 10.1017/S0960129515000389

DO - 10.1017/S0960129515000389

M3 - Article

VL - 27

SP - 782

EP - 806

JO - Mathematical Structures in Computer Science (MSCS)

JF - Mathematical Structures in Computer Science (MSCS)

SN - 0960-1295

IS - 5

ER -