相互作用の幾何の確率拡張――圏論的意味論からビッグデータへ

2015 年度 実施状況報告書

• 研究課題/領域番号: 15K11984
• 研究機関: 東京大学
• 研究代表者: 蓮尾 一郎 東京大学, 情報理工学(系)研究科, 准教授 (60456762)
• 研究分担者: 星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
• 研究期間 (年度): 2015-04-01 – 2018-03-31
• キーワード: プログラミング言語理論 / 表示的意味論 / 操作的意味論 / 抽象機械 / 高階計算 / 確率的プログラミング / 圏論 / 線形論理

研究実績の概要

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 抽象機械を行列として表現することによってさまざまな問題を線形計画法に帰着するというアイデアを得て，研究を開始した．

現在までの達成度 (区分)

2: おおむね順調に進展している

理由

挑戦的目標をかかげた本研究において，当初設定した獲得目標の達成に向け着実にサーベイや理論上の準備的知見，さらにプロトタイプ実装を積み重ねている．理論的研究については特に関連する（GoI や余代数に関する）一般論についてブレイクスルー的成果が生まれており，それら理論的成果の本研究目標への貢献が今後期待される．

今後の研究の推進方策

これまで順調に推移している研究を引き続き継続するとともに，特にハードウェア実装について，豊富な研究開発経験を持つ海外の研究者との協働を模索する（すでに準備的議論を開始している）．

次年度使用額が生じた理由

計画した旅費の額と実際の額の間に誤差が生じた．

次年度使用額の使用計画

物品費または旅費に充当する．

研究成果

• [国際共同研究] Univ. Bologna/INRIA Sophia Antipolis/hoge/hoge(イタリア)
  • 国名: イタリア
  • 外国機関名: Univ. Bologna/INRIA Sophia Antipolis/hoge/hoge
• [国際共同研究] University of Paris VII/Verimag(フランス)
  • 国名: フランス
  • 外国機関名: University of Paris VII/Verimag
• [国際共同研究] Radboud University(オランダ)
  • 国名: オランダ
  • 外国機関名: Radboud University
• [国際共同研究] University of Southampton/University of Bath(英国)
  • 国名: 英国
  • 外国機関名: University of Southampton/University of Bath
• [雑誌論文] Healthiness from Duality (2016)
  • 著者名/発表者名: Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
  • 雑誌名: Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016) 巻: - ページ: 682-691
  • DOI: 10.1145/2933575.2935319
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Semantics of Higher-Order Quantum Computation via Geometry of Interaction (2016)
  • 著者名/発表者名: Ichiro Hasuo and Naohiko Hoshino
  • 雑誌名: Annals of Pure and Applied Logic 巻: 未定 ページ: 未定
  • 査読あり / 謝辞記載あり
• [雑誌論文] Special Issue on Quantum Physics and Logic (QPL 2014) (2016)
  • 著者名/発表者名: Ichiro Hasuo and Prakash Panangaden, editors
  • 雑誌名: New Generation Computing 巻: 34 ページ: 1-152
  • DOI: 10.1007/s00354-016-0200-7
  • 国際共著
• [雑誌論文] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
  • 雑誌名: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 巻: なし ページ: 718-732
  • DOI: 10.1145/2837614.2837673
  • 査読あり / 国際共著
• [雑誌論文] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • 著者名/発表者名: Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
  • 雑誌名: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 巻: なし ページ: 748-760
  • DOI: 10.1145/2837614.2837672
  • 査読あり / 謝辞記載あり
• [雑誌論文] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (2016)
  • 著者名/発表者名: Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
  • 雑誌名: Proc. Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Lecture Notes in Computer Science 巻: 9583 ページ: 229-249
  • DOI: 10.1007/978-3-662-49122-5_11
  • 査読あり / 国際共著
• [雑誌論文] Near-Optimal Scheduling for LTL with Future Discounting (2016)
  • 著者名/発表者名: Shota Nakagawa and Ichiro Hasuo
  • 雑誌名: Proc. Trustworthy Global Computing - 10th International Symposium, TGC 2015, Lecture Notes in Computer Science 巻: 9533 ページ: 112-130
  • DOI: 10.1007/978-3-319-28766-9_8
  • 査読あり
• [雑誌論文] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 雑誌名: Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, LIPIcs 巻: 35 ページ: 320-335
  • DOI: 10.4230/LIPIcs.CALCO.2015.320
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Generic Weakest Precondition Semantics from Monads Enriched with Order (2015)
  • 著者名/発表者名: Ichiro Hasuo
  • 雑誌名: Theoretical Computer Science 巻: 604 ページ: 2-29
  • DOI: 10.1016/j.tcs.2015.03.047
  • 査読あり
• [雑誌論文] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 雑誌名: Proc. Computer Aided Verification - 27th International Conference, CAV 2015, Lecture Notes in Computer Science 巻: 9207 ページ: 356-374
  • DOI: 10.1007/978-3-319-21668-3_21
  • 査読あり
• [学会発表] Healthiness from Duality (2016)
  • 著者名/発表者名: Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
  • 学会等名: Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
  • 発表場所: New York City, USA
  • 年月日: 2016-07-05 – 2016-07-08
  • 国際学会
• [学会発表] Coalgebras and Higher-Order Computation: a GoI Approach (2016)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
  • 発表場所: Porto, Portugal
  • 年月日: 2016-06-22 – 2016-06-26
  • 国際学会 / 招待講演
• [学会発表] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
  • 学会等名: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-20 – 2016-01-23
  • 国際学会
• [学会発表] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • 著者名/発表者名: Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
  • 学会等名: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-20 – 2016-01-23
  • 国際学会
• [学会発表] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (2016)
  • 著者名/発表者名: Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
  • 学会等名: Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-17 – 2016-01-19
  • 国際学会
• [学会発表] Near-Optimal Scheduling for LTL with Future Discounting (2015)
  • 著者名/発表者名: Shota Nakagawa and Ichiro Hasuo
  • 学会等名: Trustworthy Global Computing - 10th International Symposium, TGC 2015
  • 発表場所: Madrid, Spain
  • 年月日: 2015-08-31 – 2015-09-01
  • 国際学会
• [学会発表] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 学会等名: Computer Aided Verification - 27th International Conference, CAV 2015
  • 発表場所: San Fransisco, CA, USA
  • 年月日: 2015-07-18 – 2015-07-24
  • 国際学会
• [学会発表] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 学会等名: 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
  • 発表場所: Nijmegen, the Netherlands
  • 年月日: 2015-06-24 – 2015-06-26
  • 国際学会
• [図書] 圏論の歩き方 (2015)
  • 著者名/発表者名: 圏論の歩き方委員会 (編集)
  • 総ページ数: 295
  • 出版者: 日本評論社
• [備考] 東京大学蓮尾研ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/
• [備考] 研究代表者個人ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/