×

The Church-Rosser property for ground term-rewriting systems is decidable. (English) Zbl 0641.68044

The paper proves the decidabilty of the Church-Rosser property (i.e. confluency) for any ground term-rewriting system (i.e. term rewriting system with rules not containing any variables), even if the system is not noetherian (i.e. it may contain infinite chains of reductions). While the noetherian property has been known to be decidable for ground term- rewriting systems, the problem solved in this paper has been an open problem for several years.
Several technical notions are introduced for the purpose of the proof: For the analysis of reduction sequences, pattern trees and stable pattern trees are defined and their properties studied. A restricted notion of confluency, the k-restricted confluency, is considered, for which it is shown that the confluency problem can be reduced to the k-restricted confluency problem for some \(k>0\). The proof of the decidability of the confluency problem for ground term-rewriting systems is concluded by reducing k-restricted confluency to the equivalence problem for nondeterministic root-to-root automata (already shown to be decidable by Thatcher).
Reviewer: J.Zlatuska

MSC:

68Q65 Abstract data types; algebraic specification
20M05 Free semigroups, generators and relations, word problems
68Q45 Formal languages and automata
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
08A50 Word problems (aspects of algebraic structures)
20M35 Semigroups in automata theory, linguistics, etc.
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Dershowitz, N., Termination of linear rewriting systems, (Even, S.; Kariv, O., Lecture Notes in Computer Science, 115 (1981), Springer: Springer New York), 448-458
[2] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. Assoc. Comput. Mach., 22, 465-476 (1979) · Zbl 0431.68016
[3] Guttag, J. V.; Kapur, D.; Musser, D., On proving uniform termination and restricted termination of rewriting systems, SIAM J. Comput., 12, 189-214 (1983) · Zbl 0526.68036
[4] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach., 27, 797-821 (1980) · Zbl 0458.68007
[5] Huet, G.; Lankford, D., On the uniform halting problem for term rewriting systems, (Rapport Laboria 283 (1978), IRIA: IRIA Paris)
[6] Huet, G.; Levy, J.-J., Call by need computations in non-ambiguous linear term rewriting systems, (Rapport Laboria 359 (1979), IRIA: IRIA Paris)
[7] Huet, G.; Oppen, C., Equations and rewrite rules: a survey, (Book, R. V., Formal Language Theory: Perspectives and Open Problems (1980), Academic Press: Academic Press New York), 349-393
[8] Jouannaud, J. P.; Kirchner, H.; Remy, J. L., Church-Rosser properties of weakly terminating term rewriting systems, 10th Internat. Joint Conf. on Artificial Intelligence (1983)
[9] Knuth, D.; Bendix, P., Simple word problems in universal algebra, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon Press: Pergamon Press Elmsford, NY), 263-297 · Zbl 0188.04902
[10] Nelson, G.; Oppen, D. C., Fast decision procedures based on congruence closure, J. Assoc. Comput. Mach., 27, 356-364 (1980) · Zbl 0441.68111
[11] Perdix, H., Proprietés Church-Rosser de systèmes de reécriture equationnels ayant la proprieté de terminaison faible, (Lecture Notes in Computer Science, 166 (1984), Springer: Springer Berlin), 97-107 · Zbl 0583.68005
[12] Rosen, B. K., Tree-manipulating systems and Church-Rosser theorems, J. Assoc. Comput. Mach., 20, 160-187 (1973) · Zbl 0267.68013
[13] Thatcher, J. W., Tree automata: an informal survey, (Aho, A. V., Currents in the Theory of Computing (1973), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 143-172
[14] Togashi, A.; Noguchi, S., Some decision problems and their time complexity for term rewriting systems, Trans. IECE Japan, J66-D, 1177-1184 (1983)
[15] Toyama, Y., On commutativity of term rewriting systems, Trans. IECE Japan, J66-D, 1370-1375 (1983)
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.