The interpretation of unsolvable λ-terms in models of untyped λ-calculus

Journal of Symbolic Logic 63 (4):1529-1548 (1998)
  Copy   BIBTEX

Abstract

Our goal in this paper is to analyze the interpretation of arbitrary unsolvable λ-terms in a given model of λ-calculus. We focus on graph models and (a special type of) stable models. We introduce the syntactical notion of a decoration and the semantical notion of a critical sequence. We conjecture that any unsolvable term β-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those two notions: given a graph model or stable model D, we show that any unsolvable term admitting a decoration and having a non-empty interpretation in D generates a critical sequence in the model. In the last section, we examine three classical graph models, namely the model B(ω) of Plotkin and Scott, Engeler's model D A and Park's model D P . We show that B(ω) and D A do not contain critical sequences whereas D P does

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,745

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
19 (#190,912)

6 months
7 (#1,397,300)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Lambda‐Calculus Models and Extensionality.R. Hindley & G. Longo - 1980 - Mathematical Logic Quarterly 26 (19-21):289-310.
Lambda‐Calculus Models and Extensionality.R. Hindley & G. Longo - 1980 - Mathematical Logic Quarterly 26 (19‐21):289-310.

Add more references