2009 Fiscal Year Annual Research Report
Project/Area Number |
09J03783
|
Research Institution | Kyoto University |
Principal Investigator |
星野 直彦 Kyoto University, 理学研究科, 特別研究員(DC2)
|
Keywords | 多相型線形ラムダ計算 / 観測的同値 / 相互作用の幾何 / Int構成 / トレース付モノイダル圏 / 双積 |
Research Abstract |
多相型線形ラムダ計算の観測的同値を特徴付ける圏論的モデルの構成を目指し、Girardによって提唱された相互作用の幾何(Geometry of Interaction, GoI)の研究を行った。GoIはゲーム意味論とよく似た特徴を持つ古典線形論理のモデルである。GoIからは線形実現可能性解釈を与える代数が得られることが知られている。またAbramskyによってその代数具体例の一つに基づいた実現可能性解釈が多相型ラムダ計算のML-typeに対するfull completeなモデルを与えることが示されている。このことからGoIから多相型線形ラムダ計算の観測的同値を与える線形実現可能性解釈が得られるのではないかと考えた。GoIのアイデアは証明を試みる側とそれを反証しようとする側の対話であり、その構造はトレース付モノイダル圏とInt構成という形で圏論的に与えられている。当年度はこのトレース付モノイダル圏とInt構成がそれら以外の圏論的構造、特に双積といわれる構造との間にどのような関係があるのかを研究した。その結果、Int構成はトレース付モノイダル圏が半双積を持つ場合に半双積を持つコンパクト閉圏を与えることが明らかになった。またこの応用として古典線形ラムダ論理の加法的乗法的部分論理に対する圏論的GoI解釈の枠組みを提案した。双積は多相型線形ラムダ計算のlinear exponential comonadの構成に用いることができると考える。双積に基づいたlinear exponential comonadの構成はGoIではまだ研究されていない一方でその構成自体は線形ラムダ計算の研究においては重要なものである。また(半)双積を持つコンパクト閉圏は量子計算の圏論的モデルとして用いられる構造であり量子計算への応用も考えられる。
|