Strong stability and the incompleteness of stable models for λ-calculus

Annals of Pure and Applied Logic 100 (1-3):247-277 (1999)
  Copy   BIBTEX

Abstract

We prove that the class of stable models is incomplete with respect to pure λ-calculus. More precisely, we show that no stable model has the same theory as the strongly stable version of Park's model. This incompleteness proof can be adapted to the continuous case, giving an incompleteness proof for this case which is much simpler than the original proof by Honsell and Ronchi della Rocca. Moreover, we isolate a very simple finite set, , of equations and inequations, which has neither a stable nor a continuous model, and which is included in and in , the contextual theory induced by the set of essentially λI-closed terms. Finally, using an approximation theorem suitable for a large class of models , we prove that and are included in , giving an operational meaning to the equality in these models

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,553

External links

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

Through your library

Similar books and articles

Projecting sequential algorithms on strongly stable functions.Thomas Ehrhard - 1996 - Annals of Pure and Applied Logic 77 (3):201-244.
Expansions of models of ω-stable theories.Steven Buechler - 1984 - Journal of Symbolic Logic 49 (2):470-477.
Ranks and pregeometries in finite diagrams.Olivier Lessmann - 2000 - Annals of Pure and Applied Logic 106 (1-3):49-83.
Non-isolated types in stable theories.Predrag Tanović - 2007 - Annals of Pure and Applied Logic 145 (1):1-15.
On uniqueness of prime models.Saharon Shelah - 1979 - Journal of Symbolic Logic 44 (2):215-220.
Unidimensional theories are superstable.Ehud Hrushovski - 1990 - Annals of Pure and Applied Logic 50 (2):117-138.
Unidimensional theories are superstable.Katsuya Eda - 1990 - Annals of Pure and Applied Logic 50 (2):117-137.
Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
Simplicity and uncountable categoricity in excellent classes.Tapani Hyttinen & Olivier Lessmann - 2006 - Annals of Pure and Applied Logic 139 (1):110-137.

Analytics

Added to PP
2014-01-16

Downloads
48 (#465,651)

6 months
14 (#247,632)

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

No references found.

Add more references