2018 Fiscal Year Research-status Report
エフェクトシステムの表示的意味論にまつわる数学的構造
| Project/Area Number |
15K00014
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
|
|---|
| Project Period (FY) |
2015-04-01 – 2020-03-31
|
| Keywords | エフェクトシステム / 次数付きモナド / 差分プライバシー / 次数付きコモナド / 計算効果 |
|---|
| Outline of Annual Research Achievements |
1. 2017年度に得た、次数付き線形べきコモナドを対称モノイダル圏のなす多重圏におけるモノイドとして特徴づけた研究成果は、理論計算機科学の代表的な国際会議であるFoSSaCS 2018にて採択された。
2. 次数付きモナドの応用の一つとして、アルゴリズムの差分プライバシーを型理論的に保証する研究を行った。この研究はArthur Azevedo de Amorim氏(Carnegie Mellon大学)、Justin Hsu氏(Wisconsin-Madison大学)、Marco Gaboardi氏(Buffalo大学)との共同研究である。この研究の基礎となったのは、ReedとPierceらのアフィン型システムの基本的な部分に対する距離空間を用いた意味論である(2017年度に国際学会POPLで発表)。2018年度の主な成果は、この距離空間的意味論を、確率的計算を表す型に対して拡張した点である。この拡張において導入したのがモナドの次数付き !-持ち上げと呼ばれる構造である。これは、確率的計算を表す型に関する推論規則に自然に対応するものとして導入したが、確率分布モナドと距離空間のセッティングで吟味すると、ある種の性質を満たす確率分布間の距離(Kullback-Leibler divergence、statistical divergence)と丁度対応するものであることがわかった。また、この対応を応用し、確率的計算を表す型を適切な次数付き !-持ち上げにより解釈することで、プログラムの(epsilon, delta)-差分プライバシーを表現できることがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度はモナドの次数付き!-持ち上げという構造を導入した。これは次数付きモナドと類似の構造を持ち、ReedとPierceらの計算型をエフェクトで拡張したものを解釈できる。しかも距離空間の圏において、確率分布モナドの !-持ち上げと、合成性とよばれる性質を満たす確率分布間の距離が丁度対応していることがわかった。これらは、エフェクトシステムの表示的意味論にまつわる新たな数学的構造の発見と、その特徴づけを与えた成果である。
|
| Strategy for Future Research Activity |
平成30年度にあげていた研究課題を含む以下の課題について引き続き取り組む予定である。
* 出力機能を付与した確率的プログラミング言語を用いて、様々なプログラム解析(コスト解析、実行時間解析)を確率的に拡張する方法を考察する。加えて、次数付きモナドの構造を盛り込み、コストや実行時間の期待値に関する見積もりを行える型システムの設計と意味論を考察する予定である。
* エフェクト変数の表示的意味論。エフェクト変数のあるエフェクトシステムはプログラムの副作用をより柔軟に見積もることができる。この機構の表示的意味論を、Lawvereの hyperdoctorineを参考にして与える予定である。この意味論の上に1) エフェクト多相性 2) エフェクトの再帰方程式の解釈を与え、より強力なエフェクトシステムのための表示的意味論を展開する予定である。また、新しく以下の研究課題についても取り組む予定である。
* エフェクトシステムとその双対であるコエフェクトシステムは、プログラムのコスト分析において同等な分析能力を持つことがEzgi Cicekらにより報告されている。本研究課題ではこの同等性の意味論的な対応物を次数付きコモナドと次数付きモナドの間の対応関係から説明することを検討する。
|
| Causes of Carryover |
当該年度は主にモナドの次数付き !-持ち上げについて研究した。この研究成果はエフェクトシステムの表示的意味論にまつわる数学的構造に貢献したものの、研究提案時に計画したエフェクト多相性とエフェクト再帰方程式に関する研究がまだ残っており、これらの研究を行うため、研究期間を延長することにした。
|
Research Products
(5 results)
