2004 Fiscal Year Annual Research Report
| Project/Area Number |
14540119
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
近藤 通朗 東京電機大学, 情報環境学部, 教授 (40211916)
|
|---|
| Keywords | λμ計算 / CPS変換(継続) / 多相型関数 / 抽象データ型 / カリー・ハワード同型 / ガロア対応 / 制御オペレータ / 双対性 |
|---|
| Research Abstract |
直観主義論理と型付きラムダ計算との対応関係は,カリー・ハワードの同型対応として古くから知られている.λμ計算とは,この対応関係を古典論理にまで拡張することによりM.Parigotが導入した論理体系である.λμ計算はλ計算の自然な拡張となっており,計算モデルとしてそれ自体興味深い体系となっている.平成14年度,15年度における研究成果として,
(1)タイプフリーλμ計算及び単純型付きλμ計算からλ計算へのCPS変換
(2)継続の概念に基づくλμ計算の表示的意味論及びCモノイド
(3)CPS変換と表示的意味論との完備半順序集合上の模倣関係
などについて明らかにしてきた.これらの成果を発展させるために,本研究では多相型λ計算を対象として,次の結果が得られた.
(4)存在型計算体系の導入
連言,2階存在型などを持つ存在型計算体系を新しく導入した.例えば,抽象データ型はこの体系で型付け可能となっている.そして,多相型λ計算と存在型計算体系間の変換及び逆変換を与え,変換規則が単射を形成していることが示された.
(5)多相型λ計算と存在型計算体系とのガロア対応
多相型λ計算と存在型計算体系におけるそれぞれの計算規則は,変換規則及び逆変換に関して単調性を有しており,二つの計算モデル間にはいわゆるガロア対応関係が存在していることが解明された.
(6)多相型λ計算の基本的な性質
多相型λ計算の正規化性,合流性などの基本的な性質は,ガロア対応関係にある存在型計算体系のそれらより帰結されることがわかった.
さらに,本研究で導入された概念は,多相型λμ計算に拡張しても機能することが確認されている.また,存在型計算体系は,知る限りにおいては,これまでに研究されていなかったようであり,この計算モデルの性質を解析することは,多相型λ計算を含む計算体系に新たなかつ興味深い視点を与えるものと期待される.なお,これらの成果は,日本ソフトウェア科学会第21回大会で公表された.
|
