2015 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 | 形式検証 / 特徴量抽出 / 特異値分解 / Dedekind-MacNeille完備化 / 様相不動点論理 / 余代数 |
|---|
| Outline of Annual Research Achievements |
コンピューター制御される物理システム（ハイブリッドシステム）について，その正しさを確かめることは近年の重要な課題である。とくに本研究では，純粋なコンピュータープログラムのための検証手法を適切に拡張してハイブリッドシステムの検証手法を作ることを最終的な目標としている。
トップダウンな仕様をボトムアップな部品組み立てが満たすかという問いについて，圏論的に取り扱う共同研究を2014年度から行っている。仕様の集合と部品の集合の間の単なる量的関係については，線形代数的な道具が特徴量抽出の手法として実用化までされている一方で，本研究は仕様同士や部品同士にも関係がある場合を含むよう一般化された理論を提案している点で新しい。質的関係については順序集合のDedekind-MacNeille完備化が知られていたが，その量的関係への一般化という純粋数学的な側面も本研究はもつ。共同研究の中での申請者の主要な貢献は，研究テーマと既存の圏論の道具との関連性を指摘した点，理論的結果の証明の半数程度，具体例計算に用いる新しい手法の発見と実際の計算などにわたる。また，当該年度に申請者が国際会議で口頭発表した。
システムが仕様を満たすかという問いについては，どのような仕様を記述できるのかが理論の実用性に大きくかかわる。仕様記述に不動点演算子をもつ論理を用いる場合は，システムが動作しつづけることや，後処理がいつか実行されることなどの仕様を書くことができる。圏論的に一般化された遷移システムの上でのこのような論理の解釈（意味論）に関しては2013年に共同研究し国際会議で発表しており，その学会誌版が当該年度に採録決定した。会議の予稿集版と比較して，最大不動点と最小不動点の両方について理論や具体例を議論するなどの内容が追加されている。申請者は，追加内容の理論構築や具体例計算，予稿集版の証明の簡略化，そして執筆のすべてにおいて中心的な役割を果たした。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
超準解析は，連続量に関わる問題を離散的な議論に帰着する手法のひとつであり，申請者は，ハイブリッドシステムの検証を通常のコンピュータプログラムの検証に帰着させるアプローチとして注目している。とくに，プログラム意味論を与えるための領域理論との関連において直観主義超準解析についての研究を進めている。超準解析における一階論理と高階論理の性質の差の利用という観点で上部構造を持つ超準解析の言語と圏モデルを研究しており，当該年度は，代数的集合論という，集合とクラスを区別して圏論的に公理化する理論との類似から考察を進め，国内外の研究者と議論を行った。
圏論的な特徴量抽出の理論については，国際会議での発表の後，圏論的意義についての研究が進展している。とくに，随伴関手とモナドの関係についての基礎的な事項は1960年代にさかんに研究されていたにも関わらず，共同研究において新しい数学的結果を得ている。
不動点論理についての圏論的研究については，提案していた枠組みを理論的に精密化することができた。
具体的には，型レベルと命題レベルで同時に不動点をとる構成のためには，それぞれのレベルで不動点がとれる構造の他に何を用いるのが自然かを明らかにした。
|
| Strategy for Future Research Activity |
[Eliasson 2003]によれば，直観主義超準解析のモデルとなるfilter constructionの後に二重否定位相を用いることで古典超準解析のモデルとなるultrafilter constructionを特徴づけることもできる。これは古典論理を直観主義論理に二重否定埋め込みする結果を適用しただけのようでいて，彼の研究では，Nelsonによる（公理的な古典超準解析である）Internal Set Theoryのモデルをより圏論的に与えることに成功している。層を用いる直観主義超準解析のモデルが申請者の目標であるものの，Robinsonによる超準解析の最初のモデルと比較する中間地点として，層を用いる古典超準解析のモデルとの詳細な比較をしたい。
不動点論理については，理論的には圏の双対性の利用で解決されたように見える問題も，検証のために不動点を下からおさえる文脈では最大不動点と最小不動点で異なる方法が必要となる。このような実用性の観点において，現在の理論的枠組みをどのように利用できるかについてさらなる研究を行いたい。
|
