メタ計算系における型導入によるプログラム変形導出

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

プログラムはある計算系の項の集合と考えることができる。計算系として有効性が広く認められているものに、ラムダ計算に基づく関数型計算系や、一階述語に基づく論理型計算系、項書え計算系などがある。これらの計算系を融和するシステムを本研究ではメタ計算系とよび、理論上、あるいは、メタプログラミングシステムとしての有用性に検討を加えた。われわれのアプローチは、様々な計算系を一つの計算系へと統合するのではなく、複数の計算系が一様な表現によって共存し、しかも計算系相互の接続を容易にする機構を作り出すものである。メタ計算系では、プログラムの変形導出が各固有の計算における計算(例えば、簡約化、反駁)と同等の意味を有する。われわれの研究では、型に関する知見を活用しつつ、プログラム変換技法の開発を行った。本研究によってえられた成果は次の4つに分類できる。(1)プログラム変換のアルコリズムに関して、LISPとラムダ計算に基づく関数型言語のプログラムの変換を考え、それを、LISPのコンパイラに組み込み実用的処理系を構築した。(2)プログラム変換のための計算系の形式化に関して、計算系の性質の分析と形式化が重要であることが明らかになり、言語処理系から抽象マシンに至るまで、統一的な形式化を行った。(3)型の扱いに関しては、多相型推論アルゴリズムのLISP処理系への適用を行った。(4)メタプログラミングの方法論をプログラミング変換に応用し、その結果として、メタ計算系のあり方に関する知見を得た。