This theoretical pearl is about the closed term model of pure untyped lambda-terms modulo
β-convertibility. A consequence of one of the results is that for arbitrary distinct combinators
(closed lambda terms) M, M′, N, N′ there is a combinator H such that
formula here
The general result, which comes from Statman (1998), is that uniformly r.e. partitions of the
combinators, such that each ‘block’ is closed under β-conversion, are of the form
{H−1{M}}M∈ΛΦ.
This is proved by making use of the idea behind the so-called Plotkin-terms, originally devised
to exhibit some global but non-uniform applicative behaviour. For expository reasons we
present the proof below. The following consequences are derived: a characterization of
morphisms and a counter-example to the perpendicular lines lemma for β-conversion.