| 研究課題/領域番号 |
15K00014
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | エフェクトシステム / 次数付きモナド / 計算効果 |
|---|
| 研究実績の概要 |
本研究ではモナドの一般化である次数付きモナド(パラメトリックエフェクトモナドから名称を変更)と呼ばれる構造を導入し、エフェクトシステムの表示的意味論に応用してきた。本年度は研究計画を変更し、次数付きモナドと次数付きコモナドの間の分配束の定式化と、その具体例の研究を行った。プログラミング言語の表示的意味論において、計算効果を表す構造としてモナドが用いられる一方、プログラムが消費する資源を(モナドの双対である)コモナドで表すアプローチがある。ここで、モナドとコモナドの間に分配束とよばれる構造を導入すると、これらの意味論を組み合わせ、資源を消費し外界に作用するプログラムの意味を合成的に与えることができる。このアプローチを次数付きモナド及びコモナドに拡張することで、副作用の生成と資源の消費の両方を詳細に捉える型システムと、その意味論が展開できると考えた。この着想の元、次数付きモナドと次数付きコモナドの間の分配束を定義し、その具体例を与えた。また、この分配束を与えるにはモナドおよびコモナドの次数の間に外部Zappa-Szep積の構造が必要であることがわかった。
また、関連する研究として、領域の圏と距離空間の圏を融合した圏を構成し、この中で高階プログラミング言語Fuzzの距離空間的意味論を与えた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度行った次数付きモナドと次数付きコモナドの間の分配束に関する研究は、本研究のプロジェクトの一つである「次数付きモナドの圏論的な性質の分析」における成果に該当し、本研究の進展に貢献している。
|
| 今後の研究の推進方策 |
昨年度にあげていた研究課題について引き続き取り組む予定である。
* 次数付きコモナドのEilenberg-Moore圏の定義に関する研究。本年度の研究の副次的な成果として、次数付きコモナドの単純な公理化を得た。その際、いくつかの公理はGrandisとPareらが与えたモノイダル圏がなす二重圏の2-セルに関する公理と一致することを見出した。これを応用し、次数付きコモナドを適切に設定された圏でのモノイドとして特徴づけ、そのモノイドの作用する圏としてEilenberg-Moore圏を定義する事を試みる。
* エフェクト変数の表示的意味論。エフェクト変数のあるエフェクトシステムはプログラムの副作用をより柔軟に見積もることができる。この機構の表示的意味論を、Lawvereの hyperdoctorineを参考にして与える予定である。
|
| 次年度使用額が生じた理由 |
本年度の予算のうち、必要な分をほぼ使用した。余った分については無理に使用せず、来年度に残すことにした。
|
| 次年度使用額の使用計画 |
余った分は旅費及び物品日に用いる予定である。
|
