Set-theoretical investigation on properties of sets of reals and its application to computer science

点击翻译按钮获取中文摘要

計算機上への実装の課題に重点的に取り組んだ。特に、有理数体や実閉体と密接に関連する 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 を用いた、計算機上でのアルゴリズムや測度論の定式化の可能性についても探った。生成超冪による強制法の分析についても進行中である。