| 研究概要 |
「相互作用の幾何」(Geometry of Interaction, GoI)は、もともと、Girardが、証明論における証明の標準化の過程の数学モデルとして考案したものであり、その後、Abramskyらにより、双方向に作用しあう計算プロセス同士のなす関係を理解するための枠組みとして、一般化されたGoIの理論が展開されている。本研究では、GoIを、古典論理の証明論や平行計算プロセスにおける非決定性を解釈できるように拡張した枠組み「非決定性相互作用の幾何」(Geometry of Nondeterministic Interaction, GoNI)を提唱し、その数学的な基礎と有意義な具体例を与えることを目指す。
本年度は、本研究の基礎となる数学的手法の開発と整理を中心に行った。特に、核となる、線型論理の証明論と圏論的モデルに関して研究した。これに関連して、論文「Classical Linear Logic of Implications」を発表した。また、直観主義線型論理に対応する線型ラムダ計算のための強正規化性と合流性を満たす書き換え系を与えた(論文を投稿中)。これらの結果は、今後、GoNIの研究の遂行のための有効な道具となることが期待できる。また、GoNIと同じ古典論理の証明論に対応するラムダミュー計算について、パラメトリシティ原理を確立することに成功し、論文「Relational parametricity and control」で発表した。現時点では、この結果は直接GoNIの枠組みには属さないが、今後の研究によってGoNIとのなんらかの対応が得られることが期待される。
|
