Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-05T16:47:28.655Z Has data issue: false hasContentIssue false

Applications of Plotkin-terms: partitions and morphisms for closed terms

Published online by Cambridge University Press:  01 September 1999

RICHARD STATMAN
Affiliation:
Department of Mathematics, Carnegie-Mellon University, Pittsburgh, Pennsylvania 15213, USA. (e-mail: [email protected])
HENK BARENDREGT
Affiliation:
Department of Computer Science, Catholic University, Box 9102, 6500 HC Nijmegen, The Netherlands. (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.