2017 Fiscal Year Research-status Report
エフェクトシステムの表示的意味論にまつわる数学的構造
| Project/Area Number |
15K00014
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
勝股 審也 国立情報学研究所, 大学共同利用機関等の部局等, 特任研究員 (30378963)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | エフェクトシステム / 次数付きコモナド / 計算効果 / プログラミング言語の意味論 / 線形論理 |
|---|
| Outline of Annual Research Achievements |
本研究ではモナドの一般化である次数付きモナドと呼ばれる構造を導入し、エフェクトシステムの表示的意味論に応用してきた。本年度はその双対となる次数付きコモナドの研究を行った。
Girardの導入した線形論理は冪様相で始まる論理式に対して自由にcontractionやweakeningを行うことができる。後にGirard, Scedrov, Scottらは有界線形論理を導入し、冪様相にパラメータを追加してcontractionやweakeningの回数を制御できるようにした。このパラメータ化された冪様相は非明示的計算量理論において威力を発揮した他、関数型言語のコンパイルや、プログラムのロバストネスを見積もるのに応用されている。
パラメータ化された冪様相の圏論的意味論は、Gaboardiらの2014年の研究で「次数付き線形べきコモナド」として与えられているが、その定義は複雑で、端的にどのような構造を表しているのか不明であった。これは線形論理の冪様相に対応する圏論的構造(線形べきコモナド)が対称モノイダル随伴から導かれるというエレガントな特徴づけがあるのとは対照的である。
本研究は「次数付き線形べきコモナドはどのような構造を表しているのか？」という疑問に取り組み、以下の成果を得た。まず最初に、次数付き線形べきコモナドの定義中の4つの非自明な公理が、対称モノイダル圏のなす二重圏の2-セルに関する公理の2通りのインスタンスとなっていることを見出した。次に対称モノイダル圏のなす二重圏の水平方向を多重圏へと拡張した結果、次数付き線形べきコモナドはこの多重圏の中の特定の形式のモノイドとぴったり対応することがわかった。そしてこの特徴づけを利用して、次数付き線形べきコモナドのEilenberg-Moore圏に相当するものを導出し、これが線形べきコモナドの分解を与えることを示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度の研究により、次数付き線形べきコモナドという複雑な構造を(複雑な圏の)モノイドとして簡潔に特徴づけた。そしてこの特徴づけを応用し、次数付き線形べきコモナドの分解を与えた。これらの成果をまとめた論文は、その新規性が評価され、理論計算機科学の著名な国際学会であるFoSSaCS '18で採択されるに至った。本研究は次数付きモナドを研究の主眼においているが、その双対の構造に関する理解もまた「計算の過程の詳細な分析」に有用であり、本年度のこれらの研究成果は「エフェクトシステムの表示的意味論にまつわる数学的構造」の理解に対する貢献をなしている。
|
| Strategy for Future Research Activity |
平成29年度にあげていた研究課題について引き続き取り組む予定である。
* エフェクト変数の表示的意味論。エフェクト変数のあるエフェクトシステムはプログラムの副作用をより柔軟に見積もることができる。この機構の表示的意味論を、Lawvereの hyperdoctorineを参考にして与える予定である。この意味論の上に1) エフェクト多相性 2) エフェクトの再帰方程式の解釈を与え、より強力なエフェクトシステムのための表示的意味論を展開する予定である。
また、新しく以下の研究課題についても取り組む予定である。
* エフェクトシステムとその双対であるコエフェクトシステムは、プログラムのコスト分析において同等な分析能力を持つことがEzgiらにより報告されている。本研究課題ではこの同等性の意味論的な対応物を次数付きコモナドと次数付きモナドの間の対応関係から説明することを検討する。
|
