2002 Fiscal Year Annual Research Report
圏論とグラフ論の融合を用いた高階加法体系を含む線形論理学の新しい統語論と意味論
| Project/Area Number |
14740068
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
浜野 正浩 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (50313705)
|
|---|
| Keywords | linear logic / MALL+Mix / MALL proof structure / sequentialization theorem / Joyal's softness / full completeness / proof net |
|---|
| Research Abstract |
乗法加法線形論理学(MALL)にMix規則を加えた体系(MALL+Mix)に対するsequentialization定理を得た。
この定理は、GirardのMALL proof-structures('96)がMALL+Mixの証明になることを、グラフ論的性質acyclicityによって特徴付けるものであり、乗法体系に対してはよく知られていたが、加法体系に対しては未解決であった。報告者はこの定理を、Joyal('95)による圏論的特性softnessとGirard('96)による加法体系の並行性を捉えるグラフ論的特性という全く独立な2つの概念の対応関係を与えることによって得た。このことは、従来の並列性を扱うための複雑なグラフ的方法に、より見通しの良い構造的方法を与えたことを意味する。また報告者の特徴付を得るための手法は証明論的手法に基づく構成的なものであるという利点がある。
この結果は論文"Softness of MALL Proof-Structures and a Correctness Criterion with Mix",として国際雑誌に投稿中である。
また、このsequentialization定理と密接な関連があり、報告研究の先行結果である乗法加法線形論理学(MALL)に対する充満完全性定理(full completeness theorem)に関して、国際数学者会議2002の併設ワークショップThe 8th Asian Logic Conference(中国、Southwest China Normal University) "FullCompleteness for Linear Logic"と題する招待講演を行い、現在論文"Softness of Hypercoherences and MALL Full Completeness"を投稿準備中である。
|
