2018 Fiscal Year Annual Research Report
Set-theoretical investigation on properties of sets of reals and its application to computer science
Project/Area Number |
17J00479
|
Research Institution | University of Tsukuba |
Principal Investigator |
石井 大海 筑波大学, 数理物質科学研究科, 特別研究員(DC2)
|
Project Period (FY) |
2017-04-26 – 2019-03-31
|
Keywords | Groebner 基底 / Presburger 算術 / 生成超冪 / Homotopy Type Theory / 実閉体 / 強制法理論 / 集合論的多元宇宙 |
Outline of Annual Research Achievements |
計算機上への実装の課題に重点的に取り組んだ。特に、有理数体や実閉体と密接に関連する Groebner 基底計算アルゴリズムの実装や、適したシステムの再設計に注力した。まず、以前より開発を進めていた計算代数システムの設計を見直した。その上で、効率的なGroebner 基底計算アルゴリズムの実装を完了し、テスト手法の改善や大規模なベンチマークを行い、効率を改善した。また、型レベル自然数の軽量化を実現するため、Presburger 算術の自動証明を行う型検査器プラグインの増強を行い、非解釈項を含む命題も取り扱えるようになった。 以上の詳細は、単著論文 “A Purely Functional Computer Algebra System Embedded in Haskell“ にまとめ、9月に行われた国際会議 Computer Algebra in Scientific Computing 2018 に投稿・受理され、講演を行うとともに論文集に採録された。同内容は、2018年12月に京都大学数理解析研究所の研究集会「Computer Algebra -- Theory and its Applications」でも発表を行った。 また、本課題の背景理論の一つである強制法のより体系的な分析を企図し、非整礎Boole超冪の成す生成多元宇宙の定式化を試み、沖縄において開催された数学基礎論若手の会2018で途中経過を報告し、また早稲田大学の週間セミナーで定期的に発表・情報交換を行った。 最後に進行中の結果を述べる。まずGroebner 基底計算アルゴリズムである M4GV の調査・実装を試みている。また、Homotopy Type Theory を用いた、計算機上でのアルゴリズムや測度論の定式化の可能性についても探った。生成超冪による強制法の分析についても進行中である。
|
Research Progress Status |
平成30年度が最終年度であるため、記入しない。
|
Strategy for Future Research Activity |
平成30年度が最終年度であるため、記入しない。
|
Research Products
(4 results)