研究課題
本研究の最終目的たる計算機システムの正しさの数学的保証に向けて，当初計画のアプローチを変更したものの，基礎的な結果を得た．具体的には以下のとおりである．当初計画では，システムの要素還元的（「モジュラーな」）設計手法を数学的に余代数と小宇宙原理によって表現し，これを様相論理の数学的表現であるストーン双対性と組み合わせることによって，計算機システムのモジュラーな仕様記述・検証の手法を目指した．しかし研究を進めるうちに，次のような関連した話題に関して新しい知見が得られた．すなわち，システム検証という応用面における，リアクティブ・システムの仕様記述と検証のための不動点論理（LTL やμ計算など）の重要性であり，また，その数学面では，論理の圏論的モデルとしてストーン双対性の代替となるファイブレーションの概念である．特にファイブレーションは Lawvere 以来圏論的論理の基本的構造として用いられ，ストーン双対性よりもさらに一般的な状況に適用できる．これらの概念に対する新しい知見を発展させ，ファイブレーションの表す論理の上で余帰納的述語（主に安全性仕様の記述に用いられる）を定式化し，さらにその余帰納的述語の具体的な再帰的構成法（ωチェインによる）と，この再帰が飽和するための一般的な十分条件を圏論の言葉で与えた．この十分条件はファイブレーションと locally presentable category という，これまであまり交わりのなかった圏論の2つのトピックの融合によってもたらされたものである．以上のように研究実績は当初計画とは方向の違うものになったが，計算機システムの品質保証という最終目的に対しては，かえって重要性の高いものであると考える．当初計画の中にあって今回の成果の中で考察されなかったモジュラー性については，今回の成果に立脚したさらなる研究が期待される．
すべて 2013 2012 その他
すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (4件) (うち招待講演 1件) 図書 (1件)
Proc. POPL
ページ: 417-430
doi:10.1145/2429069.2429120
Proc. Mathematical Foundations of Programming Semantics, Twenty-ninth Conference, MFPS 2013, Electronic Notes in Theoretical Computer Science
巻: 未定 ページ: 未定
Proc. Computer Aided Verification - 24th International Conference, Lecture Notes in Computer Science
巻: 7358 ページ: 462-478
10.1007/978-3-642-31424-7_34
