| 研究概要 |
直観主義論理と型付きラムダ計算との対応関係は,カリー・ハワードの同型対応として古くから知られている.λμ計算とは,この対応関係を古典論理にまで拡張することによりM.Parigotが導入した論理体系である.λμ計算はλ計算の自然な拡張となっており,計算モデルとしてそれ自体興味深い体系となっている.平成14年度,15年度における研究成果として,次の点について明らかにしてきた.
(1)タイプフリーλμ計算及び単純型付きλμ計算からλ計算へのCPS変換
(2)継続の概念に基づくλμ計算の表示的意味論及びCモノイド
(3)CPS変換の像に対する直接的意味論と継続に基づく表示的意味論との完備半順序集合上の模倣関係
これらの成果を発展させかつ今後の研究の方向性を明確にするために,本研究では多相型λ計算を対象として,次の結果が得られた。
(4)存在型計算体系の導入
連言,2階存在型などを持つ存在型計算体系を新しく導入した.例えば,抽象データ型はこの体系で型付け可能となっている。そして,多相型λ計算と存在型計算体系間の変換及び逆変換を与え,変換規則が単射を形成していることが示された。
(5)多相型λ計算と存在型計算体系とのガロア対応
多相型λ計算と存在型計算体系におけるそれぞれの計算規則は,変換規則及び逆変換に関して単調性を有しており,二つの計算モデル間にはガロア対応及びガロア埋め込みが存在していた.そして,この二つの計算モデル間に美しい双対関係が存在することを明らかにした.
(6)多相型λ計算の基本的な性質
多相型λ計算の正規化性,合流性などの基本的な性質は,ガロア対応関係にある存在型計算体系のそれらより帰結されることがわかった.
さらに,本研究で導入された概念は,多相型λμ計算に拡張しても機能することが確認されている.また,存在型計算体系は,知る限りにおいては,これまでに研究されていなかったようであり,この計算モデルの性質を解析することは,多相型λ計算を含む計算体系に新たなかつ興味深い視点を与えるものと期待される.なお,これらの成果は,ラムダ計算に関する国際会議(Typed Lambda Calculi and Applications)で公表されている.
|
