| 研究課題/領域番号 |
15K00014
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2020-03-31
|
| キーワード | エフェクトシステム / 次数付きモナド / 差分プライバシー / 次数付きコモナド / 計算効果 |
|---|
| 研究実績の概要 |
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)-差分プライバシーを表現できることがわかった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度はモナドの次数付き!-持ち上げという構造を導入した。これは次数付きモナドと類似の構造を持ち、ReedとPierceらの計算型をエフェクトで拡張したものを解釈できる。しかも距離空間の圏において、確率分布モナドの !-持ち上げと、合成性とよばれる性質を満たす確率分布間の距離が丁度対応していることがわかった。これらは、エフェクトシステムの表示的意味論にまつわる新たな数学的構造の発見と、その特徴づけを与えた成果である。
|
| 今後の研究の推進方策 |
平成30年度にあげていた研究課題を含む以下の課題について引き続き取り組む予定である。
* 出力機能を付与した確率的プログラミング言語を用いて、様々なプログラム解析(コスト解析、実行時間解析)を確率的に拡張する方法を考察する。加えて、次数付きモナドの構造を盛り込み、コストや実行時間の期待値に関する見積もりを行える型システムの設計と意味論を考察する予定である。
* エフェクト変数の表示的意味論。エフェクト変数のあるエフェクトシステムはプログラムの副作用をより柔軟に見積もることができる。この機構の表示的意味論を、Lawvereの hyperdoctorineを参考にして与える予定である。この意味論の上に1) エフェクト多相性 2) エフェクトの再帰方程式の解釈を与え、より強力なエフェクトシステムのための表示的意味論を展開する予定である。また、新しく以下の研究課題についても取り組む予定である。
* エフェクトシステムとその双対であるコエフェクトシステムは、プログラムのコスト分析において同等な分析能力を持つことがEzgi Cicekらにより報告されている。本研究課題ではこの同等性の意味論的な対応物を次数付きコモナドと次数付きモナドの間の対応関係から説明することを検討する。
|
| 次年度使用額が生じた理由 |
当該年度は主にモナドの次数付き !-持ち上げについて研究した。この研究成果はエフェクトシステムの表示的意味論にまつわる数学的構造に貢献したものの、研究提案時に計画したエフェクト多相性とエフェクト再帰方程式に関する研究がまだ残っており、これらの研究を行うため、研究期間を延長することにした。
|
