Discriminating Lambda-Terms Using Clocked Boehm Trees

Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky

Logical Methods in Computer Science , 10 (2) (2014)
# Abstract

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.

@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}
}