Abstract
Aim of this paper is to investigate the soundness and completeness for the F-semantics (F-soundness and F-completeness) of some modifications of the intersection type discipline for terms of the (untyped) λ-calculus.
As pointed out by Scott, the key of a λ-model is the set F of the elements representing functions. The F-semantics of types takes into account that the intuitive meaning of “ δ → τ ” is “a function with domain δ and range τ ” and interprets δ → τ as a subset of F.
The type theories which induce F-complete type assignments are characterized. It results that a type assignment is F-complete iff the following are derived rules for it: {ie279-1}
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Barendregt H., The Lambda Calculus, its Syntax and Semantics, (North-Holland, Amsterdam, 1981).
Barendregt H., Coppo M., Dezani-Ciancaglini M., A Filter Lambda Model and the Completeness of Type Assignment, J. Symbolic Logic 48 (1983) 931–940.
Ben-Yelles C.B., Type Assignment in the Lambda-Calculus: Syntax and Semantics, Doctoral Thesis, University College of Swansea, 1979.
Bruce K., Meyer A., The Semantics of Second Order Polymorphic Lambda Calculus, in this volume.
Coppo M., An Extended Polymorphic Type System for Applicative Languages, in: P. Dembinski, ed., Mathematical Foundations of Computer Science 1980, 9th Symposium, LNCS 88, (Springer-Verlag, Berlin, 1980) pp. 194–204.
Coppo M., On the Semantics of Polymorphism, Acta Informatica, 20 (1983) 159–170.
Coppo M., Completeness of Type Assignment in Continuous Lambda Models, Theor. Comput. Sci. (to appear).
Coppo M., Dezani-Ciancaglini M., A New Type Assignment for λ-terms, Archiv für Math. Logik und Grundlagenforschung 19 (1979) 139–156.
Coppo M., Dezani-Ciancaglini M., An Extension of the Basic Functionality Theory for the λ-Calculus, Notre Dame J. of Formal Logic 21-4 (1980) 685–693.
Coppo M., Dezani-Ciancaglini M., Honsell F., Longo G., Extended Type Structures and Filter Lambda Models, in: G. Lolli et al., eds. Logic Colloquium '82, (North-Holland, Amsterdam, 1983) (to appear).
Coppo M., Dezani-Ciancaglini M., Venneri B., Functional Characters of Solvable Terms, Z. Math. Logik Grundlag. Math. 27 (1981) 45–58.
Coppo M., Dezani-Ciancaglini M., Venneri B., Principal Type Schemes and λ-calculus Semantics in: R.Hindley and J.P.Seldin, eds., To H.B.Curry, Essay in Combinatory Logic, Lambda Calculus and Formalism, (Academic Press, 1980) pp. 595–560.
Coppo M., Dezani-Ciancaglini M., Zacchi M., Type Theories, Normal Forms and D∞ — Lambda Models, Internal Report, Computer Science Department, Turin University, 1983.
Coppo M., Giovannetti E., Completeness Results for a Polymorphic Type System, in: G. Ausiello, ed., CAAP 83, LNCS, 159 (Springer-Verlag, Berlin 1983) pp.179–190.
Curry H.B., Feys R., Combinatory Logic I, (North Holland, Amsterdam, 1958).
Curry H.B., Hindley R., Seldin J.P., Combinatory Logic II, (North Holland, Amsterdam, 1972).
Dezani-Ciancaglini M., Margaria I., A Characterization of F-complete Polymorphic Type Assignments, Internal Report, Computer Science Department, Turin University 1983.
Fortune S., Leivant D., O'Donnel M., The Expressiveness of Simple and Second Order Type Structures, Journal of ACM 30 (1983) 151–185.
Hindley R., The Principal Type Scheme of an Object in Combinatory Logic, Trans. Amer. Math. Soc. 146 (1969) 29–60.
Hindley R., The Completeness Theorem for Typing λ-terms, Theor. Comput. Sci. 22 (1) (1983) 1–17.
Hindley R., Curry's Type-Rules are Complete with respect to F-semantics too, Theor. Comput. Sci. 22 (1) (1983) 127–133.
Hindley R., The Simple Semantics for Coppo-Dezani-Sallé Type Assignment, in: M. Dezani-Ciancaglini and U. Montanari, eds., International Symposium on Programming, LNCS, 137, (Springer-Verlag, Berlin 1981) pp. 212–226.
Hindley R., Private Communication, (1980).
Hindley R., Longo G., Lambda Calculus Models and Extensionality, Zeitschr. Math. Logik 26 (1980) 289–310.
Leivant D., Polymorphic Type Inference, Proc. 10th ACM Symposium on Principles of Programming Languages, Austin Texas (1983), 88–98.
Longo G., Set-Theoretical Model of λ-calculus: Theories, Expansions, Isomorphism, Annals of Pure and Applied Logic 24(2) (1983) 153–188.
Milner R., Fully Abstract Models of Typed λ-calculus, Theor. Comput. Sci. 4 (1977) 1–22.
McCracken N., An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. Thesis, Syracuse University, 1979.
Mac Queen D.B., Sethy R., A Semantic Model of Types for Applicative Languages, ACM Symposium of LISP and Functional Programming, (1983), pp. 243–252.
Reynolds J.C., Towards a Theory of Type Structure in: B. Robinet, ed., Programming Symposium, LNCS 19 (Springer-Verlag, Berlin, 1974) pp. 408–425.
Reynolds J.C., Types, Abstraction and Parametric Polymorphism, in R.F.A. Mason, ed., Proceedings IFIP 83 (North-Holland, Amsterdam, 1983) pp. 513–529.
Scott D.S., Open Problems n.II, 4 in C. Böhm, ed., λ-calculus and Computer Science Theory, LNCS 37, (Springer-Verlag, Berlin, 1975) p.368.
Scott D.S., Data Types as Lattices, SIAM J. Comput. 5 (1976) 522–587.
Scott D.S., Lambda Calculus: some Models, some Philosophy, in: I. Barwise et al., eds., The Kleene Symposium, Studies in Logic, (North-Holland, Amsterdam, 1980) pp. 223–266.
Scott D.S., Letter to Albert Meyer (1980).
Scott D.S., Domains for Denotational Semantics in: M. Nielsen and E. Schmidt, eds. Automata, Language and Programming, LNCS 140 (Springer-Verlag, Berlin, 1982) pp. 577–610.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dezani-Ciancaglini, M., Margaria, I. (1984). F-semantics for intersection type discipline. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds) Semantics of Data Types. SDT 1984. Lecture Notes in Computer Science, vol 173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-13346-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-13346-1_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13346-9
Online ISBN: 978-3-540-38891-3
eBook Packages: Springer Book Archive