On the complexity of recursive path orderings

DOI10.1016/0020-0190(93)90105-IMaRDI QIDQ685537zbMATH OpenOpenAlexFDO

Authors Wayne Snyder

Publication date 9 January 1994

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(93)90105-i

zbMATH Keywords

ground caseKnuth-Bendix procedurepath ordering

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

Review text

We give a fast method for generating reduced sets of rewrite rules equivalent to a given set of ground equations. Since reduced sets of ground rewrite rules are in fact canonical, this is an efficient Knuth- Bendix procedure for the ground case. The dominant cost of the algorithm is for congruence closure, so the method runs in \(O(n \log n)\) time and quadratic space, or in \(O(n(\log n)^ \land 2)\) time and linear space, where \(n\) is the number of occurrences of symbols in the original set of ground equations \(E\). We also show how our method provides a precise characterization of the (finite) collection of all reduced sets of rewrite rules equivalent to a given ground set of equations \(E\), and prove that our algorithm is complete in the sense that it can enumerate every member of this collection. Finally, we show that a modified version of this procedure can produce a reduced ground rewriting system contained in the lexicographic path ordering generated by a given total precedence ordering on the symbols of \(E\), still in a worst-case time of \(O(n \log n)\).

Recommendations

• Efficient ground completion
• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• scientific article; zbMATH DE number 58292
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Extensions and comparison of simplification orderings

Cites work

• scientific article; zbMATH DE number 3905845 (Why is no real title available?)
• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• On recursive path ordering
• Path of subterms ordering and recursive decomposition ordering revisited
• Proving refutational completeness of theorem-proving strategies
• Termination of rewriting

Cited in

(12)

• Algorithms and reductions for rewriting problems. II.
• The computability path ordering
• Polymorphic higher-order recursive path orderings
• scientific article; zbMATH DE number 3926235 (Why is no real title available?)
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Efficient ground completion
• The complexity of counting problems in equational matching
• Recursive Path Orderings Can Also Be Incremental
• A path order for rewrite systems that compute exponential time functions
• Combinatorial Algorithms for Listing Paths in Minimal Change Order
• Improving associative path orderings
• The number of depth-first searches of an ordered set

This page was built for publication: On the complexity of recursive path orderings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685537)