Article contents
Applications of Plotkin-terms: partitions and morphisms for closed terms
Published online by Cambridge University Press: 01 September 1999
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.
- Type
- THEORETICAL PEARL
- Information
- Copyright
- © 1999 Cambridge University Press
- 4
- Cited by
Discussions
No Discussions have been published for this article.