The Algebra of Expansion

• Autorzy: Carlier S. , Wells J. B.
• Języki publikacji: EN

Abstrakty

EN

Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a l-term in systems with intersection types. This paper aims to clarify expansion and make it more accessible to a wider community by isolating the pure notion of expansion on its own, independent of type systems and types, and thereby make it easier for non-specialists to obtain type inference with flexible precision by making use of theory and techniques that were originally developed for intersection types. We redefine expansion as a simple algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple axioms and axiom schemas: the 3 standard axioms of a monoid, 4 standard axioms or axiom schemas of substitutions (including one that corresponds to the usual "substitution lemma" that composes substitutions), and 1 very simple axiom schema for expansion itself. Many of the results on the algebra have also been formally checked with the Coq proof assistant. We then take System E, a λ-calculus type system with intersection types and expansion variables, and redefine it using the expansion algebra, thereby demonstrating how a single uniform notion of expansion can operate on both typings and proofs. Because we present a simplified version of System E omitting many features, this may be independently useful for those seeking an easier-tocomprehend version.

Słowa kluczowe

EN

expansion algebra; canonical form; sorted expansion algebra

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

Twórcy

autor

Carlier S.

autor

Wells J. B.

• Heriot-Watt University, School of Mathematical and Computing Sciences Edinburgh, Scotland http://www.macs.hw.ac.uk/~jbw/

Bibliografia

• [1] Baader, F., Nipkow, T.: Term Rewriting and All That, Cambridge University Press, 1998.
• [2] van Bakel, S., Barbanera, F., Fern´andez,M.: Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and β-Rule, Types for Proofs and Programs, Int'lWorkshop TYPES '99, vol. 1956 of LNCS, Springer-Verlag, 2000.
• [3] van Bakel, S. J.: Principal Type Schemes for the Strict Type Assignment System, J. Logic Comput., 3(6), December 1993, 643-670.
• [4] van Bakel, S. J.: Intersection Type Assignment Systems, Theoret. Comput. Sci., 151(2), 27 November 1995, 385-435.
• [5] Barendregt, H. P.: The Lambda Calculus: Its Syntax and Semantics, Revised edition, North-Holland, 1984.
• [6] Boudol, G., Zimmer, P.: On type inference in the intersection type discipline, in: ITRS '04 [13].
• [7] Carlier, S.: Polar Type Inference with Intersection Types and ω, Proceedings of the 2nd Workshop on Intersection Types and Related Systems, 2003, The ITRS '02 proceedings appears as vol. 70, issue 1 of Elec. Notes in Theoret. Comp. Sci., 2003-02.
• [8] 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, Programming Languages & Systems, 13th European Symp. Programming, vol. 2986 of LNCS, Springer-Verlag, 2004.
• [9] Carlier, S., Wells, J. B.: Type Inference with Expansion Variables and Intersection Types in System E and an Exact Correspondence with β-Reduction, Proc. 6th Int'l Conf. Principles & Practice Declarative Programming, 2004.
• [10] Carlier, S., Wells, J. B.: Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation, in: ITRS '04 [13], 173-202.
• [11] Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal Type Schemes and λ-Calculus Semantics, in: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism (J. R. Hindley, J. P. Seldin, Eds.), Academic Press, 1980, 535-560.
• [12] Dunfield, J.: A Unified System of Type Refinements, Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA, 2007.
• [13] Proc. 3rd Int'lWorkshop Intersection Types& Related Systems (ITRS 2004), 2005, The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci.
• [14] Kamareddine, F., Nour, K., Rahli, V.,Wells, J. B.: A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables, Theoretical Aspects of Computing - ICTAC 2008, 5th Int'l Colloq., vol. 5160 of LNCS, Springer-Verlag, September 2008.
• [15] Kamareddine, F., Nour, K., Rahli, V., Wells, J. B.: Realisability Semantics for Intersection Types and Expansion Variables, 4th Workshop on Intersection Types & Related Systems (ITRS 2008), Torino, Italia, March 2008.
• [16] Kfoury, A. J.: Beta-Reduction as Unification, in: Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference, December 1996), Banach Center Publication, Volume 46 (D. Niwinski, Ed.), Springer-Verlag, 1999, 137-158.
• [17] Kfoury, A. J., Wells, J. B.: Principality and Decidable Type Inference for Finite-Rank Intersection Types, Conf. Rec. POPL '99: 26th ACM Symp. Princ. of Prog. Langs., 1999, Superseded by [19].
• [18] Kfoury, A. J.,Wells, J. B.: Principality and Type Inference for Intersection Types Using Expansion Variables, August 2003, Supersedes [17]. Available from author's web page.
• [19] Kfoury, A. J.,Wells, J. B.: Principality and Type Inference for Intersection Types Using Expansion Variables, Theoret. Comput. Sci., 311(1-3), 2004, 1-70, Supersedes [17]. For omitted proofs, see the longer report [18].
• [20] Kobayashi, N.: Model-Checking Higher-Order Functions, Proc. 11th Int'l Conf. Principles & Practice Declarative Programming, ACM Press, 2009.
• [21] Kobayashi, N.: A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes, Foundations Softw. Sci. & Comput. Structures, FoSSaCS 2011, vol. 6604 of LNCS, Springer-Verlag, 2011.
• [22] Kobayashi, N., Ong, C.-H. L.: A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Schemes, Proc. 24th Ann. IEEE Symp. Logic in Comput. Sci., IEEE Comput. Soc. Press, 2009.
• [23] Lenglet, S., Wells, J. B.: Expansion for Universal Quantifiers, Programming Languages & Systems, 21st European Symp. Programming, vol. 7211 of LNCS, Springer-Verlag, 2012.
• [24] Ronchi Della Rocca, S.: Principal Type Schemes and Unification for Intersection Type Discipline, Theoret. Comput. Sci., 59(1-2),March 1988, 181-209.
• [25] RonchiDella Rocca, S., Venneri, B.: Principal Type Schemes for an Extended Type Theory, Theoret. Comput. Sci., 28(1-2), January 1984, 151-169.
• [26] Terauchi, T.: Dependent Types from Counterexamples, Proc. 37th Symp. Principles of Programming Languages, ACM Press, 2010.
• [27] Wells, J. B.: The Essence of Principal Typings, Proc. 29th Int'l Coll. Automata, Languages, and Programming, vol. 2380 of LNCS, Springer-Verlag, 2002.