Abstract
In this paper we present a generalization of the Knuth-Bendix procedure for generating a complete set of reductions modulo an equational theory. Previous such completion procedures have been restricted to equational theories which generate finite congruence classes. The distinguishing feature of this work is that we are able to generate complete sets of reductions for some equational theories which generate infinite congruence classes. In particular, we are able to handle the class of equational theories which contain the associative, commutative, and identity laws for one or more operators.
We first generalize the notion of rewriting modulo an equational theory to include a special form of conditional reduction. We are able to show that this conditional rewriting relation restores the finite termination property which is often lost when rewriting in the presence of infinite congruence classes. We then develop Church-Rosser tests based on the conditional rewriting relation and set forth a completion procedure incorporating these tests. Finally, we describe a computer program which implements the theory and give the results of several experiments using the program.
Recommended Citation
Baird, Timothy B. and Wilkerson, Ralph W., "Complete Sets of Reductions Modulo A Class of Equational Theories which Generate Infinite Congruence Classes" (1988). Computer Science Technical Reports. 88.
https://scholarsmine.mst.edu/comsci_techreports/88
Department(s)
Computer Science
Keywords and Phrases
Complete Sets of Reductions; Knuth-Bendix Procedure; E-Completion; E-Unification; Conditional Reductions; Finite Termination Property; Church-Rosser Property
Report Number
CSc-88-5
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1988 University of Missouri--Rolla, All rights reserved.
Publication Date
July 1988
Comments
This report is substantially the Ph.D. dissertation of the first author, completed, July 1988.