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

非确定性相互作用的几何

• 批准号: 17700013
• 负责人: 長谷川 真人
• 金额: $ 2.18万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17700013/
• 关键词: 計算機科学; 証明論; 線型論理; 非決定性計算; ラムダ計算; 相互作用; 理論計算機科学; プログラミング言語; 意味論; 圏論; 数学基礎論

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

Geometry of Interaction=GoI is a mathematical model of the process of standardization of proof in mathematical theory. In this study, we propose the fundamental principles of mathematics, such as Geometry of non-deterministic interaction=GoNI, non-deterministic computation, etc. This year, we have reviewed (1) the theoretical and higher-order interaction expression methods of GoNI,(2) the basic concepts of GoNI, the specific mathematical structure of GoNI, and the characteristics of GoNI. The former is the basic policy for high-level calculation, and the former is the basic policy for high-level calculation. The theory of linear logic and the method of constructing new logic are obtained. The latter is free to generate, and the latter is free to generate, and the latter is free to generate. The relationship between the two groups is discussed in detail.

项目成果

再帰プログラムの意味論について

关于递归程序的语义

• 发表时间: 2007
• 期刊: 数学 59(2)
• 作者: Asahiro;Yuichi;Akira Suzuki;Akira Suzuki;Akira Suzuki;Akira Suzuki;Jing Wang;Yoskinobu Tamura;田村慶信;Yoshinobu Tamura;田村慶信;田村慶信;田村 慶信;Yoshinobu Tamura;田村 慶信;田村 慶信;田村慶信;松島靖;田村慶信;Yoshinobu Tamura;長谷川真人
• 通讯作者: 長谷川真人

Relational parametricity and control

关系参数性和控制

• 发表时间: 2006
• 期刊: Logical Methods in Computer Science 2
• 作者: J.R.B.Cockett;M.Hasegawa;R.A.G.Seely;M.Hasegawa
• 通讯作者: M.Hasegawa

Coherence of the double involution on *-autonomous categories

*-自治范畴上的双重对合的一致性

• 期刊: Theory and Applications of Categories (in printing)
• 作者: J.R.B.Cockett;M.Hasegawa;R.A.G.Seely
• 通讯作者: R.A.G.Seely