エフェクトシステムの表示的意味論にまつわる数学的構造

2016 Fiscal Year Research-status Report

• Project/Area Number: 15K00014
• Research Institution: Kyoto University
• Principal Investigator: 勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
• Project Period (FY): 2015-04-01 – 2019-03-31
• Keywords: エフェクトシステム / 次数付きモナド / 計算効果

Outline of Annual Research Achievements

本研究ではモナドの一般化である次数付きモナド(パラメトリックエフェクトモナドから名称を変更)と呼ばれる構造を導入し、エフェクトシステムの表示的意味論に応用してきた。本年度は研究計画を変更し、次数付きモナドと次数付きコモナドの間の分配束の定式化と、その具体例の研究を行った。プログラミング言語の表示的意味論において、計算効果を表す構造としてモナドが用いられる一方、プログラムが消費する資源を(モナドの双対である)コモナドで表すアプローチがある。ここで、モナドとコモナドの間に分配束とよばれる構造を導入すると、これらの意味論を組み合わせ、資源を消費し外界に作用するプログラムの意味を合成的に与えることができる。このアプローチを次数付きモナド及びコモナドに拡張することで、副作用の生成と資源の消費の両方を詳細に捉える型システムと、その意味論が展開できると考えた。この着想の元、次数付きモナドと次数付きコモナドの間の分配束を定義し、その具体例を与えた。また、この分配束を与えるにはモナドおよびコモナドの次数の間に外部Zappa-Szep積の構造が必要であることがわかった。
また、関連する研究として、領域の圏と距離空間の圏を融合した圏を構成し、この中で高階プログラミング言語Fuzzの距離空間的意味論を与えた。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本年度行った次数付きモナドと次数付きコモナドの間の分配束に関する研究は、本研究のプロジェクトの一つである「次数付きモナドの圏論的な性質の分析」における成果に該当し、本研究の進展に貢献している。

Strategy for Future Research Activity

昨年度にあげていた研究課題について引き続き取り組む予定である。
* 次数付きコモナドのEilenberg-Moore圏の定義に関する研究。本年度の研究の副次的な成果として、次数付きコモナドの単純な公理化を得た。その際、いくつかの公理はGrandisとPareらが与えたモノイダル圏がなす二重圏の2-セルに関する公理と一致することを見出した。これを応用し、次数付きコモナドを適切に設定された圏でのモノイドとして特徴づけ、そのモノイドの作用する圏としてEilenberg-Moore圏を定義する事を試みる。
* エフェクト変数の表示的意味論。エフェクト変数のあるエフェクトシステムはプログラムの副作用をより柔軟に見積もることができる。この機構の表示的意味論を、Lawvereの hyperdoctorineを参考にして与える予定である。

Causes of Carryover

本年度の予算のうち、必要な分をほぼ使用した。余った分については無理に使用せず、来年度に残すことにした。

Expenditure Plan for Carryover Budget

余った分は旅費及び物品日に用いる予定である。

Research Products

• [Int'l Joint Research] バッファロー大学/ペンシルバニア大学(米国)
  • Country Name: U.S.A.
  • Counterpart Institution: バッファロー大学/ペンシルバニア大学
• [Int'l Joint Research] インペリアル・カレッジ・ロンドン(英国)
  • Country Name: UNITED KINGDOM
  • Counterpart Institution: インペリアル・カレッジ・ロンドン
• [Int'l Joint Research] タリン工科大学(エストニア)
  • Country Name: ESTONIA
  • Counterpart Institution: タリン工科大学
• [Int'l Joint Research] 高等師範学校/パリディドロ大学(フランス)
  • Country Name: FRANCE
  • Counterpart Institution: 高等師範学校/パリディドロ大学
• [Journal Article] A semantic account of metric preservation (2017)
  • Author(s): Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui
  • Journal Title: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 Volume: － Pages: 545-556
  • DOI: 10.1145/3009837.3009890
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Combining effects and coeffects via grading (2016)
  • Author(s): Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, Tarmo Uustalu
  • Journal Title: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 Volume: － Pages: 476-489
  • DOI: 10.1145/2951913.2951939
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant