×

On the construction of stable models of untyped \(\lambda\)-calculus. (English) Zbl 0992.68022

Summary: Stable models of untyped \(\lambda\)-calculus have been introduced by G. Berry [Lect. Notes Comput. Sci. 62, 72-89 (1978; Zbl 0382.68041)] as a refinement of the continuous framework defined by Scott (unpublished manuscript, 1969, 53pp.). In this paper, we show that even in the stable case we have a fair amount of freedom during the construction of models. We introduce a uniform method to construct stable models that allows to obtain non standard models satisfying certain equational restraints. We apply this method in two particular examples: first, we construct a simple stable model that distinguishes the \(\lambda\)-terms \(Y\) and \(\theta\). Second, we construct a family of \(2^{\aleph_{0}}\) stable models with pairwise distinct theories. We show that the latter models are sensible using some results of R. David [Lect. Notes Comput. Sci. 1581, 98-113 (1999; Zbl 0931.03020)] and R. Kerth [J. Symb. Log. 63, No. 4, 1529-1548 (1998; Zbl 0930.03013)].

MSC:

68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baeten, J.; Boerboom, B., \( Ω\) can be Anything it should not be, Indag. Math., 41, 111-120 (1979) · Zbl 0417.03006
[2] Barendregt, H., Degrees of sensible lambda theories, J. Symbolic Logic, 43, 45-55 (1978) · Zbl 0408.03012
[3] Barendregt, H., The \(λ\)-Calculus, Its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007
[4] G. Berry, Stable models of typed \(λ\); G. Berry, Stable models of typed \(λ\)
[5] David, R., Every unsolvable \(λ\)-term admits a decoration. Every unsolvable \(λ\)-term admits a decoration, Proceedings of TLCA 1999, Lecture Notes in Computer Science, Vol. 1581 (1999), Springer: Springer Berlin · Zbl 0931.03020
[6] Girard, J.-Y., The system \(F\) of variable types, fifteen years later, Theoret. Comput. Sci., 45, 159-192 (1986) · Zbl 0623.03013
[7] Hindley, J. R.; Longo, G., Lambda calculus models and extensionality, Z. Logik Grundlag. Math., 26, 289-310 (1980) · Zbl 0453.03015
[8] Honsell, F.; Lenisa, M., Some Results on the Full Abstraction Problem for Restricted Lambda Calculi, (Lecture Notes in Computer Science, Vol. 711 (1993), Springer: Springer Berlin), 84-104 · Zbl 0925.03095
[9] Honsell, F.; Ronchi Della Rocca, S., Reasoning about interpretations in qualitative \(λ\)-models, (Broy, M.; Jones, C., Proceedings of the IFIP Conference Programming Concepts and Methods (1990), North-Holland: North-Holland Amsterdam) · Zbl 0665.03010
[10] Honsell, F.; Ronchi Della Rocca, S., An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, J. Comput. System Sci., 45, 49-75 (1992) · Zbl 0763.03012
[11] Hyland, M., A syntactic characterization of the equality in some models for the lambda calculus, J. London Math. Soc., 12, 2, 361-370 (1976) · Zbl 0329.02010
[12] Kerth, R., Isomorphism and equational equivalence of continuous \(λ\)-models, Proceedings of the ASL Logic Colloquium 1994, Studia Logica, 61, 3, 403-415 (1998) · Zbl 0964.03015
[13] Kerth, R., The interpretation of unsolvable terms in models of untyped \(λ\)-calculus, J. Symbolic Logic, 63, 1529-1548 (1998) · Zbl 0930.03013
[14] Kerth, R., Forcing in stable models of untyped \(λ\)-calculus, Indag. Math., 10, 1, 59-71 (1999) · Zbl 1025.03503
[15] Krivine, J. L., Lambda-Calculus, Types and Models (1993), Ellis Horwood: Ellis Horwood Hemel Hempstead · Zbl 0779.03005
[16] Meyer, A., What is a model of the Lambda-calculus?, Inform. Control, 52, 87-122 (1982) · Zbl 0507.03002
[17] D. Park, The Y-combinator in Scott’s Lambda calculus models, Theory of Computation Report No. 13, University of Warwick, Department of Computer Science, 1976.; D. Park, The Y-combinator in Scott’s Lambda calculus models, Theory of Computation Report No. 13, University of Warwick, Department of Computer Science, 1976.
[18] G. Plotkin, A set-theoretical Definition of Application, Memorandum MIP-R-95, School of Artificial Intelligence, University of Edinburgh, 1972.; G. Plotkin, A set-theoretical Definition of Application, Memorandum MIP-R-95, School of Artificial Intelligence, University of Edinburgh, 1972.
[19] Plotkin, G., LCF as a programming language, Theoret. Comput. Sci., 5, 3, 223-257 (1977) · Zbl 0369.68006
[20] D.S. Scott, Models for the \(λ\); D.S. Scott, Models for the \(λ\)
[21] Scott, D. S., Continuous lattices, (Lawvere, F. W., Toposes, Algebraic Geometry and Logic. Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, Vol. 274 (1972), Springer: Springer Berlin), 97-136
[22] Scott, D. S., Lambda calculus and recursion theory, (Kanger, S., Proceedings of the 3rd Scandinavian Logic Symposium. Proceedings of the 3rd Scandinavian Logic Symposium, Studies in Logic, Vol. 82 (1975), North-Holland: North-Holland Amsterdam), 154-193
[23] Scott, D. S., Data types as lattices, SIAM J. Comput., 5, 3, 522-587 (1976) · Zbl 0337.02018
[24] Wadsworth, C. P., The relation between computational and denotational properties for Scott’s \(D∞\)-models of the Lambda-calculus, SIAM J. Comput., 5, 3, 488-521 (1976) · Zbl 0346.02013
[25] Wadsworth, C. P., Approximate reduction and \(λ\)-calculus models, SIAM J. Comput., 7, 3, 337-356 (1978) · Zbl 0407.03021
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.