2019 Fiscal Year Annual Research Report
Mathematical Structures for Effect Systems
| 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. アルゴリズムの差分プライバシーの型理論的検証に関する研究をまとめた論文が、理論計算機科学のトップ国際会議であるLICS2019にて採択された。
2. 計算効果に関する距離の概念と、そのような距離から次数付きモナドを構成する方法について研究を行った。BartheらはPOPL2012で差分プライバシーの検証のためのホーア論理apRHLを導入した。その意味論は、確率分布間の距離の概念から構成される次数付きモナドにより与えられる。このシナリオを一般化し、モナドTによって記述される計算効果の間の距離の概念を導入し、それらを余稠密持ち上げにより次数付きモナドに拡張する方法を与えた。そして計算効果の距離を測ることのできるホーア論理と、その健全な意味論を与えた。
3. 与えられたシグネチャから次数付きモナドを生成する方法を研究した。モナドと代数理論の間の数学的な対応関係は1960年代頃に確立されている。これを次数付きモナドについて拡張することで、体系的に次数付きモナドを得ることが可能となると考察した。本研究では、研究代表者がPOPL2014で導入した代数的演算の概念をもとに、次数付きモナドを生成する方法を考察した。
4. ホーア論理をエフェクトシステムで拡張した論理に対する意味論を次数付き圏により与える方法を研究した。次数付き圏は次数付きモナドおよびコモナドのKleisli圏として自然に得られる、一般的な圏のクラスである。拡張されたホーア論理が自然に解釈できるよう、計算効果のモデルとして用いられるFreyd圏を次数付き圏に拡張する研究も行った。
|
