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

研究課題

研究課題/領域番号	12740060
研究種目	奨励研究(A)
配分区分	補助金
研究分野	数学一般(含確率論・統計数学)
研究機関	北陸先端科学技術大学院大学
研究代表者	浜野正浩北陸先端科学技術大学院大学, 情報科学研究科, 助手 (50313705)
研究期間 (年度)	2000 – 2001
研究課題ステータス	完了 (2001年度)
配分額 *注記	1,900千円 (直接経費: 1,900千円) 2001年度: 900千円 (直接経費: 900千円) 2000年度: 1,000千円 (直接経費: 1,000千円)
キーワード	MALL / full completeness / hypercoherence / softness / double gluing / ^-autonomous with products / proof-net / categorical semantics / linear logic / denotational semantics / dinatural transformation / Mix / -autonomous category / Pontrjagin duality
研究概要	乗法加法線形論理学(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"を投稿準備中である。