2023 Fiscal Year Research-status Report
Notion of space based on distributive lattices and its computational content
| Project/Area Number |
20K14352
|
|---|
| Research Institution | Kochi University |
|---|
Principal Investigator |
河井 達治 高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | 構成的数学 / 位相空間論 / point-freeトポロジー / コンパクト空間 / 不動点定理 / 一点コンパクト化 |
|---|
| Outline of Annual Research Achievements |
本研究は，1.分配束に基づく新たな位相空間の概念を提案し，2.この概念に基づく命題の証明からアルゴリズムを抽出することを通して，point-free位相空間論に内在する構成的意味を解明することを目的としている．前年度までに，コンパクト空間の分配束による表現を，局所コンパクト空間に拡張した．ところが，昨年度に得られた局所コンパクト空間の特徴付けに対する証明に専門家から誤りが指摘され，今年度は，その証明の修正に取り組んだ．その結果，前年度にまでに得られた結果を完全に保持する形で，新たな証明を構成することができた．この結果は，9月に行われた国際学会CCC2023で発表した（現在，証明を修正した論文を準備中である）．なお，専門家の指摘では，コンパクト空間の結果を自然に拡張する前年度の結果は成立しないのではないかとのことであった．しかし，本年度に与えた新たな証明により，昨年度までの結果が保持されたことは，コンパクト空間において成立する事実のさらなる拡張の可能性を示唆するものであると考える．一方，本年度は，上記の証明の修正に想定外の時間がかかり，本来行う予定であった，1.局所コンパクト空間の一点コンパクト化の単純な定式化やその具体例の構成，2.一般ユークリッド空間のpoint-free位相の定式化と，それに基づく種々の不動点定理のpoint-free位相のレベルでの形式化，については研究の新たな進展が得られていない．これらの課題については，来年度に取り組む予定である．
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
本年度は，前年度までに得られていた主結果の証明に誤りが指摘され，その修正に時間を取られてしまった．その結果，今年度に行う予定であった研究の進展が遅れている．幸い，上記の証明の修正は上手くいき，これまでの結果は保持されることを確認した．また，証明の修正の過程で，これまで気付かなかった新たな知見が得られたことも有用であった．今後は，これらの新たな知見を活かし，今年度に行う予定であった一点コンパクト化の定式化と証明，不動点定理のpoint-freeトポロジーにおける形式化とアルゴリズムの抽出に取り組む予定である．
|
| Strategy for Future Research Activity |
まず，局所コンパクト空間の一点コンパクト化のpoint-freeトポロジーにおける単純な証明を与え，その有用性を裏付けるための具体例を作成する．そして，一点コンパクト化に関する一連の研究成果を論文としてまとめる．また，順序関係から自然に誘導されると考えられるユークリッド空間の単体表現を用いることにより，一般のユークリッド空間のpoint-free位相表現を定式化する．そして，種々の不動点定理をpoint-free位相のレベルで形式化し，その証明を与える．一方，プログラム抽出のケーススタディとして，上記の一般ユークリッド空間の位相表現を構成的数学に基づく形式体系で実装し，不動点定理の証明の実装からのプログラム抽出を試みる．
|
| Causes of Carryover |
健康上の理由により，計画していた海外渡航（在外研究，関連学会の参加）を中止せざるを得なかったことが理由である．繰越しとなった研究費は，来年度,海外渡航費(海外研究機関における滞在費・国際学会への参加)，関連図書の購入費に充てる予定である．
|
