λ項を用いた抽象ナローイングとその完全性

• Item type: Trans(1)
• 公開日: 2001-07-15
• タイトル: λ項を用いた抽象ナローイングとその完全性
• タイトル / 言語: en
• タイトル: Completeness of Abstract Narrowing with Lambda Terms
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 三重大学
• 著者所属: 東北大学
• 著者所属(英): en
• 著者所属(英): Mie University
• 著者所属(英): en
• 著者所属(英): Tohoku University
• 著者名: 奥居, 哲; 鈴木, 太朗
• 著者名(英): Satoshi, Okui; Taro, Suzuki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿は抽象的なナローイングを定式化し，その完全性を論じるものである．もともと一階の等式の求解法として提案されたナローイングは関数・論理型プログラミング言語の基礎として発展し，現在では高階項書き換え系を用いた高階の項におけるナローイングや，グラフ書き換え系を用いたナローイングも提案されている．前者はHaskelやMLのような高階関数を扱う機能を持つ言語の，後者は遅延評価機構の計算機上への実装のモデル化に適している．これらのナローイングに共通する最も重要な理論的性質は求解完全性であるが，その証明はそれぞれの定式化の枠組みで別個に行わざるをえなかった．そこで我々は，これらのナローイングを統一的に扱える抽象的な枠組みを提供し，種々のナローイングの求解完全性を簡潔に示すことを目指す．我々の定式化はvan Oostromによる高階項書き換え系を用いる．この定式化で特徴的なのは，代入を $ｴlambda$ 項上の計算として抽象化している点である．本稿では，ナローイングをこのように定式化することで，求解完全性の証明が従来のものと比べはるかに簡潔で見通し良くなることを示す．また一階のナローイングをこの枠組みでモデル化することで，抽象ナローイングにおける求解完全性から一階のナローイングの求解完全性を導けることを示す．Nipkowによる高階項書き換え系に基づくナローイングに対しても同様のことが示せると予想される．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper we propose an abstract form of narrowing and show its completeness. Narrowing has originally been a method for solving first-order equations. Now it is extended to the solving of higher-order or term graph equations. Due to their apparent difference, completeness, the most important theoretical property of narrowing, of these narrowing methods has been proved independently. Our goal is to propose a unified framework for narrowing and to show completeness of various narrowing concisely in this framework. Our formulation is based on higher-order rewriting a la van Oostrom. Here, substitution is performed by means of so-called substitution calculus, an operation on lambda terms. This yields a simple and clear completeness proof of the abstract narrowing. We present a rigorous proof of completeness and show that completeness of conventional first-order narrowing is an instance of the above completeness result.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 42, 号 SIG07(PRO11), p. 90-90, 発行日 2001-07-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会