結合子項を用いた高階単一化アルゴリズム

• 研究課題/領域番号: 09878056
• 研究種目: 萌芽的研究
• 配分区分: 補助金
• 研究分野: 計算機科学
• 研究機関: 筑波大学
• 研究代表者: 坂井 公 筑波大学, 数学系, 助教授 (20241797)
• 研究分担者: 塚田 信高 筑波大学, 数学系, 助手 (50015559) ; 塩谷 真弘 筑波大学, 数学系, 助手 (30251028) ; 西村 泰一 筑波大学, 数学系, 講師 (70135614) ; 本橋 信義 筑波大学, 数学系, 教授 (70015874) ; 杉浦 成昭 筑波大学, 数学系, 教授 (20033805)
• 研究期間 (年度): 1997
• 研究課題ステータス: 完了 (1997年度)
• 配分額: 1,200千円 (直接経費: 1,200千円); 1997年度: 1,200千円 (直接経費: 1,200千円)
• キーワード: 高階型理論 / 単一化 / 結合子

研究概要

型付きラムダ計算に基づく高階論理のための推論メカニズムについて研究した。特に、型付き結合子論理体系を経由することで、ラムダ項の単一化問題を解くためのアルゴリズムを改善する可能性を探った。
1.結合子論理の体系としては、SとKを用いるものが事実上標準となっているが、単一化問題を考える上でこの組み合わせが最善であるという保証はない。他の組みあわせにもっと優れた特性を持つものがないか調査検討したが、この点については、現在のところ報告するに値する成果は得られていない。さらに調査を要する。
2.高階単一化アルゴリズムとしてはHuetの提案に基づくものが既に標準となっているが、結合子論理を経由することでもっと簡単で高速なアルゴリズムが得られるかどうかを調べた。結合子S,K,Iを用いる完全なアルゴリズムを新たに設計し、計算機上に実装した。実装上の困難は、Huetの提案に基づくものより少ないが、速度の向上については、確たる成果を見ていない。さらなる改善を要する。
まとめると、結合子項を用いた高階単一化アルゴリズムの設計、完全性の証明、計算機上への実装、実験による評価などが研究成果であるが、最終的なアルゴリズムとして公表するにたるほどのものは、残念ながら現在のところ得られていない。