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

点击翻译按钮获取中文摘要

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