Advertisement

Termination of a Set of Rules Modulo a Set of Equations

  • Jean-Pierre Jouannaud
  • Miguel Munoz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

Abstract

The problem of termination of a set R of rules modulo a set E of equations, called E-termination problem, arises when trying to complete the set of rules in order to get a Church-Rosser property for the rules modulo the equations. We first show here that termination of the rewriting relation and E-termination are the same whenever the used rewriting relation is E-commuting, a property inspired from Peterson and Stickel’s E-compatibility property. More precisely, their results can be obtained by requiring termination of the rewriting relation instead of E-termination if E-commutation is used instead of E-compatibility. When the rewriting relation is not E-commuting, we show how to reduce E-termination for the starting set of rules to classical termination of the rewriting relation of an extended set of rules that has the E-commutation property. This set can be classicaly constructed by computing critical pairs or extended pairs between rules and equations, according to the used rewriting relation. In addition we show that different orderings can be used for the starting set of rules and the added critical or extended pairs. Interesting issues for further research are also discussed.

Keywords

Normal Form Function Symbol Reduction Ordering Critical Pair Left Member 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Choque 83]
    Choque, G. Calcul d’un ensemble complet d’incrementations minimales pour l’ordre recursif de decomposition. Technical Report, CRIN, Nancy, France, 1983.Google Scholar
  2. [Dershowitz 82]
    Dershowitz, N. Ordering for Term-rewriting Systems. Journal of Theoretical Computer Science 17(3):279–301, 1982. Preliminary version in 20th FOCS, 1979.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [Dershowitz, Hsiang, Josephson and Plaisted 83]
    Dershowitz, N., Hsiang, J., Josephson, N. and Plaisted, D. Associate-Commutative Rewriting. Proceedings 10th IJCAI, 1983.Google Scholar
  4. [Huet 80]
    Huet, G. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journal of the Association for Computing Machinery 27:797–821, 1980. Preliminary version in 18th FOCS, IEEE, 1977.MathSciNetCrossRefzbMATHGoogle Scholar
  5. [Huet and Oppen 80]
    Huet, G. and Oppen, D. Equations and Rewrite Rules: A Survey. In Book, R. (editor), Formal Language Theory: Perspectives and Open Problems,. Academic Press, 1980.Google Scholar
  6. [Jouannaud 83]
    Jouannaud, J.P. Church-Rosser Computations with Equational Term Rewriting Systems. Technical Report, CRIN, Nancy, France, January, 1983. Preliminary version in Proc. 5th CAAP, 1983, to appear in Springer Lecture Notes in Computer Science.Google Scholar
  7. [Jouannaud and Kirchner 84]
    Jouannaud, J.P. and Kirchner, H. Completion of a set of rules modulo a set of Equations. Technical Report, SRI-International, 1984. Preliminary version in Proceedings 11th ACM POPL Conference, Salt Lake City, 1984, submitted to the SIAM Journal of Computing.Google Scholar
  8. [Jouannaud and Lescanne 82]
    Jouannaud, J.P., Lescanne, P. On Multiset Ordering. Information Processing letters 15(2), 1982.Google Scholar
  9. [Jouannaud, Kirchner C. and H. 81]
    Jouannaud, J.P., Kirchner, C. and Kirchner, H. Algebraic manipulations as a unification and matching strategy for equations in signed binary trees. Proceedings 7th International Joint Conference on Artificial Intelligence, Vancouver, 1981.Google Scholar
  10. [Jouannaud, Lescanne and Reinig 83]
    Jouannaud, J.-P., Lescanne, P., Reinig, F. Recursive Decomposition Ordering. In IFIP Working Conference on Formal Description of Programming Concepts II,. North-Holland, 1983, edited by D. Bjorner., 1983.Google Scholar
  11. [Kamin and Levy 80]
    Kamin, S. and Levy, J.J. Attempts for generalizing the recursive path ordering. 1980. Unpublished draft.Google Scholar
  12. [Kirchner C. and H. 82]
    Kirchner, C. and Kirchner, H. Resolution d’ equations dans les Algebres libres et les varietes equationelles d’Algebres. PhD thesis, Universite Nancy I, 1982.Google Scholar
  13. [Knuth and Bendix 70]
    Knuth, D. and Bendix, P. Simple Word Problems in Universal Algebra. In J. Leech (editor), Computational Problems in Abstract Algebra,. Pergamon Press, 1970.Google Scholar
  14. [Lankford and Ballantyne 77a]
    Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  15. [Lankford and Ballantyne 77b]
    Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  16. [Lankford and Ballantyne 77c]
    Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.Google Scholar
  17. [Lescanne 83]
    Lescanne P. Computer Experiments with the REVE Term Rewriting Systems Generator. In Proceedings, 10th POPL,. ACM, 1983.Google Scholar
  18. [Lescanne 84]
    Lescanne, P. How to prove termination? An approach to the implementation of a new Recursive Decomposition Ordering. Proceedings 6th CAAP, Bordeaux, 1984.Google Scholar
  19. [Manna and Ness 70]
    Manna, Z. and Ness, N. On the Termination of Markov Algorithms. Proceedings of the third Hawaii Conference on System Sciences, 1970.Google Scholar
  20. [Munoz 83]
    Munoz, M. Probleme de terminaison finie des systemes de reecriture equationnels. PhD thesis, Universite Nancy 1, 1983.Google Scholar
  21. [Peterson and Stickel 81]
    Peterson, G. and Stickel, M. Complete Sets of Reductions for Some Equational Theories. JACM 28:233–264, 1981.MathSciNetCrossRefzbMATHGoogle Scholar
  22. [Plaisted 78]
    Plaisted, D. A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems. Technical Report R-78-943, University of Illinois, Computer Science Department, 1978.Google Scholar
  23. [Plaisted 83]
    Plaisted, D. An associative path ordering. Technical Report, University of Illinois, Computer Science Department, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Jean-Pierre Jouannaud
    • 1
  • Miguel Munoz
    • 2
  1. 1.Centre de Recherche en Informatique de NANCY and GRECO ProgrammationVandoeuvre les Nancy CEDEXFrance
  2. 2.Universidad de ValenciaBurjasotSpain

Personalised recommendations