| 研究実績の概要 |
[片岡,蓮尾,長]システムの形式的な検証には，システムの意味論，および，仕様を記述する論理の意味論が必要となる。状態を持つシステムの仕様記述には時相論理が通常用いられ，その中でも様相μ計算のように最小不動点を利用する論理についての統一的な意味論を2013年に共同研究し国際会議で発表していた。システムの状態の型とその上の論理式について同時に不動点をとるこの研究の手法は，さらなる適用対象が見つかっている。当該年度は，2013年の会議の予稿集版を拡大し学会誌に投稿した。
[片岡,Pavlovic]データマイニングの基本は，2者間の関係から特徴量を抽出する方法論にある。特に，行列の固有値解析を用いる方法が実用化されているものの，特徴量あるいは関係性を線形にしかとらえていない点で，理論的な拡張の余地がある。この点に関し，データマイニングの基礎の圏論的拡張についての先駆的成果を発表していた研究者とともに2，3月に共同研究を行った。この研究ではデータマイニングへの応用としての意義と同時に，1960年代から問題となっていた圏の完備化の問題に新しい側面を提示するという純粋数学的な意義も得られた。この研究成果を3月に国際会議に概要投稿した。
[室屋,片岡,蓮尾,星野]プログラムを低レベルの実装，とくにFPGA等の電子回路基板として実装する際には，高級プログラミング言語からの自動変換技術（コンパイラ）が有効である。副作用を持つプログラムについての関数型言語から回路への自動変換の共同研究において，相互作用の幾何という理論を用いたコンパイラの試作機を完成させた。試作機ではデータとして表現した回路へ変換し，その表現の回路を汎用コンピュータ上でシミュレートする。この共同研究の理論上の重要性は，この分野で副作用を持つ場合が新規であることであり，応用上では，例えば確率的分岐という副作用を基本命令として持つ基板へのコンパイラの実現のために重要となる。
|
