2006 Fiscal Year Annual Research Report
| Project/Area Number |
17500004
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
|
|---|
| Keywords | ガロア対応 / 多相型 / 抽象データ型 / CPS変換 / 継続 / ラムダ計算 / 継続 |
|---|
| Research Abstract |
直観主義論理の証明とプログラム(型付きラムダ計算)との同型対応関係は,プログラミング言語の設計,プログラムの静的・動的な性質の解析や検証に有効に用いられてきた.この対応関係を古典論理まで拡張した計算体系としてM.Parigot(1992)によるラムダミュウ計算が知られている.そして,ラムダミュウ計算が固有に持っている計算の性質や構造を古典論理の観点から解明して,その成果をソフトウェアの実現方法に還元させることが重要な研究課題である.そこで,論理体系と型システムとの対応関係を踏まえて,ドモルガン的な双対性に基づくプログラム変換の計算的な性質を解明することを目指した.本研究で得られた成果の概要は次のとおりである.
(1)形無しラムダミュウ計算の健全かつ完全なプログラム変換と抽象機械
双対性に基づくプログラム変換を形無しラムダミュウ計算の場合に拡張して,組を持つラムダ計算に対して健全かつ完全であることを示した.さらに,プログラム変換されたコードを処理する抽象的な機械を提案した.そして,ラムダミュウ計算に対する機械の妥当性を示した.ここで,この機械は,計算に付随する代入情報を明示的に処理する機械になっている.
(2)アジョイントとしてのプログラム変換(CPS変換)*と逆変換
多相型ラムダ計算から存在型ラムダ計算への埋め込みとして定義したプログラム変換(CPS変換)は,計算規則から定義される擬順序関係の基で,アジョイントを形成していることが明らかになった.すなわち,双対性に基づくCPS変換*が与えられると,存在型ラムダ計算の式Pに対する逆変換は,*に関する逆像の最大値として定義可能である.ここで,Q≦PとはP→Q(存在型ラムダ計算の計算規則から定義される擬順序)である.
本研究で新たに導入された存在型ラムダ計算の計算的・論理的性質を解明することは、多相型ラムダ計算を含む多くの体系に興味深い視点を与えるものと期待される.
|
