
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Unreachability Proofs for β Rewriting Systems by Homomorphisms
Kiyoshi AKAMA Yoshinori SHIGETA Eiichi MIYAMOTO
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E82D
No.2
pp.339347 Publication Date: 1999/02/25
Online ISSN:
DOI:
Print ISSN: 09168532 Type of Manuscript: PAPER Category: Automata,Languages and Theory of Computing Keyword: β rewriting system, homomorphism, homomorphism theorem, unreachability,
Full Text: PDF>>
Summary:
Given two terms and their rewriting rules, an unreachability problem proves the nonexistence of a reduction sequence from one term to another. This paper formalizes a method for solving unreachability problems by abstraction; i. e. , reducing an original concrete unreachability problem to a simpler abstract unreachability problem to prove the unreachability of the original concrete problem if the abstract unreachability is proved. The class of rewriting systems discussed in this paper is called β rewriting systems. The class of β rewriting systems includes very important systems such as semiThue systems and Petri Nets. Abstract rewriting systems are also a subclass of β rewriting systems. A β rewriting system is defined on axiomatically formulated base structures, called β structures, which are used to formalize the concepts of "contexts" and "replacement," which are common to many rewritten objects. Each domain underlying semiThue systems, Petri Nets, and other rewriting systems are formalized by a β structure. A concept of homomorphisms from a β structure (a concrete domain) to a β structure (an abstract domain) is introduced. A homomorphism theorem (Theorem1)is established for β rewriting systems, which states that concrete reachability implies abstract reachability. An unreachability theorem (Corollary1) is also proved for β rewriting systems. It is the contraposition of the homomorphism theorem, i. e. , it says that abstract unreachability implies concrete unreachability. The unreachability theorem is used to solve two unreachability problems: a coffee bean puzzle and a checker board puzzle.

