明示的なα変換を用いたα単一化

• Item type: Trans(1)
• 公開日: 2010-12-10
• タイトル: 明示的なα変換を用いたα単一化
• タイトル / 言語: en
• タイトル: α Unification with Explicit α Conversion
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 慶應義塾大学理工学部情報工学科
• 著者所属: 慶應義塾大学理工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Science, Keio University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Science, Keio University
• 著者名: 山口, 文彦; 斎藤, 博昭
• 著者名(英): Fumihiko, Yamaguchi; Hiroaki, Saito
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 単一化は，述語を持つ論理系の上で自動推論を行う際の基本操作である．従来，構文的等価性という，最も強い等価性に基づいた単一化が多く用いられてきたが，より弱い等価性に基づいた単一化を用いることで，系の表現力の向上や，推論ステップ数の減少が期待できる．そのような単一化を言語処理系に用いた例として，Urbanらのλ Prologがある．λ Prologでは，項の表現として，変数を束縛することを許し，束縛変数の名前の違いを無視するα等価性に基づいた単一化を用いている．しかし，彼らの用いた単一化アルゴリズムNominal Unificationでは，項F，F'，Gについて，FとGが単一化可能でFとF'がα等価であるとき，F'とGが単一化不能になる場合がある．本発表では，単一化の操作として，α変換を明示的に返すような単一化アルゴリズムを提案する．また，提案アルゴリズムが，FとGを単一化するならば，Fとα等価なすべての項F'について，F'とGを単一化することを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Unification is the basic operation of automated reasoning on some predicate logic. Popular unification algorithms are based on the strongest equality i.e. syntactical equality. Unification based on weaker equality will empower the expression of the system and will decrease the step of reasoning. λ Prolog is an instance of such reasoning applied to programming language. In λ Prolog, bound variable can be expressed and unification method named nominal unification, which is based on α equality, is used. However, nominal unification has following problem: when terms F and G are unifiable, F and F' are α equivalent, but F' and G are not always unifiable. In this presentation, an unification algorithm, which returns α conversions explicitly, is proposed. And it will be shown that any term F' which is α equivalent to F is also unifiable with G, under the condition that F and G are unifiable.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 3, 号 5, p. 32-32, 発行日 2010-12-10
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会