Project/Area Number |
15K11984
|
Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
Allocation Type | Multi-year Fund |
Research Field |
Theory of informatics
|
Research Institution | National Institute of Informatics (2017-2018) The University of Tokyo (2015-2016) |
Principal Investigator |
Ichiro Hasuo 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
Co-Investigator(Kenkyū-buntansha) |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
室屋 晃子 京都大学, 数理解析研究所, 助教 (00827454)
|
Project Period (FY) |
2015-04-01 – 2019-03-31
|
Project Status |
Completed (Fiscal Year 2018)
|
Budget Amount *help |
¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2015: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
Keywords | プログラミング言語理論 / 確率的プログラミング言語 / 高階計算 / プログラム検証 / 確率的システム / 確率的システム検証 / 統計的機械学習 / 表示的意味論 / 操作的意味論 / 抽象機械 / 確率的プログラミング / 圏論 / 線形論理 |
Outline of Final Research Achievements |
We implemented a token-machine simulator of a (discrete) probabilistic functional programming language. We designed a language and an execution model for functional programming that allows parameter updating during program execution, and we gave a prototype implementation of the language. We constructed a denotational semantics for a probabilistic functional programming language with soft conditioning mechanism. This is the first intensional semantics for a probabilistic functional programming language. As an unexpected result, we obtained a lattice-theoretic/category-theoretic framework for the definition of martingale.
|
Academic Significance and Societal Importance of the Research Achievements |
データサイエンスにおける個々のモデルや応用例から独立した汎用処理系・静的解析手法というブレイクスルー達成に向け、数学的基盤の構築とその応用のさきがけとなるプロトタイプ実装を行った。われわれの研究成果は相互作用の幾何という論理学的成果及びその圏論的一般化に基づく理論的手法の社会応用であり、論理学および圏論のもたらす一般性・汎用性に根ざしたデータサイエンスに革新をもたらすための着実な進展である。
|