| 研究概要 |
研究の初年度として、極性を持つ線形論理(polarized linear logic)に対する意味論を圏論的に構成し、これから通常の極をもたない線型論理の圏論意味論が導かれることを定式化した。さらに、確立した構成法を代数意味論に応用した。
発表論文(カナダ国Ottawa大学Phil Scott教授との共著)Masahiro Hamano and Philip Scott."A Categorical Semantics for Polarized MALL",Annals of Pure and Applied Logic.145(2007),North-Holland,276-313.では、Multiplicative Additive Polarized Linear Logic(MALLP)の圏論的な表示意味論を正と負な部分圏の間の随伴函手と代数的なモデュールにより構成じた。MALLPの意味論は、λμ計算体系のモデルであるSelingeのControl圏('01)の線形化を用いる構成しか知られていなかったが、従来のこの方法では圏論の本質であるべきfunctorialityが弱い形でしか保証されない、不自然さがあったが、報告者の構成法はこれを克服する一般的な枠組である。また、この構成の具体例がHylandのdouble gluing構成法の繰り返し(iteration)や、chu空間などによって与えられることを示した。さらに随伴が引き起こす不動点からなる圏が通常の線形論理のモデルを与えることを定式化し、MALLPの充満完全性定理を、報告者とR.BluteとP.Scott,によって確立された(極を持たない通常の)MALLの手法("Softness of Hypercoherences and MALL Full completeness",APAL.131(2005))に還元しながら得た。さらに、上で得られた圏論的構成方法を、証明可能性のための代数的意味論として知られるphase空間に適用し、開集合と閉集合の間の随伴函手を導き、MALLPの代数的意味論を得た。この位相構造を持つphase意味論を用い、二階線型論理(LLη2)の極付な部分体系(LLηpol2)に対ずる保存拡張性定理を得た。この結果は、M.Hamano and R.Takemura,"A Phase Semantics for Polarized Linear Logic"(29pages)として国際雑誌に投稿し査読中である。
|
