2006 Fiscal Year Annual Research Report
| Project/Area Number |
17700013
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
長谷川 真人 京都大学, 数理解析研究所, 助教授 (50293973)
|
|---|
| Keywords | 計算機科学 / 証明論 / 線型論理 / 非決定性計算 / ラムダ計算 / 相互作用 |
|---|
| Research Abstract |
「相互作用の幾何」(Geometry of Interaction=GoI)は、もともと、Girardが、数理論理学の証明論における「証明の標準化」の過程の数学モデルとして考案したものであるが、その後、Abramskyらにより、双方向に作用しあう計算プロセス同士の関係を理解するための枠組みとして、一般化されたGoIの理論が展開されている。本研究では、GoIを、非決定性計算プロセスを解釈できるように拡張した枠組み、すなわち「非決定性相互作用の幾何」(Geometry of Nondeterministic interaction=GoNI)を提唱し、その数学的な基礎および有意義な具体例を与えることを目指している。
本年度も、GoNIの基礎となる数学的手法の開発と整理を行った。GoNIの核にあるのは線型論理の型理論およびその圏論的なモデルの理論であるが、これに関して、線型型付きラムダ計算の構文を分析し、合流性と停止性を併せ持つ、簡潔な書き換え系を導くことに成功し、発表した。GoNIに対応するラムダ計算は、この線型ラムダ計算の拡張とみなすことができ、この書き換え系の手法を応用できることが期待される。また、非決定性を、適切な評価戦略を固定することでGoNIから非決定性を排除した場合に相当するラムダ・ミュー計算について、パラメトリシティと呼ばれる一様性原理を前年度に引き続き研究し、その成果を発表した。これはGoNIそのものに直接結びつくものではないが、GoNIにおける一様性原理の可能性を考えるための手がかりになると思われる。
|
