| 研究概要 |
直観主義論理と型付きλ計算との対応関係は,カリー・ハワードの同型対応として知られている.λμ計算とは,この対応関係を古典論理まで拡張することによりM.Parigotによって導入された論理体系である.λμ計算はλ計算の自然な拡張となっており,計算モデルとしてそれ自体興味深い体系となっている.本研究では,表示的な意味論の観点から,外延的なタイプフリーλμ計算が固有にもっている計算の構造やその性質をλ計算との比較において解明をして,次の結果が得られた.
(1)継続の概念に基づくλμ計算の表示的意味論:完備半順序集合で,D×D=D=[D→D]を満たす領域Dより,継続の概念に基づくλμ計算のモデルを与えた.この解釈では,継続をDXDの要素として,λμ式を[D×D→D]である連続関数と定義している.従って,外延的なタイプフリーλμ式の意味は,継続を引数にとる連続関数となっている.一方,Cモノイドは,上記領域方程式を満たすカルテシアン閉カテゴリにおける対象Dのエンドモルフィズムとなっている.よってλμ式の意味は,同時に,Cモノイドでも与えられることが明らかになった.
(2)外延的なタイプフリーλμ計算から全射的な組を持つλ計算への全単射的CPS-変換:まず,外延的なλμ計算から全射的な組を持つλ計算への健全なCPS変換を定義した.次に,CPS変換の像で,簡約規則の下で閉じているλ式の集合を生成するために,文脈自由文法を与えた.この形式文法に基づき,λμ計算への逆変換を定義することができた.これにより,上で与えたCPS変換の完全性を示すことができた.さらに,このCPS変換は,λμ式の集合と簡約規則の下で閉じているλ式の集合間の全単射を形成していた.
なお,以上の成果は学術論文でそれぞれ公表されている.
|
