2001 Fiscal Year Annual Research Report
| Project/Area Number |
12740060
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
浜野 正浩 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (50313705)
|
|---|
| Keywords | MALL / full completeness / hypercoherence / softness / double gluing / ^*-autonomous with products / proof-net / categorical semantics |
|---|
| Research Abstract |
乗法加法線形論理学(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"を投稿準備中である。
|
Research Products
(1 results)
