永続性を利用した項書き換えシステムの一意正規形性の検証

• Item type: Trans(1)
• 公開日: 2023-06-29
• タイトル: 永続性を利用した項書き換えシステムの一意正規形性の検証
• タイトル / 言語: en
• タイトル: Proving Unique Normal Forms w.r.t. Conversion of Term Rewriting Systems based on Persistency
• 言語: 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
• 著者名: 渡邉, 廉; 青戸, 等人
• 著者名(英): Ren, Watanabe; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 項書き換えシステム（TRS）は，等式論理に基づく計算モデルである．TRSの計算は，項を最も単純な形（正規形）に書き換えることで実現される．TRSは非決定的な計算機構を持つ計算モデルであり，計算結果が1つに決まるとは限らない．このため，計算解の一意性を保証することは，TRS分野の重要な研究課題の1つとなっている．TRSの計算解の一意性を保証する性質の1つに，一意正規形性（UNC）がある．TRSの同様の性質の1つである合流性については，これまで合流性を保証する様々な十分条件が考案されている．一方，UNCについては，それほど多くの十分条件は知られていない．本発表では，永続性に基づく項書き換えシステムの合流性証明(鈴木ら，2012)を参考に，UNCの検証手法を検討する．合流性と同様に，UNCについても永続性が成り立つことが知られている．鈴木らの手法では，既存の合流性条件を用いて非線形型変数を具体化した型付きシステムの合流性を示すことで，永続性を使って元のシステムの合流性を示す．UNCにおいても非線形型変数を具体化した型付きシステムのUNCから，元のシステムのUNCが得られる．しかし，合流性の場合と異なり，既存のUNC条件を適用することは難しい．そのため，既存のUNC条件を適用するための更なる変換を提案し，提案手法を適用するための条件を与える．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Term rewriting systems (TRSs) are a computational model based on equational logic. The computation of TRSs is achieved by rewriting terms to their normal forms. The computation of TRSs is non-deterministic, and terms may not have unique normal forms, and thus, how to guarantee the uniqueness of normal forms is one of the important research topics in term rewriting. Unique normal forms w.r.t. conversion (UNC) is one of the properties that guarantee the uniqueness of normal forms. For confluence, which is another property of TRSs guaranteeing uniqueness of normal forms, many sufficient criteria have been known. On the other hand, only little criteria have been obtained for UNC. In this presentation, we consider a method for proving UNC, inspired from the method for proving confluence based on persistency (Suzuki et al., 2012). Confluence, as well as UNC, is known to be persistent. Based on persistency, (Suzuki et al., 2012) obtains a confluence criterion by showing confluence of typed systems obtained by instantiating variables of non-linear types, using existing other confluence criteria. Similarly, one can obtain UNC of TRSs from that of typed systems. In contrast to the case of confluence, however, existing UNC criteria are difficult to apply. Thus, we propose a further translation to apply existing UNC criteria, and give a condition to apply the proposed method.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 16, 号 2, p. 31-31, 発行日 2023-06-29
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会