| 研究概要 |
本研究課題の目的の一つは,弱外延性を持たないプログラム意味論を実現する数理モデルの一般的構築方法を与えることである.この目的の下で,具体的には,様々な表現力を持つラムダ計算の構文体系について,そのモデル論で使われている手法に基づき考察を行っている.
最も弱い単純型理論の計算体系に対して,その意味論の構築には弱カルテシアン閉圏と呼ばれる圏の構造さえあれば十分であること,その中でも特にwell-pointedでない圏構造によって弱外延性を持たない意味論が構成されることは広く知られている.これに対して,昨年度から今年度の初めにかけては,実際にwell-pointednessに関わる情報を明示的に制御する為,自由弱カルテシアン閉圏と集合・関数の圏という二つの解釈の視点を組み合わせた枠組みを提案した.(特に自由弱カルテシアン閉圏の射について新たな適用の概念を提案することでこのような仕組みが可能となる.)また,若干瑣末な結果ではあるが,こうした考察を行う過程の中で「カルテシアン閉圏の中には自明でないwell-pointedカルテシアン閉圏の構造が常に存在していること」なども分かり,単純型理論に対する弱外延性を持たない意味論の枠組みとしてカルテシアン閉圏の強すぎる側面も明らかになった.
今年度の後半では,これまでの結果を踏まえて,更にPCFと呼ばれるより強力な計算体系に対して機能する意味論の構築を試みた.PCFには新たに再帰を記述する為のμ演算子が組み込まれていて,その意味論には特定の射に対して(単純型理論の考察において導入された射の適用の概念の下で)不動点の存在が要求される.これについて有界完備領域とその上の連続関数の枠組みを取り入れ一つの構成法を与えた.現時点では「有界完備領域の代わりに完備束を採用することで自由圏の構成に必要なグラフの生成を平易にすること」や「カルテシアン閉圏の演算を全て階段関数のイデアルとして記述こと」を模索しながら,理論展開の整備を行っている.
|
