Pure patterns type systems

ABSTRACT

We introduce a new framework of algebraic pure type systems in which we consider rewrite rules as lambda terms with patterns and rewrite rule application as abstraction application with built-in matching facilities. This framework, that we call "Pure Pattern Type Systems", is particularly well-suited for the foundations of programming (meta)languages and proof assistants since it provides in a fully unified setting higher-order capabilities and pattern matching ability together with powerful type systems. We prove some standard properties like confluence and subject reduction for the case of a syntactic theory and under a syntactical restriction over the shape of patterns. We also conjecture the strong normalization of typable terms. This work should be seen as a contribution to a formal connection between logics and rewriting, and a step towards new proof engines based on the Curry-Howard isomorphism.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: Franco Barbanera , Maribel Fernández , Herman Geuvers, Modularity of strong normalization in the algebraic-λ-cube, Journal of Functional Programming, v.7 n.6, p.613-660, November 1997 [doi>10.1017/S095679689700289X]
• 3: H. Barendregt. Lambda Calculus: its Syntax and Semantics. North Holland, 1984.
• 4: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 5: Henk Barendregt , Herman Geuvers, Proof-assistants using dependent type systems, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 6: G. Barthe and T. Coquand. An Introduction to Dependent Type Theory. In Proc. of Applied Semantics Summer School, volume 2395 of LNCS. Springer-Verlag, 2002.
• 7: F. Blanqui. Type Theory and Rewriting. PhD thesis, Université de Paris-Sud, 2001.
• 8: H. Cirstea and C. Kirchner. The Rewriting Calculus --- Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427--498, 2001.
• 9: Horatiu Cirstea , Claude Kirchner , Luigi Liquori, Matching Power, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.77-92, May 22-24, 2001
• 10: Horatiu Cirstea , Claude Kirchner , Luigi Liquori, The Rho Cube, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.168-183, April 02-06, 2001
• 11: H. Cirstea, C. Kirchner, and L. Liquori. Rewriting Calculus with(out) Types. In Proc. of WRLA, volume 71 of ENTCS, 2002.
• 12: T. Coquand. Pattern Matching with Dependent Types. In Proc. of Logical Frameworks, pages 66--79, 1992.
• 13: G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via Explicit Substitutions: The Case of Higher-Order Patterns. In Proc. of JICSLP. MIT Press, 1996.
• 14: Germain Faure , Claude Kirchner, Exceptions in the Rewriting Calculus, Proceedings of the 13th International Conference on Rewriting Techniques and Applications, p.66-82, July 22-24, 2002
• 15: H. Geuvers and M.J. Nederhof. A Modular Proof of Strong Normalisation for the Calculus of Constructions. Journal of Functional Programming, 1(2):155--189, 1991.
• 16: G. Huet. Résolution d'Equations dans les Langages d'Ordre 1,2, ...,ω. Thèse de Doctorat d'Etat, Université de Paris 7, 1976.
• 17: Jean-Pierre Jouannaud , Mitsuhiro Okada, Abstract data type systems, Theoretical Computer Science, v.173 n.2, p.349-391, February 28, 1997 [doi>10.1016/S0304-3975(96)00161-2]
• 18: Delia Kesner , Laurence Puel, A typed pattern calculus, Information and Computation, v.124 n.1, p.32-61, Jan. 10, 1996 [doi>10.1006/inco.1996.0004]
• 19: J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, 1980. PhD Thesis.
• 20: Jan Willem Klop , Vincent van Oostrom , Femke van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, v.121 n.1-2, p.279-308, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90091-7]
• 21: Dale Miller, A logic programming language with Lambda-abstraction, function variables, and simple unification, Proceedings of the international workshop on Extensions of logic programming, p.253-281, February 1991, Tu¨bingen, Germany
• 22: D. Miller, G. Nadathur, F. Pfenning, and A. Shedrov. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logics, 51(1-2):125--157, 1991.
• 23: T. Nipkow and C. Prehofer. Higher-order Rewriting and Equational Reasoning. In Automated Deduction --- A Basis for Applications. Volume I: Foundations. Kluwer, 1998.
• 24: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 25: S.L. Peyton Jones and E. Meijer. Henk: a Typed Intermediate Language. In Types in Compilation Workshop, 1997.
• 26: C. Schürmann. Automating the Meta-Theory of Deductive Systems. Phd thesis, Carnegie-Mellon University, 2000.
• 27: Masako Takahashi, Parallel reductions in &lgr;-calculus, Journal of Symbolic Computation, v.7 n.2, p.113-123, Feb. 1989 [doi>10.1016/S0747-7171(89)80045-8]
• 28: S. van Bakel, L. Liquori, S. Ronchi della Rocca, and P. Urzyczyn. Comparing Cubes of Typed and Type Assignment System. Annals of Pure and Applied Logics, 86(3):267--303, 1997.
• 29: V. van Oostrom. Lambda Calculus with Patterns. Technical Report IR-228, Faculteit der Wiskunde en Informatica, Vrije Universiteit Amsterdam, 1990.
• 30: D. A. Wolfram, The clausal theory of types, Cambridge University Press, New York, NY, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages; Constraint and logic languages

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming; Mechanical theorem proving; Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
Curry-Howard, Lambda-calculus, logics, matching, patterns, pure type systems, rewriting