超準モデル構成のトポス理論的一般化と，ハイブリッドシステム検証への応用

点击翻译按钮获取中文摘要

コンピューター制御される物理システム（ハイブリッドシステム）について，その正しさを確かめることは近年の重要な課題である。とくに本研究では，純粋なコンピュータープログラムのための検証手法を適切に拡張してハイブリッドシステムの検証手法を作ることを最終的な目標に設定していた。本研究計画では[末永&蓮尾'11]のように超準解析を用いるアプローチを拡張するために，直観主義超準解析をよりよく研究することが必要と考えた。直観主義超準解析の先行研究について，[Moerdijk'95]に始まる研究ではトポスが主役として用いられていた一方，[Butz'04]ではトポスの場合の結果は一部でしかない。当初の研究計画ではトポスを重視していたが，それに限らない直観主義超準解析の研究を進めている。今年度は，圏論的な超準解析（これは直観主義論理の場合を含む）について，申請者が行った研究の一部分をまとめ，圏論に関する国際会議であるCT (International Category Theory Conference) にて発表した。申請者の発表はplenary sessionで行われた。ここで発表した結果は，[Butz'04]で与えられた論理と圏モデルをファイブレーションという圏論の道具を用いて再調査し新しい特徴付けを得たというものである。申請者がDC1採用されていた2年8ヶ月の業績をまとめると，「圏による極限的振舞いの検証」について3つの結果を得たと言える。今年度に発表した超準解析の結果は「無限小」などの超実数を論理に加えることが圏に何を加えることで達成されるのかであったことの他に，前年度までの結果として，無限に続く遷移を扱うための不動点論理に対応する圏に関する結果と，形式概念解析に対応して圏の双完備化（極限と余極限を適切に付加する）を得た結果がある。