λ項を用いた抽象ナローイングとその完全性
スポンサーリンク
概要
- 論文の詳細を見る
本稿は抽象的なナローイングを定式化し, その完全性を論じるものである. もともと一階の等式の求解法として提案されたナローイングは関数・論理型プログラミング言語の基礎として発展し, 現在では高階項書き換え系を用いた高階の項におけるナローイングや, グラフ書き換え系を用いたナローイングも提案されている. 前者はHaskelやMLのような高階関数を扱う機能を持つ言語の, 後者は遅延評価機構の計算機上への実装のモデル化に適している. これらのナローイングに共通する最も重要な理論的性質は求解完全性であるが, その証明はそれぞれの定式化の枠組みで別個に行わざるをえなかった. そこで我々は, これらのナローイングを統一的に扱える抽象的な枠組みを提供し, 種々のナローイングの求解完全性を簡潔に示すことを目指す. 我々の定式化はvan Oostromによる高階項書き換え系を用いる. この定式化で特徴的なのは, 代入をλ項上の計算として抽象化している点である. 本稿では, ナローイングをこのように定式化することで, 求解完全性の証明が従来のものと比べはるかに簡潔で見通し良くなることを示す. また一階のナローイングをこの枠組みでモデル化することで, 抽象ナローイングにおける求解完全性から一階のナローイングの求解完全性を導けることを示す. Nipkowによる高階項書き換え系に基づくナローイングに対しても同様のことが示せると予想される.
- 一般社団法人情報処理学会の論文
- 2001-07-15
著者
関連論文
- 遅延ナローイング抽象機械
- 関数・論理型言語のためのナローイング計算系
- 遅延ナローイング抽象機械のシミュレータ
- 遅延ナローイング抽象機械のアーキテクチャ
- 遅延ナローイング計算系に基づく言語Evとその処理系
- Context capturing in XML document processing based on regular tree pattern matching
- プロジェクト進捗状況 Brzozowski Derivatives and Top-Down Regular Tree Pattern Matching
- A Rewrite System with Incomplete Regular Expression Type for Transformation of XML Documents
- 抽象高階書換え系におけるナローイング
- λ項を用いた抽象ナローイングとその完全性
- 遅延ナローイングに基づく言語Evの等式翻訳方法