外部変数のある可換式条件付き項書き換えシステムの合流性条件

• Item type: Trans(1)
• 公開日: 2021-05-12
• タイトル: 外部変数のある可換式条件付き項書き換えシステムの合流性条件
• タイトル / 言語: en
• タイトル: Confluence Criteria for Semi-Equational Conditional Term Rewriting Systems with Extra Variables
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: 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
• 著者名: 笹川, 葵生; 青戸, 等人
• 著者名(英): Aoi, Sasagawa; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 項書き換えシステム（TRS）は等式論理に基づく計算モデルである．合流性は，計算解の一意性を保証するTRSの重要な性質である．このため合流性の様々な判定条件や十分条件が知られている．条件付き項書き換えシステム（CTRS）は条件付きの書き換え規則を扱えるようにしたTRSの拡張である．CTRSは条件部の解釈によっていくつかの方式が知られている．条件部を可換性によって解釈する場合を可換式CTRSとよぶ．可換式CTRSの合流性については，外山と大山口(2001)によるLR分離CTRSの危険対条件や，青戸と外山(2019)による外部変数を持たない可換式CTRSの危険対条件が知られているが，それ以外は従来ほとんど報告されていない．本研究では，まず青戸と外山(2019)の証明を拡張することによって，条件部に外部変数が含まれる可換式CTRSの合流性を保証する危険対条件を与える．次に，外部変数が条件部だけでなく右辺にも含まれる可換式CTRSに対して合流性を保証する手法を与える．これらの結果を用いて合流性を従来保証することができなかった可換式CTRSの合流性を示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Term rewriting systems (TRSs) are a model of computation based on equational logic. Confluence is an important property of TRSs that ensures unique results of computations. Thus, various criteria and sufficient conditions for confluence have been studied. Conditional term rewriting systems (CTRSs) are extensions of the framework of TRSs that allow to deal with conditional rewriting rules. Several models are known for CTRSs depending on the interpretation of the conditional part of the rewrite rules. CTRSs in which conditional parts are interpreted by conversion are called semi-equational CTRSs. Only few criteria for confluence of semi-equational CTRSs are known-one is a critical pairs criterion for LR-separated CTRSs by Toyama and Oyamaguchi (2001) and the others are critical pairs criteria for semi-equational CTRS without extra variables by Aoto and Toyama (2019). In this presentation, we first extend the proof of Aoto and Toyama (2019) to give a critical pairs criterion that ensures confluence for semi-equational CTRS that may have extra variables in the conditional part. Then, we give a method to ensure confluence of semi-equational CTRSs that may have extra variables not only in the conditional parts but also in the right hand sides of the rewrite rules. Based on our results, we show the confluence of a semi-equational CTRS for which no known criteria can be applied.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 2, p. 29-29, 発行日 2021-05-12
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会