置換に関する不動点制約を用いた名目書き換え

• Item type: Trans(1)
• 公開日: 2022-05-20
• タイトル: 置換に関する不動点制約を用いた名目書き換え
• タイトル / 言語: en
• タイトル: Nominal Rewriting with Permutation Fixed Point Constraints
• 言語: 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
• 著者名: 芳賀, 雅樹; 青戸, 等人
• 著者名(英): Masaki, Haga; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 名目技法(Gabbay and Pitts, 2002)は項の変数束縛を形式的に取り扱うための枠組みの1つであり，アトムの非出現制約や置換といった仕組みを用いて項のα同値性を特徴付けている．名目書き換えシステム(Fernández et al., 2004)は名目技法に基づく高い表現力を備えた計算モデルであり，述語論理やλ計算を表すことができる一方で，高階の場合は決定不能だった項の単一化問題が決定可能となる．近年，非出現制約の代わりに置換に関する不動点制約を用いたα同値性の特徴付けが，Ayala-Rincón et al. (2020)によって提案されている．不動点制約を用いたα同値性は，名目項のC単一化に有用であることが知られている一方で，名目書き換えとの関連性はあまり調べられていない．本発表では，不動点制約に関する基本的な性質を示すとともに，不動点制約を用いた名目書き換えの枠組みを提案する．また，提案する名目書き換えが非出現制約に基づく名目書き換えの一般化になっていることなど，書き換えの基本的な性質を明らかにする．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The nominal-set approach (Gabbay and Pitts, 2002) is one of frameworks that formally treat variable bindings of terms; it characterizes the α-equivalence relation of terms using novel mechanisms such as freshness constraints of atoms and permutations. A nominal rewriting system (Fernández et al., 2004) is a model of computation based on the nominal-set approach with a high expressive powerーit is capable of representing predicate logic, λ-calculus and so onーwhile retaining decidability of nominal unification, which is contrast to other formalizms in which higher-order unification is undecidable. Recently, an axiomatization of the α-equivalence relation using permutation fixed point constraints in stead of freshness constraints has been proposed by Ayala-Rincón et al. (2020). While the axiomatization is known to be useful for C-unification of nominal terms, its usability and effectiveness in nominal rewriting have not been well studied. In this presentation, we report on fundamental properties of fixed point constraints and propose a framework of nominal rewriting based on fixed point constraints. We moreover clarify basic properties of the proposed framework of nominal rewriting; in particular, we show that our framework generalizes the traditional framework of nominal rewriting based on freshness constraints.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 15, 号 2, p. 2-2, 発行日 2022-05-20
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会