The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Étant donnés deux termes et leurs règles de réécriture, un problème d'inaccessibilité prouve l'inexistence d'une séquence de réduction d'un terme à un autre. Cet article formalise une méthode pour résoudre les problèmes d'inaccessibilité par abstraction ; c'est-à-dire réduire un problème d'inaccessibilité concret original à un problème d'inaccessibilité abstrait plus simple pour prouver l'inaccessibilité du problème concret original si l'inaccessibilité abstraite est prouvée. La classe de systèmes de réécriture discutée dans cet article est appelée systèmes de réécriture β. La classe des systèmes de réécriture β comprend des systèmes très importants tels que les systèmes semi-Thue et les réseaux de Petri. Les systèmes de réécriture abstraite sont également une sous-classe des systèmes de réécriture β. Un système de réécriture β est défini sur des structures de base formulées axiomatiquement, appelées structures β, qui sont utilisées pour formaliser les concepts de « contextes » et de « remplacement », communs à de nombreux objets réécrits. Chaque domaine sous-jacent aux systèmes semi-Thue, aux réseaux de Petri et à d'autres systèmes de réécriture est formalisé par une structure β. Un concept d'homomorphismes d'une structure β (un domaine concret) à une structure β (un domaine abstrait) est introduit. Un théorème d'homomorphisme (Théorème 1) est établi pour les systèmes de réécriture β, qui stipule que l'accessibilité concrète implique l'accessibilité abstraite. Un théorème d'inaccessibilité (Corollaire 1) est également prouvé pour les systèmes de réécriture β. C'est la contraposition du théorème d'homomorphisme, c'est-à-dire qu'il dit que l'inaccessibilité abstraite implique l'inaccessibilité concrète. Le théorème d’inaccessibilité est utilisé pour résoudre deux problèmes d’inaccessibilité : un casse-tête en forme de grain de café et un casse-tête en damier.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Kiyoshi AKAMA, Yoshinori SHIGETA, Eiichi MIYAMOTO, "Unreachability Proofs for β Rewriting Systems by Homomorphisms" in IEICE TRANSACTIONS on Information,
vol. E82-D, no. 2, pp. 339-347, February 1999, doi: .
Abstract: 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 (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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e82-d_2_339/_p
Copier
@ARTICLE{e82-d_2_339,
author={Kiyoshi AKAMA, Yoshinori SHIGETA, Eiichi MIYAMOTO, },
journal={IEICE TRANSACTIONS on Information},
title={Unreachability Proofs for β Rewriting Systems by Homomorphisms},
year={1999},
volume={E82-D},
number={2},
pages={339-347},
abstract={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 (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.},
keywords={},
doi={},
ISSN={},
month={February},}
Copier
TY - JOUR
TI - Unreachability Proofs for β Rewriting Systems by Homomorphisms
T2 - IEICE TRANSACTIONS on Information
SP - 339
EP - 347
AU - Kiyoshi AKAMA
AU - Yoshinori SHIGETA
AU - Eiichi MIYAMOTO
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E82-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 1999
AB - 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 (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.
ER -