2008 Fiscal Year Annual Research Report
| Project/Area Number |
19540145
|
|---|
| Research Institution | Okinawa Institute of Science and Technology |
|---|
Principal Investigator |
浜野 正浩 Okinawa Institute of Science and Technology, 数理生物学ユニット, 研究員 (50313705)
|
|---|
| Keywords | Indexed linear logic / Relational semantics / Pointed relation / Polarized linear logic / Denotational completeness / Phase semantics / Topological semantics / Second order linear logic |
|---|
| Research Abstract |
発表論文"An Indexed System for Multiplicative Additive Polarized Linear Logic"、LNCS 5213,(2008)では、Bucciarelli-Ehrhard(2000)のIndexed Multiplicative Additive Linear Logic(MALL(I)を、極性を持つ体系MALLP(I)に拡張した。この拡張を通じて、報告書のindexed体系の証明可能性に関する完全性と、通常の極付き線形論理の証明に関する完全性の関連を与えた。報告者の論理体系MALLP(I)は、関係圏Rel上の左右の随伴の組からなるpointed relationの圏がMALLPの表示意味論を与えることを主張する意味論的研究から生まれた。この意味論構成のため、前年度得られたHamano-ScottのPolarized Category(APAL 145(2007))の圏論枠組みを用いた。MALLP(I)での極性交換規則は、統語論的手法を用いて随伴性を定式化することにより得ることができ、この体系の論理規則は忠実にMALLPの表示意味論を記述することができた。
(J.S.Lに)印刷中論文"A Phase Semantics for Polarized Linear Logic and Second Order Conservativity"では、線形論理の代表的な証明可能性に対する意味論であるphase空間に、位相構造を導入することにより、MALLPの代数的意味論が得られることを示した。報告者のpolarized phase spaceでは、開核と閉包作用素の随伴性により、正の極性をopennessによって負の極性をclosednessによって位相構造を用いて表現できる。さらに報告者はこの意味論を用い、O.Laurent(2002)による未解決問題"二階線形論理の極付き部分体系に対する保存性"の解決を与えた。
|
