About the confluence of equational pattern rewrite systems

  • Alexandre Boudet
  • Evelyne Contejean
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


We study the confluence of higher-order pattern rewrite systems modulo an equational theory E. This problem has been investigated by Mayr and Nipkow [13], for the case of rewriting modulo a congruence à la Huet [8]. The case we address here is rewriting using matching modulo E as done in the first-order case by Jouannaud and Kirchner [10].

The theory is then applied to the case of AC-theories, for which we provided a complete unification algorithm in [1]. It happens that the AC-unifiers may have to be constrained by some flexible-flexible equations of the form λx 1 ... λx n .F(x 1,...,x n ) = λx 1 ... λx n F(x π(1),...,x π(n)), where F is a free variable and π a permutation. This situation requires a slight technical adaptation of the theory.


Induction Hypothesis Free Variable Equational Theory Critical Pair Local Coherence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alexandre Boudet and Evelyne Contejean. AC-unification of higher-order patterns. In Gert Smolka, editor, Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 267–281, Linz, Austria, October 1997. Springer-Verlag.Google Scholar
  2. 2.
    Val Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.Google Scholar
  3. 3.
    Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.Google Scholar
  4. 4.
    Gilles Dowek. Third order matching is decidable. In Proc. 7th IEEE Symp. Logic in Computer Science, Santa Cruz, pages 2–10. IEEE Comp. Society Press, 1992.Google Scholar
  5. 5.
    Warren D. Goldfarb. Note on the undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    R. Hindley and J. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.Google Scholar
  7. 7.
    Gérard Huet. Résolution d'équations dans les langages d'ordre 1,2, ... Ω. Thèse d'Etat, Univ. Paris 7, 1976.Google Scholar
  8. 8.
    Gérard Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, October 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23:11–21, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4), November 1986.Google Scholar
  11. 11.
    Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.Google Scholar
  12. 12.
    Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, February 1998.CrossRefMathSciNetGoogle Scholar
  14. 14.
    D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming. LNCS 475, Springer Verlag, 1991.Google Scholar
  15. 15.
    M. H. A. Newman. On theories with a combinatorial definition of ‘equivalence'. Ann. Math., 43(2):223–243, 1942.zbMATHCrossRefGoogle Scholar
  16. 16.
    T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.Google Scholar
  17. 17.
    Vincent Padovani. Filtrage d'ordre supérieur. PhD thesis, Université de Paris VII, 1996.Google Scholar
  18. 18.
    Zhenyu Qian and Kang Wang. Modular AC-Unification of Higher-Order Patterns. In Jean-Pierre Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 105–120, München, Germany, September 1994. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Alexandre Boudet
    • 1
  • Evelyne Contejean
    • 1
  1. 1.LRI, CNRS URA 410Universit Paris-Sud, Centre d'OrsayOrsay CedexFrance

Personalised recommendations