2017 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)の研究成果を得た.
(1)ファジィ関係を用いたデータベース理論の形式化:
博士課程大学院生(留学生)とともに研究を行なった. 関係計算を用いた定式化を与え, 2件の同値関係に関する結果を昨年5月と12月にインドネシアでの国際会議で発表した. ここでは, 関係データベース操作を具体的な関係計算式で与え, 種々の証明を関係計算式変形にて行う基礎を与えた. また, ファジィ関係における同値関係についても, 関係計算式による定式化と計算証明を与えている. また, 関係計算式を自動計算するソフトウェアの開発にも着手した.
(2) 圏論のモナドによる関係代数:
ウルトラフィルターモナドによる関係代数の圏が位相空間の圏と同型であることの証明を関係計算を用いた計算証明で行なった. 本結果と周辺分野の紹介をIMIオーストラリア分室が主催するメルボルンでの国際研究集会において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) 離散数学の形式化の視点から, 韓国釜山大学から九州大学フレンドシップ奨学生として滞在した研究生とともに群演算から定まるケーリーグラフに関わる研究討論を韓国Yeungnam大学における代数と組合せ論の研究集会, および, 日本数学会九州支部会において討論した.
(2) CG(Computer Graphics)における図形変形の正当性については, 修士課程大学院生らとともに, CG技術の実装と数理2017に参加し, 形式化された実装方法を考えるとともに, 最近のCG技術とそのソフトウェア実装について討論を行なった.
(3) 多項式による最適化問題の求解ソフトウェアは高速かつ高性能なものが, 既に開発されており, さまざまな論理問題についても, 多項式による最適化問題で定式化することで解を求める方法が様々提案されている. この方法論に論理的側面, また, 論理式変形による正当性証明の立場から, 論理式表現の混合整数計画問題への変換について, 修士課程大学院生らとともに着手し, 日本数学会主催の異分野・異業種交流会等の参加者らと討論を進めている.
|
| Strategy for Future Research Activity |
計画通り, 平成30年度は以下の既発表の3つの論文から得られる具体的な形式化の課題に着手する. 一方で, 既存研究を深めた結果を得るだけでなく, 別の視点から, アイデアや対象領域を広げる工夫も続ける.
課題1: 圏論のモナドに関する関係計算理論の形式化: モノイド作用の入った集合の圏をトポスと捉え関係計算を与える. 有限モノイドの作用の入った有限集合は計算プログラムで実現可能なので, この計算プログラムと形式理論のインターフェイスの構成が課題になる.
課題2: トポスをモデルにしたホーア論理によるプログラム検証体系の形式化: 本形式化では, 関係計算そのものの定式化において, 底となる圏を集合ではなく, 一般のトポスとする必要が生じる. それぞれの因果関係を調べること, 普遍性を調べることが課題となる.
課題3: グラフ変換理論の関係計算による定式化: 本形式化は, 関係の圏の定式化と同値である. 関係結合だけでなく, 圏としての性質, 例えば, プッシュアウトのような極限, 余極限に対応する対象の定式化が必要になる. この結果が形式化でき, 書き換え系の合流性などに応用可能になれば, 書き換え系の理論において新しい定理が見つかるかもしれない. それは, ともかく, 本研究課題の主題は計算プログラムとのインターフェースを活用した, 命題候補の反例の提示, あるいは, 命題候補になりえる命題の可能性の提示をすることであるので, ここでも具体的なグラフ変換プログラムと圏論の定理とのインターフェスを作り, その性質を考察することが主題になる.
|
| Causes of Carryover |
年度末出張の交通費(航空券)が見積りよりも安価であったため若干の残額が生じた。次年度は、結果が固まり、さらに研究発表の機会が増えるので、計画以上の旅費が必要となる見込みなので、その旅費に充当する。
|
