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

• Project/Area Number: 17700013
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Fundamental theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: 長谷川 真人 Kyoto University, 数理解析研究所, 教授 (50293973)
• Project Period (FY): 2005 – 2007
• Project Status: Completed (Fiscal Year 2007)
• Budget Amount: ¥3,400,000 (Direct Cost: ¥3,400,000); Fiscal Year 2007: ¥1,000,000 (Direct Cost: ¥1,000,000); Fiscal Year 2006: ¥1,000,000 (Direct Cost: ¥1,000,000); Fiscal Year 2005: ¥1,400,000 (Direct Cost: ¥1,400,000)
• Keywords: 計算機科学 / 証明論 / 線型論理 / 非決定性計算 / ラムダ計算 / 相互作用 / 理論計算機科学 / プログラミング言語 / 意味論 / 圏論 / 数学基礎論

Research Abstract

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

Research Products

• [Journal Article] Finite dimensional vector spaces are complete for traced symmetric monoidal categories (2008)
  • Author(s): M. Hasegawa, M. Hofmann, G. Plotkin
  • Journal Title: Lecture Notes in Computer Science 4800 Pages: 367-385
  • Peer Reviewed
• [Journal Article] 再帰プログラムの意味論について (2007)
  • Author(s): 長谷川真人
  • Journal Title: 数学 59(2) Pages: 180-191
  • NAID: 130004558827
  • Peer Reviewed
• [Journal Article] A Terminating and Confluent Linear Lambda Calculus (2006)
  • Author(s): Y.Ohta, M.Hasegawa
  • Journal Title: Springer Lecture Notes in Computer Science 4098 Pages: 166-180
• [Journal Article] Relational Parametricity and Control (2006)
  • Author(s): M.Hasegawa
  • Journal Title: Logical Methods in Computer Science 2(3:3) Pages: 1-22
• [Journal Article] Coherence of the Double Involution on *-autonomous Categories (2006)
  • Author(s): J.R.B.Cockett, M.Hasegawa, R.A.G.Seely
  • Journal Title: Theory and Applications of Categories 17(2) Pages: 17-29
• [Journal Article] Classical linear logic of implications (2005)
  • Author(s): M.Hasegawa
  • Journal Title: Mathematical Structures in Computer Science 15(2) Pages: 323-342
• [Journal Article] Relational parametricity and control (extended abstract) (2005)
  • Author(s): M.Hasegawa
  • Journal Title: Proceedings of 20th Annual IEEE Symposium on Logic in Computer Science Pages: 72-81
• [Presentation] On Traced Monoidal Closed Categories (2007)
  • Author(s): M. Hasegawa
  • Organizer: Workshop on Traced Monoidal Categories, Network Algebras, and Applications
  • Place of Presentation: ブロツワフ(ポーランド)
  • Year and Date: 2007-07-15