非決定性相互作用の幾何構造

点击翻译按钮获取中文摘要

「相互作用の幾何」(Geometry of Interaction=GoI)は、もともと、Girardが、数理論理学の証明論における「証明の標準化」の過程の数学モデルとして考案したものであるが、その後、Abramskyらにより、双方向に作用しあう計算プロセス同士の関係を理解するための枠組みとして、一般化されたGoIの理論が展開されている。本研究では、GoIを、非決定性計算プロセスを解釈できるように拡張した枠組み、すなわち「非決定性相互作用の幾何」、(Geometry of Nondeterministic interaction=GoNI)を提唱し、その数学的な基礎および有意義な具体例を与えることを目指している。本年度は(1)GoNIの理論のなかで高階の相互作用を表現する手法、(2)GoNIの基本概念であるトレース付きモノイダル圏の具体的な数学構造による特徴づけについて成果を挙げた。前者では、トレース付きモノイダル圏が高階の計算の解釈を許すこと(モノイダル閉であること)とGoI構成が右随伴を持つことが同値であることを発見し、GoIやGoNIを高階の計算が解釈できるよう拡張する基本方針を与えた。これにより線型論理のモデルの理論とGoNIとの単純かつ基本的な関係が得られるとともに、GoNIの新しいモデルを構成する方法が得られた。後者では、自由生成されたトレース付き対称モノイダル圏が有限次元ベクトル空間と線型写像の圏における解釈を用いて完全に特徴づけられることをHofmannやPlotkinとともに示した。関連して、再帰プログラムの意味輪とトレース付きモノイダル圏に関するサーベイ論文を発表した。