An Introduction to the Clocked Lambda Calculus

TL;DR

This paper introduces the clocked lambda calculus, an extension of classical lambda calculus that incorporates a tau symbol to witness beta-steps, resulting in an infinitary strongly normalising and confluent system with enriched normal forms.

Contribution

It presents the clocked lambda calculus, a novel extension that enhances classical lambda calculus with infinitary properties and enriched normal forms called clocked Boehm Trees.

Findings

The clocked lambda calculus is infinitary strongly normalising.

It is infinitary confluent.

Normal forms are enriched with clocked Boehm Trees.

Abstract

We give a brief introduction to the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol tau used to witness the beta-steps. In contrast to the classical lambda calculus, this extension is infinitary strongly normalising and infinitary confluent. The infinitary normal forms are enriched Boehm Trees, which we call clocked Boehm Trees.