Completion of a Set of Rules Modulo a Set of Equations 论文

摘要

Church-Rosser properties are first presented, depending on an arbitrary relation R, an equivalence relation E and a reduction relation $R^E $ used to compute normal forms of R modulo E. Terminating rewriting systems operating on equational congruence classes of terms of a free algebra are then considered. In this framework, the Church–Rosser property is proved decidable for a very general reduction relation which may take into account the left-linearity of rules for efficiency reasons, under the only assumption of existence of a complete and finite unification algorithm for the underlying equational theory, whose congruence classes are assumed to be finite. This extends previous results by Lankford and Ballantyne, Peterson and Stickel, Huet, Jouannaud. A general completion procedure for mixed sets of rules and equations is then presented that generalizes and improves Peterson and Stickel’s one. In addition to computing a Church–Rosser set of rules when it terminates, it yields a semi-decision procedure for testing equality when it runs forever. Finally a post-processor is described that yields a Church–Rosser set of inter-reduced rules. All proofs, including the correctness proof of our completion algorithm, are based on the powerful proof technique of multiset induction.