×

Building continuous webbed models for system F. (English) Zbl 1079.03017

Summary: We present here a large family of concrete models for Girard and Reynolds polymorphism (system F), in a noncategorical setting. The family generalizes the construction of the model of Barbanera and Berardi, hence it contains complete models for F\(\eta\), and we conjecture that it contains models which are complete for F. It also contains simpler models, the simplest of them, \(\mathcal E^2\), being a second-order variant of the Engeler-Plotkin model \(\mathcal E\). All the models here belong to the continuous semantics and have underlying prime algebraic domains, all have the maximum number of polymorphic maps. The class contains models which can be viewed as two intertwined compatible webbed models of untyped \(\lambda\)-calculus (in the sense of C. Berline [“From computations to foundations: the \(\lambda\)-calculus and its webbed models, revised version”, Theor. Comput. Sci. (to appear)]), but it is much larger than this. Finally, many of its models might be read as two intertwined strict intersection type systems.

MSC:

03B70 Logic in computer science
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] R. Amadio, K. Bruce, G. Longo, The finitary projection model for 2nd order calculus, IEEE Conf. on Logic in Computer Science, Boston, Juin, 1986.; R. Amadio, K. Bruce, G. Longo, The finitary projection model for 2nd order calculus, IEEE Conf. on Logic in Computer Science, Boston, Juin, 1986.
[2] Barbanera, F.; Berardi, S., A full continuous model of polymorphism, Theoret. Comput. Sci., 290, 407-428 (2003) · Zbl 1018.68015
[3] H. Barendregt, The lambda-calculus, its syntax and semantics, Studies in Logic, revised ed., Vol. 103, North-Holland, Amsterdam, 1984.; H. Barendregt, The lambda-calculus, its syntax and semantics, Studies in Logic, revised ed., Vol. 103, North-Holland, Amsterdam, 1984. · Zbl 0551.03007
[4] Berardi, S., Retractions on dI-domains as a model for typetype, Inform. and Comput., 94, 204-231 (1991) · Zbl 0728.68036
[5] Berardi, S.; Berline, C., βη-complete models for System \(F\), Math. Struct. Comput. Sci., 12, 823-874 (2002) · Zbl 1029.03004
[6] S. Berardi, C. Berline, Easy models for \(F_ωY\), Calculus of Construction, and Types: Types, in preparation.; S. Berardi, C. Berline, Easy models for \(F_ωY\), Calculus of Construction, and Types: Types, in preparation. · Zbl 0968.68087
[7] Berline, C., Retractions et interprétation interne du polymorphismele problème de la rétraction universelle, Informatique Théorique et Applications (Theoret. Informatics Appl.), 26, 1, 59-91 (1992) · Zbl 0751.03004
[8] Berline, C., From computations to foundations: the \(λ\)-calculus and its webbed models, revised version, Theoret. Comput. Sci., 249, 81-161 (2000) · Zbl 0949.68049
[9] M. Coppo, M. Dezani-Ciangaglini, F. Honsell, G. Longo, Extended type structures and filter \(λ\)-models, in: G. Longo, G. Lolli, A. Marcja (Eds.), Logic Coll, Vol. 82, Elsevier Science Publishers, Amsterdam, 1984, pp. 241-262.; M. Coppo, M. Dezani-Ciangaglini, F. Honsell, G. Longo, Extended type structures and filter \(λ\)-models, in: G. Longo, G. Lolli, A. Marcja (Eds.), Logic Coll, Vol. 82, Elsevier Science Publishers, Amsterdam, 1984, pp. 241-262. · Zbl 0558.03007
[10] T. Coquand, C. Gunter, G. Winskel, DI-domains as a model of polymorphism, 3rd Workshop on Mathematical Foundations of Programming Language Semantics (April 87), Lecture Notes in Computer Science, Vol. 298, Springer, Berlin, 1987, pp. 344-363.; T. Coquand, C. Gunter, G. Winskel, DI-domains as a model of polymorphism, 3rd Workshop on Mathematical Foundations of Programming Language Semantics (April 87), Lecture Notes in Computer Science, Vol. 298, Springer, Berlin, 1987, pp. 344-363. · Zbl 0644.68041
[11] Coquand, T.; Gunter, C.; Winskel, G., Domain theoretical models of polymorphism, Inform. and Comput., 81, 123-167 (1989) · Zbl 0683.03007
[12] Engeler, E., Algebras and combinators, Alg. Univ., 13, 3, 289-371 (1981)
[13] Friedman, H., Equality between functionals, (Parikh, R., Logic Coll. 1972-1973. Logic Coll. 1972-1973, Lecture Notes in Mathematics, Vol. 453 (1975), Springer: Springer New York), 22-37
[14] Girard, J. Y., Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures et à la théorie des types, (Fenstadt, J. E., Proc. 2nd Scandinavian Logic Symp (1971), North-Holland: North-Holland Amsterdam), 63-92
[15] J.Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’Arithmétique d’ordre supérieure, Thèse, Vol. 7, Université Paris, 1972.; J.Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’Arithmétique d’ordre supérieure, Thèse, Vol. 7, Université Paris, 1972.
[16] Girard, J. Y., System \(F\) of variable types, fifteen years later, Theoret. Comput. Sci., 45, 159-192 (1986) · Zbl 0623.03013
[17] Jiang, Y.; Gouy, X., Universal retractions on dI-domains, Inform. and Comput., 119, 2, 252-257 (1995) · Zbl 0832.68066
[18] Krivine, J. L., Lambda-calcul, Types et Modèles (1990), Masson: Masson Paris
[19] Krivine, J. L., Lambda-calculus, Types and Models (1993), Ellis-Horwood: Ellis-Horwood Chichester, UK, (augmented english translation of the above) · Zbl 0779.03005
[20] K.G. Larsen, G. Winskel, Using Information Systems to Solve Recursive Domain Equations, Lecture Notes in Computer Science, Vol. 173 (Semantics of data types), Springer, Berlin, 1984, pp. 109-130.; K.G. Larsen, G. Winskel, Using Information Systems to Solve Recursive Domain Equations, Lecture Notes in Computer Science, Vol. 173 (Semantics of data types), Springer, Berlin, 1984, pp. 109-130. · Zbl 0539.68019
[21] Longo, G., Set-theoretical models of \(λ\)-calculustheories, expansions and isomorphisms, Ann. Pure Appl. Logic, 24, 153-188 (1983) · Zbl 0513.03009
[22] Longo, G.; Milsted, K.; Soloviev, S., The genericity theorem and the notion of parametricity in the polymorphic \(λ\)-calculus, Theoret. Comput. Sci., 121, 323-349 (1993) · Zbl 0793.03008
[23] N. McCracken, An investigation of a programming language with a polymorphic type structure, Ph.D. Dissertation, School of Computer and Information Science, Syracuse University, Syracuse, New York, June 1979, 126pp.; N. McCracken, An investigation of a programming language with a polymorphic type structure, Ph.D. Dissertation, School of Computer and Information Science, Syracuse University, Syracuse, New York, June 1979, 126pp.
[24] N. McCracken, A Finitary Retract Model for the Polymorphic \(λ\)-calculus, unpublished, 1984.; N. McCracken, A Finitary Retract Model for the Polymorphic \(λ\)-calculus, unpublished, 1984.
[25] Nielsen, M.; Plotkin, G.; Winskel, G., Petri nets, event structures and domains, Part I, Theoret. Comput. Sci., 13, 85-108 (1981) · Zbl 0452.68067
[26] P. O’Hearn, Parametric polymorphism, in: M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, I. Stark (Eds.), Domains and Denotational Semantics: History, Accomplishments and Open Problems, Bulletin of EATCS, Vol. 59, 1996, pp. 227-256.; P. O’Hearn, Parametric polymorphism, in: M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, I. Stark (Eds.), Domains and Denotational Semantics: History, Accomplishments and Open Problems, Bulletin of EATCS, Vol. 59, 1996, pp. 227-256.
[27] D. Park, The Y combinator in Scott’s Lambda-calculus models, Theory of Computation Report 13, Department of Computer Science, University of Warwick, 1976.; D. Park, The Y combinator in Scott’s Lambda-calculus models, Theory of Computation Report 13, Department of Computer Science, University of Warwick, 1976.
[28] 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.
[29] J. Reynolds, Toward a theory of type structures, Colloque sur la programmation, Lecture Notes in Computer Science, Vol. 19, Springer, Berlin, 1974, pp. 408-425.; J. Reynolds, Toward a theory of type structures, Colloque sur la programmation, Lecture Notes in Computer Science, Vol. 19, Springer, Berlin, 1974, pp. 408-425.
[30] Reynolds, J., Types, abstraction and parametric polymorphism, (Mason, R. E.A., Information Processing 83, Proc. IFIP 9th World Computer Science Congr., Paris, September 1983 (1983), Elsevier Science Publishers B.V. (North-Holland): Elsevier Science Publishers B.V. (North-Holland) Amsterdam), 513-523
[31] Scott, D., Data types as lattices, SIAM J. Comput., 5, 3, 522-587 (1976) · Zbl 0337.02018
[32] D. Scott, A space of retracts, manuscript, 1980.; D. Scott, A space of retracts, manuscript, 1980.
[33] D. Scott, Domains for Denotational Semantics, Lecture Notes in Computer Science, Vol. 140, ICALP’82, Springer, Berlin, 1982, pp. 577-613.; D. Scott, Domains for Denotational Semantics, Lecture Notes in Computer Science, Vol. 140, ICALP’82, Springer, Berlin, 1982, pp. 577-613. · Zbl 0495.68025
[34] A. Simpson, Categorical completeness results for the simply-typed \(λ\)-calculus, in: M. Dezani-Ciancaglini, G. Plotkin (Eds.), Lecture Notes in Computer Science, Vol. 902, TLCA’95, Springer, Berlin, 1995, pp. 414-427.; A. Simpson, Categorical completeness results for the simply-typed \(λ\)-calculus, in: M. Dezani-Ciancaglini, G. Plotkin (Eds.), Lecture Notes in Computer Science, Vol. 902, TLCA’95, Springer, Berlin, 1995, pp. 414-427. · Zbl 1063.03524
[35] A.S. Troelstra, Notes on second order arithmetic, in: Mathias, Rogers (Eds.), Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics, Vol. 337, Springer, Berlin, 1973, pp. 171-205.; A.S. Troelstra, Notes on second order arithmetic, in: Mathias, Rogers (Eds.), Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics, Vol. 337, Springer, Berlin, 1973, pp. 171-205. · Zbl 0275.02036
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.