Unreachability proofs for beta rewriting systems by homomorphisms

Given two terms and their rewriting rules, an unreachability problem proves the non-existence of a reduction sequence from one term to another. This p aper formalizes a method for solving unreachability problems by abstraction ; i.e., reducing an original concrete unreachability problem to a simpler a bstract unreachability problem to prove the unreachability of the original concrete problem if the abstract unreachability is proved. The class of rew riting systems discussed in this paper is called beta rewriting systems. Th e class of beta rewriting systems includes very important systems such as s emi-Thue systems and Petri Nets. Abstract rewriting systems are also a subc lass of beta rewriting systems. A beta rewriting system is defined on axiom atically formulated base structures, called beta structures, which are used to formalize the concepts of "contexts" and "replacement," which are commo n to many rewritten objects. Each domain underlying semi-Thue systems, Petr i Nets, and other rewriting systems are formalized by a beta structure. A c oncept of homomorphisms from a beta structure (a concrete domain) to a beta structure (an abstract domain) is introduced. A homomorphism theorem (Theo rem 1) is established for beta rewriting systems, which states that concret e reachability implies abstract reachability. An unreachability theorem (Co rollary 1) is also proved for beta rewriting systems. It is the contraposit ion of the homomorphism theorem, i.e., it says that abstract unreachability implies concrete unreachability. The unreachability theorem is used to sol ve two unreachability problems: a coffee bean puzzle and a checker board pu zzle.