2018 Fiscal Year Research-status Report
関係計算の形式化を用いた数学とソフトウェア検証のための理論構築
| Project/Area Number |
17K05346
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 数理論理学 / 関係計算 / 形式証明 / 形式手法 / モデル検査 / 圏論のモナドの形式化 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は, 高信頼ソフトウェア開発の基礎となる数理論理学や離散数学, 特に計算機による自動検証可能な形式証明を意識した, 関係計算による証明を用いた数学体系を広けることである. 今年度計画にある結果としては関係計算理論の形式化に関して, 次の(1),(2),(3)の研究成果を得た.
(1) 圏論のモナドに関する関係計算理論の形式化として, モノイド作用の入った集合の圏をトポスと捉え関係計算を考え定式化, および, 計算プログラムの形式検証のための領域としての考察を行なった. (2) トポスをモデルにしたホーア論理によるプログラム検証体系の形式化として, 関係計算そのものの定式化において, 底となる圏を集合ではなく, 一般のトポスに拡張した体系について形式的に定式化した. その中で, いくつかの普遍性の形式化についての考察を行なった. (3) グラフ変換理論の関係計算による定式化として, 関係の圏でのプルバックやプッシュアウトのような極限, 余極限に対応する対象の形式的な定式化を整理した. 具体的なグラフ変換プログラムと圏論の定理とのインターフェスについては, 継続して精査中である.
さらに、海外、および、他大学の大学院生らと、いくつかの研究集会において関係計算理論の定式化と形式化について議論を重ねることにより、関係計算理論と圏論を応用したソフトウェア検証についてのアイデアを深めることが出来た。また、ゲーム・ソフトウェアのモデル検査に関連した関係計算理論と圏論の応用可能性についての議論を深めることが出来た.
|
| 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) JSPSサマープログラムにおいて英国UCLから私の研究室を訪問した博士課程研究生とともに部分関数の圏論を用いた代数的形式化についての研究を進めた. その結果は, 佐世保高専で開催されたIndustrial Math Seminarにおいて発表し議論を深めた.
(2) CG(Computer Graphics)における図形変形の正当性については, 2名の修士課程大学院生らとともに研究を続け, 第1回論理と計算セミナーを開催し, そのソフトウェア実装について討論を行なった.
(3) ゲーム開発会社とのゲームソフトウェアの正当性に関するモデル検査に関する共同研究に着手し、最初のアイデアが、CEDEC2018(Computer Enterteinment Developer Developers Conference)にて公表された. 本手法についての形式検証について議論を深めることが出来た.
|
| Strategy for Future Research Activity |
計画通り, 平成31年度は平成30年度に続き, 以下の既発表の3つの論文から得られる具体的な形式化の課題に着手する.また, 計算実験環境としての関係計算システムの完成も目指す.
課題1: 圏論のモナドに関する関係計算理論の形式化: モノイド作用の入った集合の圏をトポスと捉え関係計算を与える. 有限モノイドの作用の入った有限集合 は計算プログラムで実現可能なので, この計算プログラムと形式理論のインターフェイスの構成が課題になる.
課題2: トポスをモデルにしたホーア論理によるプログラム検証体系の形式化: 本形式化では, 関係計算そのものの定式化において, 底となる圏を集合ではなく, 一般のトポスとする必要が生じる. それぞれの因果関係を調べること, 普遍性を調べることが課題となる.
課題3: グラフ変換理論の関係計算による定式化: 本形式化は, 関係の圏の定式化と同値である. 関係結合だけでなく, 圏としての性質, 例えば, プッシュアウトのような極限, 余極限に対応する対象の定式化が必要になる. この結果が形式化でき, 書き換え系の合流性などに応用可能になれば, 書き換え系の理論において新しい定理が見つかるかもしれない. それは, ともかく, 本研究課題の主題は計算プログラムとのインターフェースを活用した, 命題候補の反例の提示, あるいは, 命題候補になりえる命題の可能性の提示をすることであるので, ここでも具体的なグラフ変換プログラムと圏論の定理とのインターフェスを作り, その性質を考察することが主題になる.
|
| Causes of Carryover |
次年度は最終年度であるので成果取りまとめのための共同研究機会の拡大、および、成果発表のための出張旅費に充当する予定である。
|
