| 研究課題/領域番号 |
15K00013
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
長谷川 真人 京都大学, 数理解析研究所, 教授 (50293973)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | プログラミング言語 / 意味論 / 位相的量子計算 / 遅延評価 / 圏論 / 線形論理 |
|---|
| 研究実績の概要 |
プログラミング言語の実装モデルに焦点をあてたプログラム意味論の構築を目指し、前年度に引き続き必要となる数学構造の研究を行った。
前年度に開始した、効率的なプログラム実装の意味論の基礎となる線形論理の圏論モデルの研究では、位相的量子計算など、可換性（対称性）が成り立たないか制限されているような計算モデルを念頭に置き、対称性を必ずしも持たないモノイダル圏における線形冪コモナドの概念および例を調べ、国際研究集会LINEARITY2017およびそのポストプロシーディングスにて発表した。
まだ、対称性を仮定しないモノイダル圏における巡回構造・再帰構造を捉えるトレースについて研究した。これについては、以前得ていた、対称性をもつ場合にトレースと弱い双対性（*-自律性）から強い双対性（コンパクト閉性）が導かれるという結果を、対称性がない場合に拡張することを目指した。この問題については最終的な結果には至らなかったが、具体的に強い双対性（の候補）をつくる構成や証明の方針など、多くの新しい知見を得ることができ、得られた成果を内外のセミナー・研究会にて発表した。
さらに、対称性をもつモノイダル圏がトレース付きモノイダル圏に埋め込められるかどうかを問う２０年来の未解決問題について研究し、これについても部分的な成果を得た。特に、Selingerの予想が成り立たないことを、星野直彦らとともに確認し、埋め込み可能性の様々な必要条件を見出した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
対称性を仮定しない意味論の構築が順調に進んでいる。線形冪コモナドについては基礎的な理論整備が済み論文が出版された。トレースと*-自律性についても、新しい知見が多く得られた。トレース付きモノイダル圏への埋め込み問題についても、星野直彦らの協力を得て、顕著な進展が見られた。
|
| 今後の研究の推進方策 |
引き続き、これまでに得られたモノイダル圏等に関する研究を進める。特に、トレースと*-自律性の問題、及びトレース付きモノイダル圏への埋め込み問題について、早期解決を目指す。
あわせて、プログラミング言語の実装の意味論の構築を進めていく。
|
