2014 Fiscal Year Annual Research Report
超準モデル構成のトポス理論的一般化と，ハイブリッドシステム検証への応用
| Project/Area Number |
14J09142
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
片岡 俊基 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2014-04-25 – 2017-03-31
|
| Keywords | 圏論的論理 / 形式検証 / 様相論理 / データマイニング / 完備化 / コンパイラ / 相互作用の幾何 |
|---|
| Outline of Annual Research Achievements |
[片岡,蓮尾,長]システムの形式的な検証には，システムの意味論，および，仕様を記述する論理の意味論が必要となる。状態を持つシステムの仕様記述には時相論理が通常用いられ，その中でも様相μ計算のように最小不動点を利用する論理についての統一的な意味論を2013年に共同研究し国際会議で発表していた。システムの状態の型とその上の論理式について同時に不動点をとるこの研究の手法は，さらなる適用対象が見つかっている。当該年度は，2013年の会議の予稿集版を拡大し学会誌に投稿した。
[片岡,Pavlovic]データマイニングの基本は，2者間の関係から特徴量を抽出する方法論にある。特に，行列の固有値解析を用いる方法が実用化されているものの，特徴量あるいは関係性を線形にしかとらえていない点で，理論的な拡張の余地がある。この点に関し，データマイニングの基礎の圏論的拡張についての先駆的成果を発表していた研究者とともに2，3月に共同研究を行った。この研究ではデータマイニングへの応用としての意義と同時に，1960年代から問題となっていた圏の完備化の問題に新しい側面を提示するという純粋数学的な意義も得られた。この研究成果を3月に国際会議に概要投稿した。
[室屋,片岡,蓮尾,星野]プログラムを低レベルの実装，とくにFPGA等の電子回路基板として実装する際には，高級プログラミング言語からの自動変換技術（コンパイラ）が有効である。副作用を持つプログラムについての関数型言語から回路への自動変換の共同研究において，相互作用の幾何という理論を用いたコンパイラの試作機を完成させた。試作機ではデータとして表現した回路へ変換し，その表現の回路を汎用コンピュータ上でシミュレートする。この共同研究の理論上の重要性は，この分野で副作用を持つ場合が新規であることであり，応用上では，例えば確率的分岐という副作用を基本命令として持つ基板へのコンパイラの実現のために重要となる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
年次計画の通り，コンピュータ科学における様々な課題に関して，圏論の適用先を幅広く調査することができた。システム検証の論理の理論の他にも，コンパイラの理論やデータマイニングの理論に関しても理解を深めるとともに結果を得ており，トポス理論的あるいは超準解析的なアプローチのためには受けの広い布石にできた。
当該年度に発表に至った結果は国際ワークショップ発表1本であるものの，国際会議論文2本と学術誌論文1本が投稿中であり，単純な成果の量としても十分である。
|
| Strategy for Future Research Activity |
引き続き，システム検証に関する汎用性のある定式化を圏論の視点から試みる。
また，修士論文で研究した直観主義超準解析に関する成果を学術誌に投稿する。これに関連して，synthetic domain theoryでモデルとして用いられる圏Effective toposに対する具体的な計算方法を探す。
|
