2016 Fiscal Year Research-status Report
| Project/Area Number |
16K21557
|
|---|
| Research Institution | Sojo University |
|---|
Principal Investigator |
津曲 紀宏 崇城大学, 総合教育センター, 助教 (70632834)
|
|---|
| Project Period (FY) |
2016-04-01 – 2018-03-31
|
| Keywords | 確率的システム / 意味論 / 関係理論 / 圏論 / 代数 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，確率的システムのための定量的な検証手法を提供しうる代数を提案することである。そのため本研究では，セガラシステムの等価性について健全かつ完全な公理系の構築とその公理系の有効性の確認を行うことにしている。今年度の研究成果は下記の通りである。
１．セガラシステムの特殊な例である確率多重関係について，システムの逐次合成などの演算を関係理論の枠組みで解析した既存の結果 [Tsumagari et al, JLAMP, 2014]を拡張することに成功した。ここでは「全域性」という条件を排除するという一般化を行っており，近日中にその研究結果をまとめ発表する予定である。
２．１の結果は，[Furusawa et al, RAMiCS, 2015]の結果を拡張することで与えられた。具体的には，確率多重関係における逐次合成を，二項多重関係のPeleg合成の一般化として与えた。この二項多重関係について，Kleisli合成・Parikh合成・Peleg合成に関する議論をより深めた論文を投稿中である。また，同内容については国内研究集会で口頭発表を行っている。
３．１，２の過程で，関係理論における選択公理の取り扱いが問題となった。そこで，関係計算の抽象化であるデデキント圏にいくつか公理を加えたカントール圏を提案し，カントール圏において選択公理を形式化した。また，この枠組みにおいて，選択公理とツォルンの補題の等価性についても明らかにした。この研究成果は論文にまとめられ，現在投稿中である。
４．２で扱った二項多重関係は２人ゲームの意味論やプログラムの述語変換子意味論など，様々な文脈で登場する。種々の多重関係を包括的に扱うべく，圏論を用いた一般化を行い，多値多重関係を提案した。未確認ではあるが，確率多重関係など確率システムのモデルも多値多重関係の具体例であることが予想される。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
平成28年度は確率的システムのモデルの１つであるセガラシステムについて，その軌跡意味論に対する確率的正規表現を提案する予定であったが，セガラシステムの特殊な例である確率多重関係の解析が進んだためこちらを優先する形となった。また，その結果は二項多重関係という確率的ではないモデルに関する結果の一般化となっており，確率に付随する定量的な要素が現れる箇所を特定したという見方もできる。また，その他にも複数の関連研究で成果が出ており，申請時の計画からは遅れが生じているものの，今後の計画遂行に有用な結果が得られている。
|
| Strategy for Future Research Activity |
今後は，既定の路線に戻り，前年度までに遂行できなかった研究を行う。具体的には，以下のことを追究する。
１．セガラシステムの等価性に対する確率的な正規表現を提案し，システムと正規表現の間のクリーニの定理を証明する。証明が困難である場合は正規表現を随時改善する。
２．正規表現上の公理系として，等式・ホーン節の集合を与える。公理系の構築は，McIverらの確率クリーニ代数 (pKA) や研究協力者の知見を参考にしながら行う。また，与えた公理系の健全性・完全性を証明する。
３．新しい代数を用いた自動定理証明などの実験を行ない，代数の有効性を確認する。実験ではIsabelleやProver9などの自動定理証明器を用いる。
|
| Causes of Carryover |
以下の事由により，使用計画が変更されたため，差額が生じることとなった。
・研究打ち合わせのための海外渡航を予定していたが実現しなかった。
・次年度購入予定だった物品を前倒しで購入した。
|
| Expenditure Plan for Carryover Budget |
国際会議出席のための海外渡航費の一部とする。
|
Research Products
(4 results)
