Towards a Categorical Calculus for Critical-Pair/Completion

The ultimate aim of the research reported here is to provide a general framework for algorithms that show the following two characteristics: critical pairs and completion. Here completion means extending a certain set of reductions (given by, e.g., rewrite rules, or polynomials from an ideal) until that set fulfills some completeness property. Critical pairs are used for the selection of elements for which the reduction relation to be completed is not yet confluent. The selection is essentially done by superposing left hand sides of basic reduction rules, and testing whether applying the applicable reduction rules yield the same reducts. If not, one forces confluence by adding a reduction rule between the differing reducts (if possible without violating certain conditions on the reduction relation).