研究実績の概要 |
研究の基礎となってい位相空間の形式化の一部と、ベールカテゴリー定理、ビング収縮定理の形式化を、COQとSSReflect拡張の混在から、よりSSReflect拡張を用いたものへと整備した。SSReflectについては、eqtypeが導入され、自然数型などがCOQと十分な整合性がないので、完全にSSReflectに書き換えるのは難しいが、できる範囲で十分整備されたと考えている。この結果は国際会議CICM2016(Intelligent Computer Mathematics, Bialystok, Poland)で発表し、SpringerのレクチャーノートLNAI9791で出版された。また、フリードマンによる可算シェンフリース定理の形式化に向けて、具体的な次元のユークリッド円板や球面を扱うのではなく、これらの性質を抽象化して収縮定理を適応することの重要性を指摘し、抽象的胞体性の概念を定式化した。伝統的な数学の立場では、このような抽象化は、数学的に新しい応用を生むことが不明な場合、意義が少ないと考えられる傾向があるが、COQのような証明支援系が基礎としている帰納 的構成の論理では、構成的議論と非構成的議論を分離する意味でも、また、実数概念を用いた多様体や、さらにn次元球面などの具体的な形式化に依存しない可搬的な形式化という意味でも意義が生まれていると考えている。これらの抽象胞体体性は、上記の論文「Formalization of BIng's shrinking method in geometric topology, Lecture Notes in Artificial Intelligence 9791, Springer (2016)において発表した。
|