交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について

• Item type: Trans(1)
• 公開日: 2022-05-20
• タイトル: 交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について
• タイトル / 言語: en
• タイトル: On the Soundness of Unraveling for Join Conditional Rewriting Systems
• 言語: 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
• 著者名: 大野, 峻; 青戸, 等人
• 著者名(英): Shun, Ohno; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 等式論理に基づく計算モデルとして項書き換えシステム（TRS）がある．条件付き項書き換えシステム（CTRS）は条件部を持つ書き換え規則を扱えるようにTRSを拡張したものである．交差式CTRSは，条件部の判定に交差性を用いており，擬等式論理との対応と効率的な計算を両立できる体系となっている．CTRSからTRSへの変換法としてアンラベリング変換が知られている．変換において書き換えステップを保存する性質を健全性といい，アンラベリング変換が健全性を持つための条件がいくつか知られている．合流性は計算の解の一意性を保証する性質の1つであり，書き換えシステムの基本的な性質として知られている．このため合流性を保証するための様々な証明法が提案されているが，指向式CTRSに対する合流性証明法としてアンラベリング変換を用いて指向式CTRSの合流性をTRSの合流性に帰着する手法が知られている．一方，交差式CTRSについては同様の手法が可能かどうかは知られていない．アンラベリング変換を用いた合流性証明には通常の健全性だけではなく，項変換に関する健全性が必要となるが，これは指向式CTRSに対しては示されているが，交差式CTRSに対しては与えられていない．本発表では，交差式CTRSのアンラベリング変換における項変換tbに関する健全性について報告し，交差式CTRSに関してもアンラベリング変換を利用する合流性証明法が可能なことを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Term rewriting systems (TRSs) are a computational model based on the equational logic. Conditional term rewriting systems (CTRSs) are an extension of TRSs that handles rewrite rules with conditions. Join CTRSs, in which the conditions of rewrite rules are interpreted by the joinability, are a framework of CTRSs that achieves both efficient calculations and the correspondence with the quasi-equational logic. Unraveling is a transformation from CTRSs to TRSs. The transformation is said to be sound if it preserves rewrite steps, and some conditions for the soundness of unraveling are known. Confluence is a property that guarantees the uniqueness of computational results, and is known as a basic property of rewriting systems. Various proof methods have been proposed to guarantee the confluenceーone of such methods for oriented CTRSs to use unraveling to reduce confluence problems of oriented CTRSs to those of TRSs. On the other hand, it is not known whether a similar method is possible for join CTRSs. Proofs of confluence using unraveling require not only the usual soundness but also soundness w.r.t. a term transformation, which have been known for oriented CTRSs but not for join CTRSs. In this presentation, we report on the soundness of unraveling w.r.t. the term transformation ‘tb’ of join CTRSs, so that the confluence proof method using the unraveling is possible for join CTRSs.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 15, 号 2, p. 3-3, 発行日 2022-05-20
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会