2015 Fiscal Year Research-status Report
相互作用の幾何の確率拡張――圏論的意味論からビッグデータへ
| Project/Area Number |
15K11984
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 准教授 (60456762)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | プログラミング言語理論 / 表示的意味論 / 操作的意味論 / 抽象機械 / 高階計算 / 確率的プログラミング / 圏論 / 線形論理 |
|---|
| Outline of Annual Research Achievements |
2015年度においては理論面での大きな進展があり，この成果がプログラミング言語分野のトップ国際会議に採択され発表した [室屋・星野・蓮尾，POPL’16]．この論文では，本研究の基盤となった [星野・室屋・蓮尾，CSL-LICS’14] の枠組みに再帰計算を導入し，Plotkin-Power 流の計算副作用付き操作的意味論との対応（妥当性 adequacy）を示した．この成果は，本研究の基礎となる GoI 抽象機械の（数学的に定義された）振る舞いがプログラミング言語的見地から自然・妥当なものであることを示すものであり，今後の研究の理論的基盤をさらに強化する結果として重要である．
上記とは別の理論的進展として，（確率的分岐などの）さまざまな「分岐」を持つプログラム及びシステムの解析・検証手法として，クライスリ圏の中の余代数の理論の研究を発展させた．たとえば [卜部・蓮尾，CALCO’15] においては，[蓮尾，CONCUR’06] のクライスリ模倣の概念が，システムの生成する（無限語や無限木などの）無限トレースの包含関係に対しても健全であることを一般的に示した．この理論の次の大きな一歩として，Buechi 及び parity 受理条件を持つシステムに対しての研究も行った．
確率的プログラム処理系の専用ハードウェア実装の目標に対しては，前年度得られたコンパイラ及びシミュレータを洗練し，web インターフェイスを作成して公開した（http://koko-m.github.io/TtT/）．専用ハードウェア実装の基礎となるであろうこのツールについては，上記 POPL 論文の発表時にも言及し，多数の聴衆の興味を集めた．
確率的プログラムの一般静的解析アルゴリズムの目標に対しては，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
挑戦的目標をかかげた本研究において，当初設定した獲得目標の達成に向け着実にサーベイや理論上の準備的知見，さらにプロトタイプ実装を積み重ねている．理論的研究については特に関連する（GoI や余代数に関する）一般論についてブレイクスルー的成果が生まれており，それら理論的成果の本研究目標への貢献が今後期待される．
|
| Strategy for Future Research Activity |
これまで順調に推移している研究を引き続き継続するとともに，特にハードウェア実装について，豊富な研究開発経験を持つ海外の研究者との協働を模索する（すでに準備的議論を開始している）．
|
| Causes of Carryover |
計画した旅費の額と実際の額の間に誤差が生じた．
|
| Expenditure Plan for Carryover Budget |
物品費または旅費に充当する．
|
-
-
-
-
-
[Journal Article] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
-
Journal Title
Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Volume: -
Pages: 682-691
DOI
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
[Presentation] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
Organizer
Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Place of Presentation
New York City, USA
Year and Date
2016-07-05 – 2016-07-08
Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
