2016 Fiscal Year Research-status Report
4次元ポアンカレ予想を含む幾何的トポロジーの形式化
| Project/Area Number |
15K13433
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究科, 教授 (30186374)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | formalization / geometric topology / shrinking method / coq / ssreflect |
|---|
| Outline of Annual Research Achievements |
研究の基礎となってい位相空間の形式化の一部と、ベールカテゴリー定理、ビング収縮定理の形式化を、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)において発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
ポアンカレ予想の形式化は、時間と労力をつぎ込むことによって十分可能であると考えるようになったか、それ以上に、この研究の過程で、このような形式化を行うにあたり、より本質的なのは「構成可能性」にどう対処するか、ということであると考えるようになり、「実数」概念のように、この意味で扱いにくい（不透明な）概念を使う前に、組み合わせ的に可能な一般論を展開することが重要であると考えるようになった。我々の文脈でいえば、フリードマンの加算シェンフリース定理をそのまま形式化すると、まず、次元nというパラメーターがあり、各次元ごとに、n次元球面という、実数概念を用いて定義される図形があり、その上で証明が（決定可能性や排中律、選択公理を自由に使って）なされるが、抽象的胞体性を定義し、それを用いることによって、このような具体的な図形の定義に依存しない可搬な形式化になり、さらに、実数概念の使用を遅らせることができる。さらに進んで、多様体の概念自体も、より組み合わせ的に行いたいと考えるようになった。そこで、古典的論理と既存のライブラリを使用した形式化を急ぐよりも、議論の本質部分を抽象概念として抽出すること、また、多様体の概念自体も実数に依存しない組み合わせ的な形で形式化する方向に研究が向かっている。
|
| Strategy for Future Research Activity |
COQ/SSReflectを用いた形式化の仮定として、基本的にはINRIA(フランス国立情報学自動制御研究所)の既存ライブラリ等を用いて、ポアンカレ予想に向けた形式化を急ぐ当初の計画は維持するが、構成可能性を重視すると同時に、決定可能集合の型を定義し、基本的な部分から諸命題を記述していくようにする。また、同じ観点から、構成可能性の点から不透明な概念である実数概念の使用を議論の後の方にできるだけ移動し、多様体の概念自体も、組み合わせ的に行うようにする。これは組み合わせ的(PL)多様体論の実数概念を用いない組合せ的形式化であるので、これ自体が重要であると考えている。実数概念に依存しない抽象論で単体的複体を扱うことになるが、これを基礎に多様体論を展開するためには、単体細分の定式化が不可欠である。単体的集合の一般論では、単体細分の概念がほとんどないが、Jardineによる単体近似の定式化を利用して、これが行えないかを研究したいと考えている。
|
