Unreachability Proofs for β 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 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 semi-Thue 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 semi-Thue 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 (Theorem 1) is established for β rewriting systems, which states that concrete reachability implies abstract reachability. An unreachability theorem (Corollary 1) 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.
社団法人電子情報通信学会の論文
1999-02-25

Unreachability Proofs for β Rewriting Systems by Homomorphisms

スポンサーリンク

概要

著者

関連論文

スポンサーリンク