圏論とグラフ論の融合を用いた高階加法体系を含む線形論理学の新しい統語論と意味論

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14740068
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 浜野 正浩 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (50313705)
• Keywords: linear logic / full completeness / MALL / hypercoherences / proof nets / softness

Research Abstract

前年度(14年度)に得られたMALL+Mixに対するsequentialization定理(裏面発表論文参照)で開発された圏論とグラフ論の関連を与える手法を利用して、乗法加法線形論理(MALL)に対する充満完全な意味論をEhrhardのhyper coherence圏('93)を用いて構成することに成功した。得られた充満完全性定理は、hypercoherence圏からdouble gluing構成して得られる圏の対角化自然変換(dinatural transfomation)がMALLの証明となっていることを主張するものである。これは、統語論からの独立性が不明瞭であった既存のゲーム意味論を全く用いることのない最初のMALLに対する充満完全な意味論となるものである。報告者はこの定理を、hypercoherence圏の持つsoftnessという圏論的性質と、GirardのMALL proof-structureが持つ加法体系の並行性を捉えるグラフ論的特性との対応関係に基づいて示した。また、加法体系の証明のグラフ論的特徴付けのために必要なサイクルの分析も行った。この結果は論文"Softness of Hypercoherences and MALL Full Completeness" (R.BluteとP.Scottとの共著、63pg.)として国際雑誌(Annals of Pure and Applied Logic, North Holland)に投稿して、査読後'04年3月に受理された。
また、このMALLに対する充満完全性定理の応用を、より簡明な証明論的性質を持つことが知られてきているPolarized Linear Logicに対して行った。さらに、これらの研究の過程で、線形論理の、創始者であるJ-Y.Girard教授やT.Ehrhard教授との議論により示唆されたcoherence spaceの持つ双対性のhyper coherenceへの一般化を解明するため、報告者のMALLの充満完全性定理で開発された手法の応用を試み、Coherence spaceとhypercoherencesの間に存在する階層とこの双対性の関連を明らかにした。

Research Products

• [Publications] Masahiro HAMANO: "Softness of MALL Proof-Structures and a correctness criterion with Mix"Archive for Mathematical Logic (Springer Verlag). to appear.
• [Publications] Richard BLUTE, Masahiro HAMANO, Philip SCOTT: "Softness of Hypercoherences and MALL Full completeness"Annals of Pure and Applied Logic (North Holland). to appear.