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

线性逻辑完备性定理的数学发展

基本信息

批准号：
12740060
负责人：
浜野正浩
金额：
$ 1.22万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
2000
资助国家：
日本
起止时间：
2000 至 2001
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12740060/
关键词：
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"を投稿準備中である。

从Ehrhard（'93）的超副词中，通过双胶合结构获得的接线区域的完整性。因此，我们首先给出了Joyal Sphere Sphere Sphere，对角线化自然转换与Girard的购物中心证明结构之间的对应关系。接下来，支持GHCOH的对角线自然转换的验证结构充满了连接性和周效，这是Gi-Rard（'96）的正确性标准。 GHCOH的任意对角线自然转化是对购物中心证明的表示，这是不取决于游戏环方法的第一个结果。结果发表在附属研讨会“ Full Computer Science”（2001年6月，美国波士顿，美国），为ND购物中心充分完整做准备。此外，在上述研究的过程中，已经发现，混合规则中的行为与ONS -Law系统中的行为完全不同。基于此观察，Girard的购物中心证明结构提供了图形理论特征，以证明购物中心+混合。获得此功能的方法是基于证明方法的配置的优点，这是对球体概念的响应，这是第一次实现的。结果将在AMS-SMF大会（2001年7月，里昂，法语，法语）上宣布，目前正在准备“购物中心证明结构的柔软性和与Mix的正确性标准”的论文。