Algorithm to Test for Confluence in a System of Left to Right Rewrite Rules

摘要

Formal specifications of computation systems promise to afford us not only a strictly enforced discipline in describing the semantics of the system, but also a way of proving that the system functions as described. There exists a rich body of mathematical theory regarding the use of formal specifications. However, the bridge from the theoretical world to the practical world is nonexistent in most cases. This research concentrates on developing practical techniques to determine the correctness of a formal specification. The foundation for the specifications we describe is in abstract algebras. However, the view of the axioms for a specification is modified so that axioms are treated as left to right rewrite rules, rather than as mathematical equalities. The major result of the research is a new and practical algorithm to determine confluence in an axiom system of left to right rewrite rules that satisfy certain restrictions.