| 研究課題/領域番号 |
17700013
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
長谷川 真人 京都大学, 数理解析研究所, 教授 (50293973)
|
|---|
| 研究期間 (年度) |
2005 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,400千円 (直接経費: 3,400千円)
2007年度: 1,000千円 (直接経費: 1,000千円)
2006年度: 1,000千円 (直接経費: 1,000千円)
2005年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| キーワード | 計算機科学 / 証明論 / 線型論理 / 非決定性計算 / ラムダ計算 / 相互作用 / 理論計算機科学 / プログラミング言語 / 意味論 / 圏論 / 数学基礎論 |
|---|
| 研究概要 |
「相互作用の幾何」(Geometry of Interaction=GoI)は、もともと、Girardが、数理論理学の証明論における「証明の標準化」の過程の数学モデルとして考案したものであるが、その後、Abramskyらにより、双方向に作用しあう計算プロセス同士の関係を理解するための枠組みとして、一般化されたGoIの理論が展開されている。本研究では、GoIを、非決定性計算プロセスを解釈できるように拡張した枠組み、すなわち「非決定性相互作用の幾何」、(Geometry of Nondeterministic interaction=GoNI)を提唱し、その数学的な基礎および有意義な具体例を与えることを目指している。
本年度は(1)GoNIの理論のなかで高階の相互作用を表現する手法、(2)GoNIの基本概念であるトレース付きモノイダル圏の具体的な数学構造による特徴づけについて成果を挙げた。前者では、トレース付きモノイダル圏が高階の計算の解釈を許すこと(モノイダル閉であること)とGoI構成が右随伴を持つことが同値であることを発見し、GoIやGoNIを高階の計算が解釈できるよう拡張する基本方針を与えた。これにより線型論理のモデルの理論とGoNIとの単純かつ基本的な関係が得られるとともに、GoNIの新しいモデルを構成する方法が得られた。後者では、自由生成されたトレース付き対称モノイダル圏が有限次元ベクトル空間と線型写像の圏における解釈を用いて完全に特徴づけられることをHofmannやPlotkinとともに示した。関連して、再帰プログラムの意味輪とトレース付きモノイダル圏に関するサーベイ論文を発表した。
|
