トポロジカル手法による理論分散計算の統一理論の構築
| Project/Area Number |
18J21885
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | The University of Tokyo |
|---|
| Research Fellow |
西脇 友一 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2018-04-25 – 2021-03-31
|
| Project Status |
Granted (Fiscal Year 2019)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2019: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2018: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | 様相論理 / 圏論 / 意味論 / プログラミング言語理論 / 証明論 |
|---|
| Outline of Annual Research Achievements |
今年度は，直観主義様相論理に基づくプログラムを中心に研究を行った．当初予定していた組み合わせ幾何を直接扱うアプローチは数学的な困難さが回避できないことがわかった．一方で，直観主義様相論理を経由して組み合わせ幾何を扱うアプローチが有効であることがわかったのでそちらに基づいて研究を行った．大きな成果が得られたものから順に述べる．まず，直観主義様相論理の意味論を古典的なKripkeモデルではなくより現代的な圏論的モデルによって与える研究をおこなった．この研究によって，直観主義様相論理が圏論で用いられる豊穣圏という概念と密接に関連していることがわかった．次に，圏論的モデルを検討することによって得られた知見をもとに，直観主義様相論理の証明論にかんする研究を行った．この研究によって双文脈流とFitch流と呼ばれる直観主義様相論理の二つの証明体系が圏論的には随伴によって説明できることがわかった．それらと平行して外部の研究者と新しいプログラミングパラダイムについての共同研究を行った．この研究では探索問題を解くプログラムを簡潔に記述するための手法を提案した．申請者は特にプログラミング言語の理論に関する知見を生かして提案手法の数学的基礎づけを担当した．先立つ直観主義様相論理の研究では直観主義のボックス様相のみを扱ってきたので，その双対である直観主義ダイヤモンド様相についての研究を行った．この研究により直観主義ダイヤモンド様相と次数付き代数的効果が密接な関係にあることがわかった．また，量子計算に関連して，分布モナドの変種の研究を行った．この研究では，量子通信プロトコルの検証のためのモナドを定義し，その性質を調べた．また，ゲーデル論理と呼ばれる中間論理に対応するプログラミング言語の研究を行った．この研究では証明論的な議論によって並列・平行計算の基礎となる抽象的な言語の構文を作成した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初予定していたアプローチを修正する必要はあったものの，修正後の研究ではインパクトのある成果が得られている．一方で，本来の目標である分散計算に関連した成果は限定的なものにとどまっている．アプローチの修正によって得られた成果を再検討し分散計算に適用することが今後の重要な課題である．以上を総合して，着実に研究成果が積み重なっておりおおまかには順調に発展していると考える．
|
| Strategy for Future Research Activity |
引き続き，直観主義様相論理を通して分散計算のための基礎理論の構築を目指す．直観主義様相論理の研究をさらに進めて，意味論の解明に努める．特に，現在までに中間的な成果が出ているが論文化できていない，直観主義ダイヤモンド様相と次数付き代数的効果の対応，量子通信プロトコルの検証のためのモナド，ゲーデル論理に基づく平行プログラミング言語の研究を進める．
|
Report
(1 results)
Research Products
(6 results)
