2000 Fiscal Year Annual Research Report
| Project/Area Number |
12740060
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
浜野 正浩 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (50313705)
|
|---|
| Keywords | linear logic / full completeness / categorical semantics / denotational semantics / dinatural transformation / Mix / *-autonomous category / Pontrjagin duality |
|---|
| Research Abstract |
乗法的線形論理(MLL)に対する充満完全性定理(full completeness theorem)を、数学的に具体性を持つ様々な^*-autonomous圏(MLLの圏論モデル)の中で得た。"Z-modules and Full Completeness of Multiplicative Linear Logic"では、Z-加群のなす圏で論理式を対象に、証明を対象間のz-不変な射に解釈するモデルが、MIX規則を含んだMLLに対して充満完全になることを示した。この解釈はMLLのカット除去のプロセスによって不変であることより表示的意味論(denotational semantics)とみなすことができる。"Pontrjagin Duality and Full Completeness for Multiplicative Linear Logic(Without Mix)"では、位相ア-ベル群のなす圏で、論理式をmultivariant-functorに、証明をdinatural transformationに解釈するモデルが、MIX規則を持たない純粋なMLL体系に対して充満完全になることを示した。このことは有名な双対定理であるPontrjagin Dualityを用いて示された。さらにこれらを乗法加法的線形論理(MALL)に拡張する重要な基礎として、GirardのMALL proof-structureとJoyalの圏論的性質softnessの関連を与えた。特に、productを持つ^*-autonomous圏(MALLの圏論モデル)が乗法的充満完全でかつsoftnessの性質を満たすならばその圏の全ての対角化自然がGirardのMALL proof-structureに対応していることを示した。具体的にはEhrhardのhyper coherenceのなすproductを持つ^*-autonomous圏の全ての射がsoftになることが分かった。これらとMALL+MIX proofのグラフ論的特徴付定理に基づき、hyper coherencesのなす圏を用いたMALL+MIXに対する充満完全性定理を現在準備中である。
|
-
[Publications] Masahiro Hamano: "Pontrjagin duality and full completeness for multiplicative linear logic (without Mix)"Math.struct.in comp.science. vol.10. 231-259 (2000)
-
[Publications] Masahiro Hamano: "Z-modules and full completeness of multiplicative linear logic"Annals of Pure and Applied Logic . 107. 165-191 (2001)
