Clocked Lambda Calculus

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

Mathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)
# Abstract

We introduce the *clocked lambda calculus*,
an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps.
This calculus consists of the following two rules:
\[
\begin{aligned}
(\lambda x.M) N &\to \tau( M[x = N] ) \\
\tau(M)N &\to \tau(MN)
\end{aligned}
\]
The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent,
and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees),
which we call *clocked Böhm trees*.
We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

@article{clocked:lambda:calculus:2017,
author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
title = {{Clocked Lambda Calculus}},
journal = {Mathematical Structures in Computer Science},
volume = {27},
number = {5},
pages = {782--806},
year = {2017},
doi = {10.1017/S0960129515000389},
keywords = {rewriting, infinitary rewriting, lambda calculus},
type = {journal}
}