| Co-Investigator(Kenkyū-buntansha) |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
|
|---|
| Strategy for Future Research Activity |
令和５年度, MathComp-Analysisが提供する実解析の拡張を行う. 具体的に, 連続確率論の形式化の継続として, 基本的な分布(正規分布など)の形式化し, 確率分布間の距離の形式化を行う. また、積分と微分の関係を明らかにする定理(微分積分学の基本定理など)の形式化を行う. さらに, ベクトル空間の一般的な形式化を行い, 積分の形式化をLp空間で抽象化し, 微分の形式化を多変数へ拡張する. 以上の拡張によって, 例えば, ロボティクスの基礎となる幾何学と運動学の形式化が可能となる.
確率や非決定性などを扱うプログラミング言語の機能の意味論について形式化を見据えた理論を構築する. 令和５年度, その形式基盤を充実する. 令和４年度の確率的一階プログラミング言語の形式化を完成させる. 疑ボレル空間及びその一般論として具体層の形式化を行い, 高階関数を扱うようにする. そのため, MathComp-Analysisによる可測空間の拡張が必要である. また, 量化代数的推論とローヴェア理論を取り組むことによって, プログラム検証のための等式推論の基盤を整備する. また、令和４年度に開発した一般的なモナドの持ち上げを、標準的な差分プライバシーにより具体化してプログラム論理を導出し、いくつかのアルゴリズムの差分プライバシー検証をその中で行う。
様々な副作用を伴うプログラムに対し, 定理証明支援系Coq上において, プログラム検証を可能とするMonaeという形式基盤を開発してきた. 令和５年度, Monaeの汎用性を改善する. とくに, 連続確率分布に基づく確率的プログラムの検証を可能にする. そのため, 上記のMathComp-Analysisと連携し, 測度モナドを形式化する. 連続確率分布を考慮した等式推論を実現し, 超分布や高階関数などを扱える確率的プログラムの検証をサポートする.
|
