Skip to main content
SpringerLink
Log in

Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 902))

Included in the following conference series:

Abstract

We propose a constructive termination proof in the Calculus of Constructions of any finite term rewriting systems whose rules can be oriented by the multiset path ordering. We propose a new proof which consists in an embedding of the rewrite relation into the standard ordering over natural numbers. Then, we show how to derive automatically constructive well-foundedness proofs of rewrite relations. This work has been completely formalised in the Coq system. Such a mechanization is not useless since there was some nontrivial mistakes in the previous proofs of Cichon and Weiermann. Furthermore this kind of development reflects the ability to formalise in Coq parts of nontrivial mathematics.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. A. Cichon. Bounds on derivation lenghts from termination proofs. Technical Report CSD-TR-622, Royal Holloway and Bedford New College, 1990.

    Google Scholar 

  2. E. A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N. Y., USA), volume 607 of Lecture Notes in Computer Science, pages 139–147. Springer-Verlag, June 1992.

    Google Scholar 

  3. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

    Article  Google Scholar 

  4. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant. User's guide, INRIA-CNRS-ENS, 1991.

    Google Scholar 

  5. N. Dershowitz and M. Okada. Proof-theoretic techniques and the theory of rewriting. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), pages 104–11. IEEE, 1988.

    Google Scholar 

  6. J. Gallier. What's so special about Kruskal's theorem and the ordinal Γ 0? A survey of some results in proof theory. Annals of Pure and Applied Logic, 53(3):199–261, September 1991.

    Article  Google Scholar 

  7. D. Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lenghts. In Hélène Kirchner and W. Wechler, editors, Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), volume 463 of Lecture Notes in Computer Science, pages 347–358, 1990.

    Google Scholar 

  8. C. Lautemann. A note on polynomial interpretation. Bulletin of European Association for Theoretical Computer Science, 1(36):129–131, October 1988.

    Google Scholar 

  9. P. Lescanne. On the recursive decomposition ordering with lexicographical status and other related orderings. Journal of Automated Reasoning, 6:39–49, 1990.

    Article  Google Scholar 

  10. Catherine Parent. Developing certified programs in the system coq-the program tactic. RR 93-29, ENS, October 1993.

    Google Scholar 

  11. C. Paulin-Mohring. Inductive Definitions in the System Coq — Rules and Properties. In Proceedings of the conference Typed Lambda Calculus and Applications, Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  12. Rathjen, M. and Weiermann A. Proof-theoretic investigations on kruskal's theorem. Annals of pure and applied logic, 60:49–88, 1993.

    Article  Google Scholar 

  13. Joseph Rouyer and Pierre Lescanne. Verification and programming of first-order unification in the calculus of constructions with inductive types, November 1992.

    Google Scholar 

  14. Joseph Rouyer. Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. RR 1795, INRIA, November 1992.

    Google Scholar 

  15. Andreas Weiermann. Bounds for derivation lengths from termination proofs with rpo and rlpo. Private communication, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lés-Nancy, France

    François Leclerc

Authors
  1. François Leclerc
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mariangiola Dezani-Ciancaglini Gordon Plotkin

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leclerc, F. (1995). Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014061

Download citation

  • DOI: https://doi.org/10.1007/BFb0014061

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59048-4

  • Online ISBN: 978-3-540-49178-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation