Applications of Plotkin-Terms: Partitions and Morphisms for Closed Terms

Abstract

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.