Definitions by Rewriting in the Calculus of Constructions

Computing Research Repository, no. 1 (2006): 9-9

Cited by: 90|Views122
EI

Abstract

Abstract: The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prove the strong normalization of the reduction relation generated by the β-rule and the user-defined rules under some general syntactic conditions including conflue...More

Code:

Data:

0
Introduction
  • This work aims at defining an expressive language allowing to specify and prove mathematical properties in which functions and predicates can be defined by rewrite rules, enabling the automatic proof of equational problems.

    The Calculus of Constructions.
  • The main contribution of the work is a strong normalization result for the Calculus of Constructions extended with, at the predicatelevel, user-defined rewrite rules satisfying some general admissibility conditions.
  • The authors assume given a set R of rewrite rules defining the symbols in F .
Highlights
  • This work aims at defining an expressive language allowing to specify and prove mathematical properties in which functions and predicates can be defined by rewrite rules, enabling the automatic proof of equational problems.

    The Calculus of Constructions
  • Following Martin-Lof’s theory of types [24], Coquand and Paulin-Mohring defined an extension of CC with inductive types and their associated induction principles as first-class objects : the Calculus of Inductive Constructions (CIC) [26] which is the basis of the proof-assistant Coq [17]
  • The main contribution of our work is a strong normalization result for the Calculus of Constructions extended with, at the predicatelevel, user-defined rewrite rules satisfying some general admissibility conditions. We show that these conditions are satisfied by a sub-system of CIC with strong elimination [26] and the Natural Deduction Modulo [13] a large class of equational theories
  • We can define simplification rules on propositions that are not definable in CIC
  • We consider general syntactic conditions, including confluence, that ensure the strong normalization of the calculus. These conditions are fulfilled by two important systems : a sub-system of the Calculus of Inductive Constructions which is the basis of the proof assistant Coq [17], and the Natural Deduction Modulo [12, 13] a large class of equational theories
Results
  • The symbols 0 : int, s : int → int, p : int → int, + : int → int → int and × : int → int → int defined by the rules s(p(x)) → x, p(s(x)) → x and others for + and × are all constructors of the type int of integers.
  • The constructors of primitive predicates, defined by usual first-order rules, are shown to be strongly normalizing since the combination of first-order rewriting with →β preserves strong normalization [8].
  • The authors present an extension of the General Schema defined in [5] to deal with type-level rewriting, the main novelty of the paper.
  • The General Schema is based on Tait and Girard’s computability predicate technique [19] for proving the strong normalization of the -typed λ-calculus and system F.
  • The simplicity condition in (A3) extends to the case of rewriting the restriction in CIC of strong elimination to “small” inductive types, that is, to the types whose constructors have no predicate-arguments except the parameters of the type.
  • The main difficulty is to define an interpretation for predicate symbols that is invariant by reduction, a condition required by the type conversion rule.
  • When a predicate symbol is defined by a rule whose right-hand side contains quantifiers, its combination with β may not preserve normalization.
  • The authors require that left-hand sides are made of free symbols and that at most one rule can apply at the top of a term.
Conclusion
  • As a combination of the two previous applications, the work shows that the extension of CIC− with userdefined rewrite rules, even at the predicate-level, is sound if these rules follow the admissibility conditions.
  • These conditions are fulfilled by two important systems : a sub-system of the Calculus of Inductive Constructions which is the basis of the proof assistant Coq [17], and the Natural Deduction Modulo [12, 13] a large class of equational theories.
  • The authors expect to extend this work with rewriting modulo some useful equational theories like associativity and commutativity, and by allowing η-reductions in the type conversion rule.
