| 研究概要 |
今年度は、証明網の研究をさらに深めるため、J.-Y.Girard"Locus Solum"を研究し、さらにケンブリッジ大のM.Hyland,エジンバラ大のG.Plotkin,J.Power及びパリ大のP.-L.Gurienとの共同研究を行った。その結果まず論理式の役割が
(1)証明の構成要素として位置(ロケーション)を表す(証明論的役割)
(2)証明の推論プロセスを表す半順序構造を表す(ドメイン理論的役割)
(3)証明を真とする空間(通常To-分離公理を満たす)(型理論的役割)
となることがわかった。また。計算の意味論を深める上で、論理学におけるドモルガン性をゲームセマンティクスにより新解釈を与えることが重要であると認識した。今後、並列計算のモデルとして評価されてきた証明網の意味論の研究に、型理論的"Fully-Abstract"であるCurry-Howard同型対応とドメイン理論的"Fully-Abstract"であるBohmの定理がどのように反映され、さらに発展する方向を定めていくのか大変興味深い。
|
