| 研究概要 |
直観主義論理の証明とプログラムとの同型対応関係は,プログラミング言語の設計,プログラムの静的・動的性質の解析や検証に有効に用いられてきた.この対応関係を古典論理まで拡張した計算体系としてM.Parigot(1992)によるλμ計算が知られている.そして,λμ計算が固有に持っている計算の性質や構造を古典論理の観点から解明して,その成果をソフトウェアの実現方法に還元することが重要な研究課題である.そこで,論理体系と型システムとの対応を踏まえて,ドモルガン的な双対性に基づくプログラム変換の計算的な性質を解明することを目指した.申請研究期間において得られた成果の概要を次にまとめる.
(1)多相型λ計算から存在型λ計算へのガロア埋め込み
双対性に基づくプログラム変換を多相型λ計算から存在型λ計算への埋め込みとして定義した.そして,この変換は,1ステップの計算規則から定義される擬順序関係に関して,所謂ガロア対応を形成していることが示された.
(2)形無しλμ計算の健全かつ完全なプログラム変換と抽象機械
双対性に基づくプログラム変換を形無しλμ計算の場合に拡張して,組を持つλ計算に対して健全かつ完全であることを示した.さらに,プログラム変換されたコードを処理する抽象的な機械を提案した.ここで,この機械は,計算に付随する代入情報を明示的に処理する機械になっている.
(3)アジョイントとしてのプログラム変換(CPS変換)と逆変換
多相型λ計算から存在型λ計算への埋め込みとして定義されたプログラム変換は,計算規則から定義される擬順序関係の基で,アジョイントを形成していることが明らかになった.
本研究で新たに導入された計算体系である存在型λ計算の計算的および論理的性質を今後解明することは,多相型λ計算を含む多くの計算体系に興味深い視点を与えるものと期待される.
|
