フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性

• Item type: Trans(1)
• 公開日: 2021-05-12
• タイトル: フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性
• タイトル / 言語: en
• タイトル: Undecidability of Some Properties Related to the Uniqueness of Normal Forms for Flat Term Rewiting Systems
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] 項書き換えシステム，一意正規形性，決定不能性
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者名: 佐藤, 悠稀; 青戸, 等人
• 著者名(英): Yuki, Sato; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 項書き換えシステム（TRS）は等式論理に基づく計算モデルである．TRSの計算による正規形の一意性を保証する性質として，合流性（CR），可換に関する一意正規形性（UNC），簡約に関する一意正規形性（UNR），正規形性（NFP）が知られている．これらの4つの性質は等価でなく，CR⇒NFP⇒UNC⇒UNRという関係がある．TRSの性質の決定可能性については，従来いろいろな結果が知られており，たとえば左線形右基底TRSに対してはこれらの4つの性質がすべて決定可能であることが知られている．また，すべての書き換え規則の高さがたかだか1であるTRSをフラットTRSとよぶ．フラットTRSに対しては，CRが決定不能（三橋ら，2006），UNCが決定可能（Radcliffeら，2017），UNRが決定不能（Godoyら，2009）ということがすでに知られているが，NFPについては決定可能か決定不能かは未解決な問題であった．本論文ではフラットTRSに対するNFPが決定不能であることを報告する．具体的には，三橋らのCRの決定不能性の証明を拡張し，ポストの対応問題をフラットTRSに対するNFPに帰着することで，NFPの決定不能性を証明する．また，同様に三橋らのCRの決定不能性の証明を拡張することにより，既存の方法とは異なる方法でUNRの決定不能性を証明する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Term rewriting systems (TRSs) are a computational model based on equational logic. Some properties that guarantee the uniqueness of normal forms for computations of TRSs are known: confluence (CR), uniqueness of normal forms with respect to conversions (UNC), uniqueness of normal forms with respect to reductions (UNR), and the normal form property (NFP). These four properties are mutually inequivalent, and the following relation holds: CR⇒NFP⇒UNC⇒UNR. Various results are known about the (un)decidability of the properties of TRSs. In particular, it is known that these four properties are decidable for left-linear and right-ground TRSs. TRSs in which the height of each rewriting rule is at most 1 are called flat TRSs. For flat TRSs, it is already known that CR is undecidable (Mitsuhashi et al., 2006), UNC is decidable (Radcliffe et al., 2017) and UNR is undecidable (Godoy et al., 2009); however, it is not known whether NFP is decidable or undecidable. In this paper, we show that NFP is undecidable for flat TRSs. To be exact, we extend the proof of the undecidability of CR by Mitsuhashi et al. (2006), and prove the undecidability of NFP for flat TRSs by reducing the PCP (Post Correspondence Problem) to it. Similarly, we give a new proof of the undecidability of UNR for flat TRSs by extending the proof of undecidability of CR by Mitsuhashi et al. (2006).
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 2, p. 15-24, 発行日 2021-05-12
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会