| 研究概要 |
直観主義論理の証明とプログラム(ラムダ計算)との対応関係は,カリー・ハワードの同型対応として知られている。ラムダミュウ計算とは,この対応関係を古典論理にまで拡張することによってParigotにより導入された論理体系である。ラムダミュウ計算はラムダ計算の自然な拡張となっており,それ自体興味深い計算体系である。本研究では,特に表示的意味論の観点から,タイプフリーのラムダミュゥ計算が固有にもっている計算の構造やその性質を,ラムダ計算との比較において解明して,以下の二つの成果が得られた。
(1)任意のラムダモデルからラムダミュウモデルが構成可能である:最初に,ラムダミュウ計算のミュウオペレータが不動点演算子によりコード化可能であることが示された。この結果を用いて,ミュウ式μa.Mとそのη展開した式とがβ変換のみで等価となる解釈が与えられた。このアイディアにより,外延的なラムダモデルが任意に与えられると,Godel-Gentzenの変換を介して,外延的なラムダミュウモデルが構築された。本結果の副産物として,ミュウオペレータは無限に続くラムダ抽象として解釈可能であることが明らかになった。
(2)ラムダミュウ計算の継続的な意味論は,CPS変換の像に対するScott流の直接的な意味論と模倣関係にある:再帰的な領域方程式D×D=D=[D→D]を満たす任意の領域Dより,ラムダミュウ計算の継続的意味論を与えた。次に,ラムダミュゥ計算からラムダ計算への構文的な変換であるCPS変換を定義した。そして,その像に対する所謂Scott流の直接的な意味論と,前述の継続的な意味論との間には完備半順序集合(CPO)上の形式的な模倣関係が定義可能であることが示された。
なお,以上の二つの結果は,学術論文によりそれぞれ公表されている。
|
