Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems

Pierre Lescanne

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (1982)

  • Volume: 16, Issue: 4, page 331-347
  • ISSN: 0988-3754

How to cite

top

Lescanne, Pierre. "Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 16.4 (1982): 331-347. <http://eudml.org/doc/92169>.

@article{Lescanne1982,
author = {Lescanne, Pierre},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {term rewriting systems; equational theories; recursive path ordering; decomposition ordering; termination; left-weighted terms; recursive lexicographic ordering},
language = {eng},
number = {4},
pages = {331-347},
publisher = {EDP-Sciences},
title = {Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems},
url = {http://eudml.org/doc/92169},
volume = {16},
year = {1982},
}

TY - JOUR
AU - Lescanne, Pierre
TI - Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 1982
PB - EDP-Sciences
VL - 16
IS - 4
SP - 331
EP - 347
LA - eng
KW - term rewriting systems; equational theories; recursive path ordering; decomposition ordering; termination; left-weighted terms; recursive lexicographic ordering
UR - http://eudml.org/doc/92169
ER -

References

top
  1. 1. N. DERSHOWITZ, Ordering for Term Rewriting Systems, Proc. 20th Symposium on Foundations of Computer Science, 1979, pp. 123-131, also in Theoritical Computer Science, Vol. 17, 1982, pp. 279-301. Zbl0525.68054MR648438
  2. 2. N. DERSHOWITZ, A note on Simplification Orderings, Inform. Proc. Ltrs., Vol. 9, 1979, pp. 212-215. Zbl0433.68044MR552535
  3. 3. J. FRANÇON, G. VIENNOT and J. VUILLEMIN, Description and Analysis of an Efficient Priority Queues Representation, Proc. 19th Symposium of Foundations of Computer Science, 1978, pp. 1-7. MR539825
  4. 4. G. HUET, A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm, Rapport INRIA 25, 1980. Zbl0465.68014MR636177
  5. 5. G. HUET and J. HULLOT, Proof by Induction in Equational Theories with Constructors, Proc. 21th Symposium on Foundations of Computer Science, 1980. Zbl0532.68041
  6. 6. G. HUET and D. C. OPPEN, Equations and Rewrite Rules: a Survey, in Formal Languages perspectives and Open Problems, R. BOOK, Ed., Academic Press, 1980. 
  7. 7. D. E. KNUTH, The Art of Computer Programming. Vol. 1: Fundamental Algorithms, Addison Wesley, Reading, Mass., 1968. Zbl0191.17903MR378456
  8. 8. D. E. KNUTH and P. BENDIX, Simple Word Problems in Universal Algebra, in Computational Problems in Abstract Algebra, J. LEECH, Ed., Pergamon Press, 1970, pp. 263-297. Zbl0188.04902MR255472
  9. 9. J. B. KRUSKAL, Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture, Trans. Amer. Math. Soc., Vol. 95, 1960, pp. 210-225. Zbl0158.27002MR111704
  10. 10. P. LESCANNE, Two Implementations of the Recursive Path Ordering on Monadic Terms, 19th Annual Allerton Conf. on Communication, Control, and Computing, Allerton House, Monticello, Illinois, 1981. 
  11. 11. P. LESCANNE, Decomposition Ordering as a Tool to prove the Termination of Rewriting Systems, 7th IJCAI, Vancouver, Canada, 1981, pp. 548-550. 
  12. 12. P. LESCANNE and F. REINIG, A Well-Founded Recursively Defined Ordering on First Order Terms, Centre de Recherche en Informatique de Nancy, France, CRIN 80-R-005. 
  13. 13. D. L. MUSSER, On Proving Inductive Properties of Abstract Data Types, Proc. 7th ACM Symposium on Principles of Programming Languages, 1980. 
  14. 14. C. St. J. A. NASH-WILLIAM, On Well-Quasi-Ordering on Finite Trees, Proc. Cambridge Philos. Soc., Vol. 60, 1964, pp. 833-835. Zbl0122.25001MR153601
  15. 15. D. PLAISTED, Well-Founded Orderings for Proving Termination of Systems of Rewrite Rules, Dept of Computer Science Report 78-932, U. of Illinois at Urbana-Champaign, July 1978. 
  16. 16. D. PLAISTED, A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems, Dept of Computer Science Report 78-943, U. of Illinois at Urbana-Champaign, Sept. 1978. 
  17. 17. F. REINIG, Les ordres de décomposition: un outil incrémental pour prouver la terminaison finie de systèmes de réécriture de termes, Thèse, Université de Nancy, 1981. 
  18. 18. J.-P. JOUANNAUD and P. LESCANNE, On Multiset Orderings, in Inform. Proc. Ltrs., Vol. 15, 1982, pp. 57-63. Zbl0486.68041MR675869
  19. 19. J.-P. JOUANNAUD, P. LESCANNE and F. REINIG, Recursive Decomposition Ordering, IFIP Conf. on Formal Description of Programming Concepts, Garmisch-Partenkirchen, Germany, 1982. Zbl0513.68026MR787625

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.