×

Automating the Knuth Bendix ordering. (English) Zbl 0715.68044

The paper describes an algorithm that automatically constructs a Knuth- Bendix ordering for a finite system of terms rewriting rules if one such exists. The algorithm is based on a practical and simple algorithm to solve systems of linear inequalities.
Reviewer: M.Jantzen

MSC:

68Q42 Grammars and rewriting systems
03D03 Thue and Post systems, etc.

Software:

REVE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bellegarde, F.: Rewriting systems of FP expressions to reduce the number sequences yielded. Sci. Comput. Program.6, 11-34 (1986) · Zbl 0613.68012 · doi:10.1016/0167-6423(86)90017-1
[2] Boyer, R.S., Moore, J.S.: A computational logic. New York: Academic Press 1979 · Zbl 0448.68020
[3] Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.9, 137-160 (1987) · Zbl 0625.68036 · doi:10.1016/0167-6423(87)90030-X
[4] Chvatal, V.: Linear programming. New York: Freeman 1983 · Zbl 0318.05002
[5] Dershowitz, N.: Orderings for term rewriting systems. Theor. Comp. Sci.17, 279-301 (1982) · Zbl 0525.68054 · doi:10.1016/0304-3975(82)90026-3
[6] Dershowitz, N.: Termination of rewriting. J. Symbol. Comput.3, 69-116 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[7] Forgaard, R., Detlefs, D.: A procedure for automatically proving the termination of a set of rewrite rules. Proceedings of the First International Conference on Rewriting Techniques and Applications. (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985 · Zbl 0576.68013
[8] Dick, A.J.J.: ERIL ? Equational reasoning: an interactive laboratory. Rutherford Appleton Laboratory Report RAL-86-010, March 1985
[9] Dick, A.J.J., Kalmus J.R.: ERIL (Equational reasoning: an interactive laboratory). User’s manual. Version R1.6, Rutherford Appleton Laboratory Report RAL-88-055, September 1988
[10] Feferman, S.: Systems of predicative analysis II: Representation of ordinals. J. Symbol. Logic33, 193-220 (1968) · Zbl 0162.02201 · doi:10.2307/2269866
[11] Gale, D.: The theory of linear economic models. New York: McGraw Hill 1960 · Zbl 0114.12203
[12] Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. Ass. Comp. Mach.27(4) 797-821 (1980), preliminary version in 18th Symposium on Foundations of Computer Science, IEEE, 1977 · Zbl 0458.68007
[13] Huet, G., Lankford, D.S.: On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, March 1978
[14] Higman, G.: Ordering by divisibility in abstract algebras. Proc LMS(3)2, 326-336 (1952) · Zbl 0047.03402
[15] Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R. (ed.), Formal language theory, perspectives and open problems, pp. 349-405. New York: Academic Press 1980
[16] Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational problems in abstract algebra, pp. 263-297. New York: Pergamon Press 1970 · Zbl 0188.04902
[17] Kreko, B.: Linear programming. London: Pitman 1968 · Zbl 0103.10202
[18] Lankford, D.S.: Canonical algebraic simplification in computational logic. Mem ATP-25. Automatic Theorem Proving Project. University of Texas, Austin TX, May 1975
[19] Lescanne, P.: Computer experiments with the REVE term rewriting system generator, Proc 10th ACM POPL symposium, Austin, TX 1983, pp. 99-108
[20] Lescanne, P.: Divergence of the Knuth Bendix completion procedure and termination orderings. Bull. Eur. Assoc. Theoret. Comput. Sci.30, 80-83 (1986) · Zbl 1023.68595
[21] Lescanne, P.: Private communication
[22] Manna, Z., Ness, S.: On the termination of Markov algorithms. Proceedings of the Third Hawaii International Conference on System Science, Honolulu, HI, January 1970, pp. 789-792
[23] Martin, U.: How to choose the weights in the Knuth Bendix ordering. Proceedings of the Second International Conference on Rewriting Techniques and Applications (RTA 87), Bordeaux, France, May 1987. (Lect. Notes Comput. Sci., vol. 256, pp. 42-53) Berlin Heidelberg New York: Springer 1987 · Zbl 0638.68108
[24] O’Donnell, M.J.: Computing in systems described by equations (Lect Notes Comput. Sci., vol. 58) Berlin Heidelberg New York: Springer 1977
[25] Rusinowitch, M.: Plaisted ordering and recursive decomposition ordering revisited. Proceedings of the First International Conference on Rewriting Techniques and Applications. (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985 · Zbl 0576.68016
[26] Uzawa, H.: An elementary method for linear programming. In: Arrow, K.J., Hurwicz, L., Uzawa, H. (eds.) Studies in linear and non-linear programming, pp. 179-188. Stanford: Stanford University Press 1958 · Zbl 0091.16002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.