We 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. in Particular, We Are Able to Handle the Class of Collapse Equational Theories Which Contain Associative, Commutative, and Identity Laws for One or More Operators.
T. B. Baird and R. W. Wilkerson, "Termination Via Conditional Reductions," CSC 1991 - Proceedings of the 19th Annual Conference on Computer Science, pp. 53 - 60, Association for Computing Machinery, Apr 1991.
The definitive version is available at https://doi.org/10.1145/327164.327207
International Standard Book Number (ISBN)
Article - Conference proceedings
© 2023 Association for Computing Machinery, All rights reserved.
01 Apr 1991