| 研究課題/領域番号 |
15K00014
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | 次数付きモナド / エフェクトシステム / プログラミング言語の意味論 |
|---|
| 研究実績の概要 |
本研究ではエフェクトシステムに対し、パラメトリックエフェクトモナド(PEM)を用いて表示的意味論を与えている。これは標準的な圏論の構造であるモナドを一般化したものである。
本年度は、モナドの随伴による分解という古典的な事柄をPEMに拡張する研究を行った。ある固定されたモナドTに対し、それを誘導する随伴 L -| R のことをT-Resolutionという。T-Resolutionとそれら(随伴)の間の射はT-Resolutionの圏をなし、Kleisli圏とEilenberg-Moore圏を用いたモナドTのResolutionはそれぞれT-Resolutionの圏の始対象と終対象となることが知られている。
今年度はこの古典的な結果の類似物をPEMに対して与えた。まずResolutionの概念をPEMに対して拡張した。随伴だけではPEMのデータを復元するには不十分だったため、さらにモノイドの圏に対する作用を加えてResolutionの定義とした。次に、PEMに対するKleisli圏とEilenberg-Moore圏を定義し、それらがResolutionの圏において始対象と終対象となることを示した。
これらの成果に加えて、東京大学の藤井宗一郎氏とパリ・ディドゥロ大学のPaul-Andre Mellies氏との共同研究で、適切に構成された2-圏の中では、上述のEilenberg-Moore圏とKleisli圏がStreetの意味のEilenberg-Moore対象とKleisli対象となることが判明した。本年度のこれらの成果をまとめた論文は、国際会議 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)で採択された。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究のプロジェクトの一つに「PEMの圏論的な性質の分析」があり、このプロジェクトの本年度の目標は「PEMの随伴による分解に関する研究」である。研究実績欄に記したように、本年度のこの目標を達成し、研究は概ね順調に推移していると考えられる。
|
| 今後の研究の推進方策 |
今後はまず本研究のプロジェクトである「エフェクトシステムに見られる様々な機構の表示的意味論による扱い」に関する研究を行う。このプロジェクトの目標の一つに、エフェクト変数の表示的意味論がある。これはエフェクトシステムにエフェクト多相性とエフェクト上の不動点演算子を追加する際の基盤となる技術である。この表示的意味論をLawvere の hyperdoctorine と類似の構造を用いて与える予定である。
本研究のもうひとつのプロジェクトである「パラメトリックエフェクトモナドの圏論的な性質を分析」に関しては、PEMの双対であるパラメトリックエフェクトコモナドについて研究する予定である。特に、線形論理の!-様相をSemiringによってパラメタライズしたものはパラメトリックエフェクトコモナドの構造を持つ。そのようなパラメトリックエフェクトコモナドのEilenberg-Moore圏による分解を研究する予定である。
|
| 次年度使用額が生じた理由 |
本年度は概ね予定通り研究費を利用したが、本年度はもうひとつの科研費による助成を受けていたため、若干の余裕があり、研究費の１割ほどが次年度使用額となった。
|
| 次年度使用額の使用計画 |
次年度の研究費とあわせて国外出張に用いる予定である。
|
