Summary
One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm.
Roughly speaking, the Böhm tree of a lambda term is its infinite normal form.
If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible.
But what if their Böhm trees coincide?
For example, all fixed-point combinators have the same Böhm tree, namely
\[ \lambda x. x(x(x(\ldots))) \]
We refine Böhm trees with a clock that records how many head reduction steps have been used to rewrite each subterm to head normal form.
We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.
We refer to Discriminating Lambda-Terms Using Clocked Boehm Trees (LMCS 2014) for an extended journal version of this paper.
In the extended version we improve the precision of the clocks to atomic clocks
and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
@inproceedings{lambda:clocks:2010,
author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
title = {{Modular Construction of Fixed Point Combinators and Clocked B\"{o}hm Trees}},
booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2010)},
pages = {111--119},
publisher = {{IEEE} Computer Society},
year = {2010},
doi = {10.1109/LICS.2010.8},
keywords = {rewriting, infinitary rewriting, lambda calculus},
type = {conference}
}