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 witness 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 different 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 existence 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 imply a negative answer to Statman’s question.

Research: Clocked Lambda Calculus

Clocked Böhm Trees

Relevant Papers

References

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier