# Research: Clocked Lambda Calculus

The **clocked lambda calculus** [1] is an extension of the classical lambda calculus.

The classical lambda calculus is based on the \( \beta \)-rule: \[ (\lambda x.M) N \to M[x = N] \]

The clocked lambda calculus introduces a unary symbol \( \tau \) that serves as a wittness of \( \beta \)-steps.

Clocked Lambda Calculus

The **clocked lambda 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}
\]

So the clocked lambda calculus refines lambda calculus such that each \( \beta \)-step produces one symbol \( \tau \). The second rule of the calculus ensures that the \( \tau \)’s can be moved out of the way of \( \beta \)-redex.

Consider **Curry’s fixed-point combinator** \( Y_0 \):
\[
\begin{align}
Y_0 & \equiv \lambda f. \omega_f \omega_f
\\
\omega_f & \equiv \lambda x. f(xx)
\end{align}
\]

We have the following reduction: \[ \begin{align} Y_0 f &\to \tau ( \omega_f \omega_f ) \\ &\to \tau ( \tau ( f (\omega_f \omega_f) ) ) \\ &\to \tau ( \tau ( f ( \tau (f (\omega_f \omega_f) )))) \\ &\to \tau ( \tau ( f ( \tau (f (\tau (f (\omega_f \omega_f) )) )))) \\ &\to \cdots \end{align} \]

Consider **Turing’s fixed-point combinator** \( Y_1 \):
\[
\begin{align}
Y_1 & \equiv \eta \eta
\\
\eta & \equiv \lambda xf. f (xxf)
\end{align}
\]

We have the following reduction: \[ \begin{align} Y_1 f &\equiv \eta \eta f \\ &\to \tau ( (\lambda f. f (\eta \eta f))) f \\ &\to \tau ( (\lambda f. f (\eta \eta f)) f ) \\ &\to \tau ( \tau ( f (\eta \eta f) ) ) \end{align} \]

The clocked lambda calculus is

**confluent**,**infinitary strongly normalizing**and**infinitary confluent**.

Note that the classical lambda calculus does not exhibit the latter two properties.

## Clocked Böhm Trees

Clocked Lévy-Longo Trees

So every term has a unique infinitary normal form.
These infinitary normal forms constitute enriched Lévy-Longo trees (a variant of Böhm trees),
which we call **clocked Lévy-Longo trees**.

So instead of defining Lévy-Longo trees (Böhm trees) by corecursion, in the clocked lambda calculus they arise naturally by rewriting the terms to their infinitary normal form.

Böhm trees are often used to discriminate lambda terms:

If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible.

But what if two terms have the same Böhm trees? For instance all fixed-point combinators have the same Böhm trees (and Lévy-Longo trees), namely: \[ \lambda f. f ( f ( f ( \ldots ))) \] However, they can have differnt clocked Lévy-Longo trees:

The infinite normal form, the clocked Lévy-Longo tree, of

- Curry’s fixed-point combinator \( Y_0 \) is \[ \tau^2 ( f ( \tau (f ( \tau (f ( \tau (\ldots ))))))) \]
- Turing’s fixed-point combinator \( Y_1 \) is \[ \tau^2 ( f ( \tau^2 (f ( \tau^2 (f ( \tau^2 (\ldots ))))))) \]

This can easily be seen from the reductions given above.

So Curry’s and Turing’s fixed-point combinators have distinct clocked Lévy-Longo trees.
Moreover, their `clock speed`

(the number of \( \tau \)’s) differs at an infinite number of positions.
This suffices to conclude that Curry’s and Turing’s fixed-point combinator are not \( \beta \)-convertible
since both Curry’s and Turing’s fixed-point combinators are `simple terms`

.

Clocked Lévy-Longo trees can also be helpful in discriminating general (non-simple) lambda terms. In [2] we use the technique to answer the following question of Gordon Plotkin:

A Question of Gordon Plotkin

Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]

## Relevant Papers

In [3] we introduce **clocked Böhm trees** to discriminate lambda terms with respect to \( \beta \)-convertibility.

In [2] we increase the discrimination power by improving the precision of the clocks, leading to **atomic clocked Böhm trees**, and
we show that the method can be fruitfully applied to general lambda terms by **answering the question of Gordon Plotkin mentioned above**.

In [1] we introduce the **clocked lambda calculus** which internalizes the clock.
Now the *clocked Böhm trees* arise naturally by rewriting, as infinite normal forms.
In contrast to the standard lambda calculus, the *clocked lambda calculus* is infinitary confluent and infinitary strongly normalizing.

In [4] we consider **fixed-point combinator (fpc) generators**,
that is, lambda terms \( G \) such that \( Y G \) is a fixed point combinator whenever \( Y \) is.
We derive a complete characterization of all *simply-typed* fpc generators using *Barendregt’s Inhabitation Machines*.

The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan’s Owl, is a famous fpc generator. It has the peculiar property that a term \( Y \) is a fixed-point combinator if and only if \( Y =_\beta \delta Y \).

This led Richard Statman to the following question:

Statman’s question on the existance of double fixed-point combinators

Is there a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \)?

Statman called this combinator \( Y \) a *double fixed-point combinator* since it would satisfy both
\( Y =_\beta \delta Y \) and \( Y =_\beta Y \delta \).
This question remains **open** as the proof by Benedetto Intrigila contains a gap.

In [4] we present a conjecture that vastly generalizes Statman’s question.
Our conjecture concerns the relation of the \( \mu \)-operator (also known as `letrec`

) and its implementation by fixed-point combinators:

Conjecture

We conjecture that for any fixed-point combinator \( Y \) and simply-typed \(\lambda\mu\)-terms \( s,t \) it holds that

\[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \]

where \(s_Y, t_Y\) are the *untyped* lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).

A confirmation of this conjecture would immediately implya negative answer to Statman’s question.

## References

- Clocked Lambda CalculusJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyMathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)
- Discriminating Lambda-Terms Using Clocked Boehm TreesJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyLogical Methods in Computer Science , 10 (2) (2014)
- Modular Construction of Fixed Point Combinators and Clocked Böhm TreesJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopIn: Proc. Symp. on Logic in Computer Science (LICS 2010), pp. 111–119, IEEE Computer Society (2010)
- Clocks for Functional ProgramsJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyIn: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)