On the complexity of recursive path orderings
type: Item
instance of: scholarly article
title: On the complexity of recursive path orderings
zbMATH Open document ID: 0778.68045
DOI: 10.1016/0020-0190(93)90105-I
author: Wayne Snyder
published in: Information Processing Letters
publication date: 1994-01-09T00:00:00Z
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)\).
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 417428
zbMATH Keywords: Knuth-Bendix procedure
zbMATH Keywords: ground case
zbMATH Keywords: path ordering
MaRDI profile type: Publication
cites work: Q4091421
cites work: Q4264723
cites work: Termination of rewriting
cites work: Q4385532
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Q3683533
cites work: On recursive path ordering
cites work: Path of subterms ordering and recursive decomposition ordering revisited
full work available at URL: 0020-0190(93)90105-i
OpenAlex ID: W2041678518
description: scientific article; zbMATH DE number 417428