2015 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 | 幾何的トポロジー / ビング収縮定理 / 形式化 / COQ / SSReflect |
|---|
| Outline of Annual Research Achievements |
本年度は幾何的トポロジーの位相同形構成法として重要なビング収縮定理の形式化を整理し、COQのSSReflect拡張による形式化にほぼ書き換えることに成功した。この書き換えによって、コードはより簡潔になり、可読性と保守性が増した。この書き換えには、千葉大学数学・情報数理学科の山本光晴氏と萩原学氏の協力を得ている。この結果は https://github.com/CuMathInfo/Topology/BingShrinkingCriterion で公開されている。
ビング収縮定理の形式化は、我々が初めてCOQを用いて２６年度内に達成したが、これをさらに一般シェンフリース定理や、フリードマンによるシェンフリース定理の形式化に繋げ、さらに、より一般の幾何的トポロジーの広範な形式化に発展させるためには、特異ホモロジー論を始めとする代数的トポロジーの基礎部分を形式化することが不可欠である。このためにはINRIA(フランス国立情報学自動制御研究所)が4色定理やファイト・トンプソンの定理を形式化するために開発した数学ライブラリであるMathcompの代数ライブラリーを利用することが重要であると考えられる。ところがこのライブラリはSSReflect拡張で書かれており、通常のCOQとの互換性はとられていない。このような状況であるので、我々のCOQによる形式化をSSReflectのコードとしたことは実際的な意義が大きく、この形式化の広範な進展の実行の可能性を広げるものである。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
COQにおけるProp型（命題型）による集合の定義に基づくと、そのままでは集合の特性関数を得ることができず、ビング収縮法やセルラー集合の収縮において現れる無限の部分集合系の扱いができない。すなわち、無限部分集合列をそのまま扱おうとすると、元は無限の証明列を与えなければ定義されず、実用的ではない。このことは幾何的トポロジーの形式化におおきな障害となる。このため、Prop型とbool型を行き来する仕組みとしてのSSReflect拡張を使用することが有効である。従って、２７年度に我々のBing収縮定理COQによる形式化からSSReflect拡張に書き換えることができたことは、実際上の重要な進展と考えている。また、これによってINRIA(フランス国立情報自動制御研究所)が開発している数学ライブラリMathcompの利用がより容易になることも、形式化の進展に寄与すると考えられる。
また、我々はＭ．ブラウンの一般シェンフリース定理のセルラー集合の（形式化されたビング収縮定理を直接は使わない）抽象的な定式化のもとで、形式化することにほぼ成功している。この方法はＭ．フリードマンによる可算シェンフリース定理の形式化に向かって、必要なステップである。実際、可算シェンフリース定理の証明においては、関数でなく、その拡張概念としての「関係」の極限値が扱われており、これは直接的にはビング収縮定理でカバーされていない部分であり、セルラー集合の抽象的設定での収縮の形式化によって可能となる。
|
| Strategy for Future Research Activity |
我々はＭ．ブラウンによる一般シェンフリース定理の形式化は抽象的設定のもとでほぼ完成に近づいている。抽象的設定とは、球面や円板の性質を用いて証明の形式化をえるもので、球面や円板の具体的表示の仕方に依存しない方法として重要である。実際、キャッソンハンドルや、それを積み上げたタワーを形式化するとき、キャッソンハンドルの具体的表示式を使うやりかたでは、具体的図形としては、複雑なものなので、仮に形式化できたとしても、全くポータブルでないものになってしまい、利用できない。そこで、この抽象的設定のもとでの形式化の方針を堅持する。Ｍ．ブラウンによる、このような方針での形式化を完成させた後、フリードマンによる可算シェンフリース定理の形式化にとりかかる。ここでは関数でなく、その拡張概念としての「関係」の極限を扱う。このような基本的概念を縦横に使うことを円滑化するために、集合論的トポロジーの形式化を平行して進める。可算シェンフリース定理の形式化の先には、キャッソンハンドルの形式化の問題にとりくむ。より一般にキャッソンハンドルのタワーや、円板でなく曲面を利用したグロウプ構成の形式化も行う必要がある。ここに至ると代数トポロジーの基本概念を使用する必要が出てくる。そのために、基本群や特異ホモロジー論の形式化が成されなければならない。すなわち代数トポロジーの形式化も平行して進める。これによって、本題の幾何的トポロジーの形式化をもっとも汎用性の高いやりかたで行う予定である。
|
| Remarks |
ビング収縮定理のCOQ/SSReflectによるFormalization
Baire範疇定理のCOQ/SSReflectによるFormalization
|
