2021 Fiscal Year Annual Research Report
観測モードに依らないシステム解析アルゴリズムの開発：ファイバー圏によるアプローチ
| Project/Area Number |
21J13334
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
小森田 祐一 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2021-04-28 – 2023-03-31
|
| Keywords | モデル検査 / 確率的システム / 圏論 / 余代数 / ファイバー圏 |
|---|
| Outline of Annual Research Achievements |
本研究では、状態遷移システムの分析に関し、同値関係、距離などの観測モードに依らない形での理論の定式化・実証コードの実装を目指している。
理論部分については、共同研究として、過去にLICS2019にて発表した論文のジャーナル版の提出と、LICS2021論文の発表・口頭発表を行った。LICS2019論文ジャーナル版については、本研究の基礎のひとつである「観測モードをファイバー圏と関手の持ち上げにより表す」という定式化を、新たな観測モードの例を複数挙げて行った。特に双模倣同値関係については、LICS2019論文では「ひとつのシステムの異なる状態の間の関係」しか直接は扱えなかったが、今回「ふたつのシステムから各々取り出した状態の間の関係」を扱うことができるようになり、これは「状態遷移システムの学習」という本研究の目標にとっては無くてはならないものである。LICS2021論文においては、本研究のもう一つの基礎である「状態遷移システムの性質を多値様相論理により記述する」という定式化に関係して、そのような様相論理が十分な表現力を持つための条件を一般的な形で定式化した。令和4年度はこれらから新たに得られた実例等を足掛かりに、比較・学習アルゴリズムの抽象的定式化を目指す。
実装部分については、圏論的に定式化されたアルゴリズムが実装された例について、予備的な調査を行っている。当初はふたつのアプローチ、「システムや観測モードの種類を実装言語のポリモーフィズムで実現する」と「システムや観測モードの種類にかかわらず実装言語ではある一つのデータ型を用いる」を検討しており、どちらかを後で選ぶという方針であったが、申請書提出以後の研究[Kori+, preprint 2022]も参考にした結果、前者が適切であろうと現在は考えている。令和4年度は、理論側の進捗に合わせ、具体的な実装を行っていく予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
本研究はアルゴリズムの理論的・抽象的な定式化と、実際の実装とからなるが、研究の進捗が遅れている理由は主に前者の理論部分にある。より詳細に言えば、統一しようとした既存のアルゴリズムたちの間の違いが、申請者の予想に比べて非常に大きかったことが影響している。
同値関係などの質的な対象の計算において、現在主流となっているアルゴリズムの大きな流れは、初めにシステムの全てを同一視した状態から始め、システムの動作の観測結果により、徐々に区別をつけていく、というものである。一方、距離などの量的な対象の計算においては、それとは逆に、初めにシステム内を全て区別し、その後、計算により同一視できる・近づけられる部分を特定していく、という手法をとる。この違いはファイバー圏を用いた抽象的定式化においても消えることはなく、むしろ「上からの近似」と「下からの近似」という、互いにまったく逆のアプローチであることが、抽象的定式化によりますます明らかになる。
これにより、「質的な計算と量的な計算を統合する」という本研究の目標の一つは不可能となった。
|
| Strategy for Future Research Activity |
上記「現在までの進捗状況」内「理由」に述べた通り、当初の計画通りの研究は困難である。そのため理論面において方針を転換し、以下の二つの目標を立てて研究を行うこととする。
一つは、質的計算と量的計算で、効率的なアプローチが異なる理由を、抽象的理論から説明づけることである。二つの状況は、数学的構造として見ればよく似ているため、既存の効率的なアプローチが異なっている理由は、それら構造のある種の不変量の違いとして定式化されうると考えられる。ひとつの具体的予想は、ファイバー圏として定式化した際の各ファイバーの「高さ」の違いが、これらをもたらすのではないかというものである。
もう一つは、質的計算と量的計算、それぞれの領域での統一理論を目指すことである。質的計算にも同値関係や順序などさまざまなものがあり、また量的計算においても、対象システムの種類と観測モードの両面で多様な結果があるため、これらを統一的視点のもとに収めることには意義があると考えられる。特に後者については、さまざまな状況で計算過程として使われる「ゲーム」の構成を、統合できるのではないかと考えており、現在作業中である。
|
