Summary
As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible.
Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree.
This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.
Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus,
and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.
To prove such beta-inconvertibilities, we refine the concept of Böhm trees:
we introduce clocked Böhm trees's with annotations that convey information of the tempo in which the Böhm trees are produced.
Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms.
An analogous approach pertains to Levy-Longo trees and Berarducci trees.
We illustrate applicability of our refined Böhm trees at the following examples:
- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer 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 ))
\]
We further increase the discrimination power of the technique by enhancing the precision of the clock, arriving at a notion that we call
atomic clocks.
This paper is an extended version of Modular Construction of Fixed Point Combinators and Clocked Böhm Trees (LICS 2010).
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
@article{lambda:clocks:2014,
author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}},
journal = {Logical Methods in Computer Science},
volume = {10},
number = {2},
year = {2014},
doi = {10.2168/LMCS-10(2:4)2014},
keywords = {rewriting, infinitary rewriting, lambda calculus},
type = {journal}
}