2017 Fiscal Year Research-status Report
相互作用の幾何の確率拡張――圏論的意味論からビッグデータへ
| Project/Area Number |
15K11984
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
蓮尾 一郎 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | プログラミング言語理論 / 確率的プログラミング言語 / 高階計算 / プログラム検証 / 確率的システム / 確率的システム検証 |
|---|
| Outline of Annual Research Achievements |
2017年度においては，獲得目標の一つである高階関数型確率的プログラムの静的解析アルゴリズムの開発に向けて，その基礎となる確率的状態機械および命令形プログラムの解析手法に特に注力して研究を継続した．国際会議予稿集論文として発表した論文 [Cirstea, Shimizu & Hasuo, CALCO’17], [Urabe, Hara & Hasuo, LICS’17] はこの方向の成果であり，圏論的定式化によって定性的なモデル検査アルゴリズムを定量的なアルゴリズムに拡張するものである．特に，理論計算機科学分野の旗艦国際会議で発表された後者の論文においては，圏論的一般論の具体化の一例として，確率的状態機械の可達性確率を定量的に下から近似する新奇な手法を与えた．近年確率的プログラミング言語の分野でマルチンゲールを基礎とした解析手法が盛んに研究されているが，前述の可達性確率近似手法はこれらと補完的関係にある手法である．これらのさまざまな解析手法について不動点理論の視点から理論的整理を行い，また自動解析アルゴリズムの理論整備と実装を行う論文を，現在準備中である [Takisaka, Oyabu, Urabe & Hasuo, in preparation]．
また，理論計算機科学分野の旗艦国際会議での予稿集論文 [Dal Lago, Tanaka, Yoshimizu, LICS’17] においては，並行計算を行う高階計算系を，複数トークンで拡張した GoI によって状態遷移系に翻訳する成果を得た．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2つの獲得目標（ハードウェア実装および静的解析アルゴリズム）に向けて，特に確率的状態機械の静的解析アルゴリズムの理論的基盤について顕著な進捗が見られる．これらの成果の高階関数型確率的プログラムへの拡張と，高階関数型確率的プログラムの回路への翻訳については，研究期間を延長して2018年度に重点的に取り組む．
|
| Strategy for Future Research Activity |
これまで順調に推移している研究を引き続き継続するとともに，残された課題（すなわち，静的解析アルゴリズムの高階関数型確率的プログラムへの拡張，および，高階関数型確率的プログラムの回路への翻訳）については新たな研究協力者と協働する．前者についてはすでに，フランスの研究者と相互訪問を通じて議論をおこなっている．後者については室屋晃子氏（京大数理研）に研究分担者として参加してもらい，研究をさらに推進する．
|
| Causes of Carryover |
（理由）計画していた海外出張がとりやめになったため．
（使用計画）残された課題の研究推進のため研究体制を拡大する．そのための旅費および物品購入に使用する．
|
