線形論理学における充満完全性定理の数学的展開

乗法加法線形論理学(MALL)に対する充満完全性定理(full completeness theorem)を、Ehrhard('93)のhypercoherenceがなす(productとcoproductを持つ)^*-autonomous圏HCohからdouble gluing constructionによって得られる圏GHCohの中で得た。このためにまず、Joyalの圏論的性質softnessを満たす圏の対角化自然変換とGirardのMALL proof-structureの対応関係を与えた。次にGHCohの対角化自然変換と対応しているproof-structureはGi-rard('96)のcorrectness criterionであるconnectednessとacyclicityを満たしていることを示した。このGHCohの任意の対角化自然変換がMALLの証明のdenotationになっていることを示す充満完全性定理は、ゲーム輪的方法によらない最初の結果である。この結果は国際会議Logic in Computer Scienceの提携ワークショップ"Full Completeness and Full Abstraction"('01年6月,ボストン,合衆国)で発表し現在論文"Softness of Hypercoherences and MALL Full Completeness"を投稿準備中である。さらに上記の研究の過程でMix規則の加法体系の中での、振る舞いが乗法体系の中でのそれと、全く異なることが分かってきた。この観察に基づき、GirardのMALL proof-structureがMALL+Mixの証明となるためのグラフ論的特徴付を与えた。この特徴付を得るための手法は証明論的手法に基づく構成的なものであるという利点があり、これは圏論概念との対応を与えることによって始めて可能になった。この結果はAMS-SMF共同国際会議('01年7月,リヨン,仏国)で発表し、現在論文"Softness of MALL Proof-Structures and Correctness Criterion with Mix"を投稿準備中である。

乗法加法線形論理学(MALL)に対する充満完全性定理(full completeness theorem)を、Ehrhard('93)のhypercoherenceがなす(productとcoproductを持つ)^*-autonomous圏HCohからdouble gluing constructionによって得られる圏GHCohの中で得た。このためにまず、Joyalの圏論的性質softnessを満たす圏の対角化自然変換とGirardのMALL proof-structureの対応関係を与えた。次にGHCohの対角化自然変換と対応しているproof-structureはGi-rard('96)のcorrectness criterionであるconnectednessとacyclicityを満たしていることを示した。このGHCohの任意の対角化自然変換がMALLの証明のdenotationになっていることを示す充満完全性定理は、ゲーム輪的方法によらない最初の結果である。この結果は国際会議Logic in Computer Scienceの提携ワークショップ"Full Completeness and Full Abstraction"('01年6月,ボストン,合衆国)で発表し現在論文"Softness of Hypercoherences and MALL Full Completeness"を投稿準備中である。さらに上記の研究の過程でMix規則の加法体系の中での、振る舞いが乗法体系の中でのそれと、全く異なることが分かってきた。この観察に基づき、GirardのMALL proof-structureがMALL+Mixの証明となるためのグラフ論的特徴付を与えた。この特徴付を得るための手法は証明論的手法に基づく構成的なものであるという利点があり、これは圏論概念との対応を与えることによって始めて可能になった。この結果はAMS-SMF共同国際会議('01年7月,リヨン,仏国)で発表し、現在論文"Softness of MALL Proof-Structures and Correctness Criterion with Mix"を投稿準備中である。