2008 Fiscal Year Annual Research Report
| Project/Area Number |
20500010
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
長谷川 真人 Kyoto University, 数理解析研究所, 教授 (50293973)
|
|---|
| Keywords | プログラム理論 / プログラム意味論 / 数理論理学 / 圏論 |
|---|
| Research Abstract |
双方向に作用しあう計算プロセスからなるシステムのモデルである「相互作用の幾何」は、高階関数・高階プログラムの解釈に必要な構造(モノイダル閉圏の構造)を加えることにより、計算資源の非線型な利用を明快に表現できる、より豊かな数学構造を自然に持つようになることが、研究代表者の)最近の研究によって明らかになってきた。本研究は、この最近の発見を出発点として、高階関数と巡回・再帰構造の有機的な組み合わせを中核にした、「高階相互作用の幾何」の理論を提唱し、その数学的な基礎とプログラミング言語理論における応用を与えることを目指すものである。本年度の主要な研究実績は以下のとおりである。
(1) 「高階相互作用の幾何」を展開するために必要な数学構造の定式化に取り組み、その中核をなすトレース付モノイダル閉圏の性質について調べた。
(2) 「相互作用の幾何」の圏論的な基礎であるInt構成に関するJoyal, Street, Verityの有名な主定理にこれまで知られていなかった欠陥(双随伴の不成立)があることを指摘し、その修正を行った(勝股審也との共同研究)。
(3) トレース付モノイダル閉圏に関する基本的な結果(トレース付モノイダル圏がモノイダル閉圏になることとInt構成により得られるトーティルモノイダル圏への埋め込みが右随伴を持つことの同値性)を学術雑誌に投稿し、受理された。
(4) 具体例として、ゲーム意味論におけるネガティヴなConwayゲームからなるトレース付モノイダル閉圏について考察した。
|
