An algorithm for finding a minimal recursive path ordering
Aït-Kaci, Hassan
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 19 (1985), p. 359-382 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 1985-01-01
@article{ITA_1985__19_4_359_0,
     author = {A\"\i t-Kaci, Hassan},
     title = {An algorithm for finding a minimal recursive path ordering},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {19},
     year = {1985},
     pages = {359-382},
     mrnumber = {827483},
     zbl = {0578.68029},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_1985__19_4_359_0}
}

Aït-Kaci, Hassan. An algorithm for finding a minimal recursive path ordering. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 19 (1985) pp. 359-382. http://gdmltest.u-ga.fr/item/ITA_1985__19_4_359_0/

[ADJ78] J. A. Goguen, J. W. Thatcher and E. G. Wagner, An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, Current Trends in Programming Methodology, in R. T. YEH Ed., V. 4, Prentice Hall, 1978.

[DER 82] (a) N. Dershowitz, Orderings for Term-Rewriting Systems, Theor. Comp. Sc., Vol. 17, (3), pp. 279-301; | MR 648438 | Zbl 0525.68054

(b) N. Dershowitz, Computing with Rewrite Systems, Technical Paper Draft, Bar-Ilan University, August 1982.

[DRM79] N. Dershowitz and Z. Manna, Proving Termination with Multiset Ordering, Communications of the A.C.M., Vol. 22, (8), 1979, pp. 465-476. | MR 540043 | Zbl 0431.68016

[GOT79] J. A. Goguen and J. J. Tardo, An Introduction to OBJ: a Language for Writing and Testing Formal Algebraic Program Specifications, Proceedings of the I.E.E.E. Conference on Specifications of Reliable Software, Cambridge, MA, 1979, pp. 170-189.

[GOR65] S. Gorn, Explicit Definitions and linguistic Dominoes, in Systems and Computer Science, J. HART, S. TAKASU Eds., University of Toronto Press, 1965. | MR 237245

[HOD82] C. M. Hoffman and M. O'Donnell, Programming with Equations, A.C.M. Transactions on Programming Languages and Systems, Vol. 4, (1), 1982, pp. 83-112. | Zbl 0481.68008

[HOP80] G. Huet and D. C. Oppen, Equations and Rewrite Rules, in Formal Language Theory, Perspective and Open Problems, R. BOOK Ed., Academic Press, 1980, pp. 349-393.

[HUE81] G. Huet, A Complete Proof of Correctness of the Knuth-Bendix Algorithm, J.C.S.S., Vol. 23,(1), 1981, pp. 11-21. | MR 636177 | Zbl 0465.68014

[JLR83] J. P. Jouannaud, P. Lescanne and F. Reinig, Recursive Decomposition Ordering, in I.F.I.P. Working Conference on Formal Description of Programming Concepts II, D. BJORNER Ed., North-Holland, 1983. | MR 787625 | Zbl 0513.68026

[JOL82] J. P. Jouannaud and P. Lescanne, On Multiset Ordering, Inf. Proc. Lett., Vol. 15, (2), 1982. | MR 675869 | Zbl 0486.68041

[LES82] P. Lescanne, Some Properties of Decomposition Path Ordering, a Simplification Ordering to Prove Termination of Rewriting Systems, R.A.I.R.O., Informatique Theorique, Vol. 16, 1982, pp. 331-347. | Numdam | MR 707635 | Zbl 0518.68025

[LES83] (a) P. Lescanne, How to Prove Termination? An Approach to the Implementation of a New Recursive Decomposition Ordering, Technical Report, Centre de Recherche en Informatique de Nancy, Nancy, France, July 1983;

(b) P. Lescanne, Computer Experiments with the REVE Rewriting System Generator, in Proceedings of the 10th POPL Symposium, 1983.

[KNB70] 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. | MR 255472 | Zbl 0188.04902

[MUS79] D. R. Musser, Abstract Data Types Specification in the AFFIRM System, Proceedings of the I.E.E.E. Conference on Specifications of Reliable Software, Cambridge, Ma., 1979, pp. 45-57.

[ODN78] M. O'Donnell, Computing in Systems Described by Equations, Lecture Notes in Computer Science, Vol. 58, Springer-Verlag, 1978. | MR 483644 | Zbl 0421.68038

[PLT78] D. Plaisted, A Recursively Defined Ordering for Proving Termination of Term-Rewriting Systems, Report R-78-943, Department of Computer Science, University of Illinois, Urbana, III., 1978.

[PTS81] G. E. Peterson and M. E. Stickel, Complete Sets of Reductions for some Equational Theories, J.A.C.M., Vol. 28, (2), 1981, pp. 233-264. | MR 612079 | Zbl 0479.68092

[ROS73] B. K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, J.A.C.M., Vol. 20, (1), 1973, pp. 160-187. | MR 331850 | Zbl 0267.68013