2005 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階ラムダ計算から存在型を持つ体系へのガロア埋め込み
双対性に基づくプログラム変換を2階ラムダ計算から存在型体系への埋め込みとして定義した.そして,この変換は,1ステップの計算規則から定義される擬順序関係に関して,所謂ガロア対応を形成していることが示された.さらに,2階ラムダ計算の正規な証明図におけるパスは,この変換により,ドモルガンの双対性の基で,存在型体系の証明図中の反転したパスに対応していること(証明双対性)が解明された.特に,多相型関数が,抽象データ型のプログラムにより自然に解釈されることも明らかになった.
(2)型無しラムダミュウ計算の健全および完全なプログラム変換
(1)のプログラム変換を型無しラムダミュウ計算の場合に拡張して,組を持つラムダ計算に対して健全かつ完全であることを示した.さらに,プログラム変換されたコードを処理する抽象的な機械を提案した.ここで,この機械は,計算に伴う代入情報を明示的に処理する機械にもなっている.
なお,以上の成果はそれぞれ学術論文において公表されている.
|
Research Products
(3 results)
