On Realisability Semantics for Intersection Types with Expansion Variables

• Autorzy: Kamareddine F. , Nour K. , Rahli V. , Wells J. B.
• Języki publikacji: EN

Abstrakty

EN

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason about. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for type systems with intersection types, but none whatsoever before our work, on type systems with E-variables. In this paper we expose the challenges of building a semantics for E-variables and we provide a novel solution. Because it is unclear how to devise a space of meanings for E-variables, we develop instead a space of meanings for types that is hierarchical. First, we index each type with a natural number and show that although this intuitively captures the use of E-variables, it is difficult to index the universal type ωwith this hierarchy and it is not possible to obtain completeness of the semantics if more than one E-variable is used. We then move to a more complex semantics where each type is associated with a list of natural numbers and establish that both ů and an arbitrary number of E-variables can be represented without losing any of the desirable properties of a realisability semantics.

Słowa kluczowe

EN

realisability semantics; expansion variables; intersection types; completeness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 121, nr 1/4
• Strony: 153--184
• Opis fizyczny: Bibliogr. 27 poz.

Twórcy

autor

Kamareddine F.

autor

Nour K.

autor

Rahli V.

autor

Wells J. B.

• ULTRA Group (Useful Logics, Types, Rewriting, and their Automation), Heriot-Watt University, School of Mathematical and Computer Sciences, Edinburgh EH14 4AS, UK. http://www.macs.hw.ac.uk/ultra

Bibliografia

• [1] Bakel, S. V.: Strict Intersection Types for the Lambda Calculus; a survey, 2011, Located at http://www.doc.ic.ac.uk/~svb/Research/.
• [2] Barendregt, H. P.: The Lambda Calculus: Its Syntax and Semantics., Revised edition, North-Holland, 1984, ISBN 0-444-88748-1 (hardback).
• [3] Barendregt, H. P., Coppo, M., Dezani-Ciancaglini, M.: A Filter Lambda Model and the Completness of Type Assignment., The Journal of Symbolic Logic, 48(4), 1983.
• [4] Böhm, C., Ed.: Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, March 25-27, 1975, vol. 37 of Lecture Notes in Computer Science, Springer, 1975, ISBN 3-540-07416-3.
• [5] Carlier, S., Polakow, J., Wells, J. B., Kfoury, A. J.: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types, ESOP (D. A. Schmidt, Ed.), 2986, Springer, 2004, ISBN 3-540-21313-9.
• [6] Carlier, S., Wells, J. B.: Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation, Electr. Notes Theor. Comput. Sci., 136, 2005, 173-202.
• [7] Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and λ-calculus semantic., in: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J.R. Hindley and J.P. Seldin, 1980, 535-560.
• [8] Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional Characters of Solvable Terms, Mathematische Logik Und Grundlagen der Mathematik, 27, 1981, 45-58.
• [9] Coquand, T.: Completeness Theorems and lambda-Calculus, TLCA (P. Urzyczyn, Ed.), 3461, Springer, 2005, ISBN 3-540-25593-1.
• [10] Dezani-Ciancaglini, M., Honsell, F., Alessi, F.: A complete characterization of complete intersection-type preorders, ACM Trans. Comput. Log., 4(1), 2003, 120-147.
• [11] Farkh, S., Nour, K.: Résultats de complétude pour des classes de types du système AF2, Theoretical Informatics and Applications, 31(6), 1998, 513-537.
• [12] Gallier, J. H.: On Girard's "Candidats de Reductibilité"., in: Logic and Computer Science (P. Odifreddi, Ed.), Academic Press, 1990, 123-203.
• [13] Gallier, J. H.: On the correspondence between proofs and λ-terms., Cahiers du centre de logique, 8, 1995, 55-138.
• [14] Gallier, J. H.: Proving Properties of Typed λ-Terms Using Realisability, Covers, and Sheaves., Theoretical Computer Science, 142(2), 1995, 299-368.
• [15] Gallier, J. H.: Typing Untyped λ-Terms, or Realisability strikes again!., Annals of Pure and Applied Logic, 91, 1998, 231-270.
• [16] Hindley, J. R.: The simple semantics for Coppo-Dezani-Sallé types., Symposium on Programming (M. Dezani-Ciancaglini, U. Montanari, Eds.), 137, Springer, 1982, ISBN 3-540-11494-7.
• [17] Hindley, J. R.: The Completeness Theorem for Typing lambda-Terms., Theor. Comput. Sci., 22, 1983, 1-17.
• [18] Hindley, J. R.: Curry's Types Are Complete with Respect to F-semantics Too, Theoretical Computer Science, 22, 1983, 127-133.
• [19] Hindley, J. R.: Basic Simple Type Theory, vol. 42 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1997.
• [20] Hindley, J. R., Longo, G.: Lambda-Calculus Models and Extensionality., Zeit. Math. Logik, 26, 1980, 289-310.
• [21] Kamareddine, F., Nour, K.: A completeness result for a realisability semantics for an intersection type system., Annals of Pure and Applied Logic, 146, 2007, 180-198.
• [22] Kamareddine, F., Nour, K., Rahli, V., Wells, J. B.: On Realisability Semantics for Intersection Types and Infinite Expansion Variables, 2008, Located at http://www.macs.hw.ac.uk/~fairouz/papers/drafts/long-fund-inf-sem.pdf.
• [23] Koletsos, G.: Church-Rosser Theorem for Typed Functional Systems., Journal of Symbolic Logic, 50(3), 1985, 782-790.
• [24] Krivine, J.-L.: Lambda-calcul, types et modèles., Masson, 1990.
• [25] Labib-Sami, R.: Typer avec (ou sans) types auxilières.
• [26] Oosten, J. V.: Realizability: a historical essay, Mathematical. Structures in Comp. Sci., 12(3), 2002, 239-263, ISSN 0960-1295.
• [27] Tait, W. W.: Intensional Interpretations of Functionals of Finite Type I., The Journal of Symbolic Logic, 32(2), 1967, 198-212.