Reference
  • F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalization in the algebraic-λcube. Journal of Functional Programming, 7(6):613– 660, 1997.
    Google ScholarLocate open access versionFindings
  • H. Barendregt. Lambda calculi with types. In S. Abramski, D. Gabbay, and T. Maibaum, editors, Handbook of logic in computer science, volume Oxford University Press, 1992.
    Google ScholarLocate open access versionFindings
  • F. Blanqui. Termination and confluence of higherorder rewrite systems. In Proc. of RTA’00, LNCS 1833.
    Google ScholarLocate open access versionFindings
  • F. Blanqui. Theorie des Types et Reecriture (Type Theory and Rewriting). PhD thesis, Universite Paris-Sud (France), 2001. Available at http://www.lri.fr/~blanqui. An english version will be available soon.
    Findings
  • F. Blanqui, J.-P. Jouannaud, and M. Okada. The Calculus of Algebraic Constructions. In Proc. of RTA’99, LNCS 1631.
    Google ScholarLocate open access versionFindings
  • F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-data-type systems. Theoretical Computer Science, 277, 2001.
    Google ScholarLocate open access versionFindings
  • V. Breazu-Tannen. Combining algebra and higherorder types. In Proc. of LICS’88, IEEE Computer Society.
    Google ScholarLocate open access versionFindings
  • V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 83(1):3–28, 1991.
    Google ScholarLocate open access versionFindings
  • T. Coquand and J. Gallier. A proof of strong normalization for the Theory of Constructions using a Kripke-like interpretation, 1990. Paper presented at the 1st Int. Work. on Logical Frameworks but not published in the proceedings. Available at ftp://ftp.cis.upenn.edu/pub/papers/ gallier/sntoc.dvi.Z.
    Google ScholarLocate open access versionFindings
  • T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2–3):95–120, 1988.
    Google ScholarLocate open access versionFindings
  • N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6. NorthHolland, 1990.
    Google ScholarLocate open access versionFindings
  • G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Technical Report 3400, INRIA Rocquencourt (France), 1998.
    Google ScholarFindings
  • G. Dowek and B. Werner. Proof normalization modulo. In Proc. of TYPES’98, LNCS 1657.
    Google ScholarLocate open access versionFindings
  • G. Dowek and B. Werner. An inconsistent theory modulo defined by a confluent and terminating rewrite system, 2000. Available at http://pauillac.inria.fr/~dowek/.
    Findings
  • C. Kirchner et al. ELAN, 2000. Available at http://elan.loria.fr/.
    Locate open access versionFindings
  • C. Marche et al. CiME, 2000. Available at http://www.lri.fr/~demons/cime.html.
    Locate open access versionFindings
  • C. Paulin et al. The Coq Proof Assistant Reference Manual Version 6.3.1. INRIA Rocquencourt (France), 2000. Available at http://coq.inria.fr/.
    Findings
  • H. Geuvers, R. Nederpelt, and R. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. NorthHolland, 1994.
    Google ScholarLocate open access versionFindings
  • J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1988.
    Google ScholarFindings
  • J. Hsiang. Refutational theorem proving using termrewriting systems. Artificial Intelligence, 25:255–300, 1985.
    Google ScholarLocate open access versionFindings
  • J.-P. Jouannaud and M. Okada. Abstract Data Type Systems. Theoretical Computer Science, 173(2):349– 391, 1997.
    Google ScholarLocate open access versionFindings
  • J.-P. Jouannaud and A. Rubio. The Higher-Order Recursive Path Ordering. In Proc. of LICS’99, IEEE Computer Society.
    Google ScholarLocate open access versionFindings
  • J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121:279–308, 1993.
    Google ScholarLocate open access versionFindings
  • P. Martin-Lof. Intuitionistic type theory. Bibliopolis, Napoli, Italy, 1984.
    Google ScholarFindings
  • N. P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, United States, 1987.
    Google ScholarFindings
  • [27] M. Stefanova. Properties of Typing Systems. PhD thesis, Nijmegen University (Netherlands), 1998.
    Google ScholarFindings
  • [28] J. van de Pol. Termination of higher-order rewrite systems. PhD thesis, University of Utrecht, Nederlands, 1994.
    Google ScholarFindings
  • [29] V. van Oostrom. Confluence for Abstract and HigherOrder Rewriting. PhD thesis, Vrije Universiteit, Netherlands, 1994.
    Google ScholarFindings
  • [31] B. Werner. Une Theorie des Constructions Inductives. PhD thesis, Universite Paris VII, France, 1994.
    Google ScholarFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科