| 研究課題/領域番号 |
20K14352
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 高知大学 (2022-2023)
北陸先端科学技術大学院大学 (2020-2021) |
|---|
研究代表者 |
河井 達治 高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 構成的数学 / 位相空間論 / point-freeトポロジー / コンパクト空間 / 不動点定理 / 一点コンパクト化 / プログラム抽出 / 実現可能解釈 / 測度論 / pointfreeトポロジー / 分配束 / point-free位相 |
|---|
| 研究開始時の研究の概要 |
構成的数学の主眼は，構成的証明とプログラムの対応を通して，数学に内在するアルゴリズム的側面を解明することにある．しかし，構成的位相空間論の主要なアプローチであるpoint-free位相の構成的意味の解明は全く進んでいない．本研究では，申請者の直近の研究に基づく分配束による位相構造を拡張することにより，厳密な構成的立場から，広範囲の空間を表現できるようなpoint-free位相の概念を提案する．また，この位相概念を用いて，構成的解析学の主要な部分を位相的観点から再構築する．さらに，証明からのプログラムの抽出を通して，point-free位相空間論の存在証明に内在するアルゴリズムを明らかにする．
|
| 研究実績の概要 |
本研究は，1.分配束に基づく新たな位相空間の概念を提案し，2.この概念に基づく命題の証明からアルゴリズムを抽出することを通して，point-free位相空間論に内在する構成的意味を解明することを目的としている．前年度までに，コンパクト空間の分配束による表現を，局所コンパクト空間に拡張した．ところが，昨年度に得られた局所コンパクト空間の特徴付けに対する証明に専門家から誤りが指摘され，今年度は，その証明の修正に取り組んだ．その結果，前年度にまでに得られた結果を完全に保持する形で，新たな証明を構成することができた．この結果は，9月に行われた国際学会CCC2023で発表した（現在，証明を修正した論文を準備中である）．なお，専門家の指摘では，コンパクト空間の結果を自然に拡張する前年度の結果は成立しないのではないかとのことであった．しかし，本年度に与えた新たな証明により，昨年度までの結果が保持されたことは，コンパクト空間において成立する事実のさらなる拡張の可能性を示唆するものであると考える．一方，本年度は，上記の証明の修正に想定外の時間がかかり，本来行う予定であった，1.局所コンパクト空間の一点コンパクト化の単純な定式化やその具体例の構成，2.一般ユークリッド空間のpoint-free位相の定式化と，それに基づく種々の不動点定理のpoint-free位相のレベルでの形式化，については研究の新たな進展が得られていない．これらの課題については，来年度に取り組む予定である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
本年度は，前年度までに得られていた主結果の証明に誤りが指摘され，その修正に時間を取られてしまった．その結果，今年度に行う予定であった研究の進展が遅れている．幸い，上記の証明の修正は上手くいき，これまでの結果は保持されることを確認した．また，証明の修正の過程で，これまで気付かなかった新たな知見が得られたことも有用であった．今後は，これらの新たな知見を活かし，今年度に行う予定であった一点コンパクト化の定式化と証明，不動点定理のpoint-freeトポロジーにおける形式化とアルゴリズムの抽出に取り組む予定である．
|
| 今後の研究の推進方策 |
まず，局所コンパクト空間の一点コンパクト化のpoint-freeトポロジーにおける単純な証明を与え，その有用性を裏付けるための具体例を作成する．そして，一点コンパクト化に関する一連の研究成果を論文としてまとめる．また，順序関係から自然に誘導されると考えられるユークリッド空間の単体表現を用いることにより，一般のユークリッド空間のpoint-free位相表現を定式化する．そして，種々の不動点定理をpoint-free位相のレベルで形式化し，その証明を与える．一方，プログラム抽出のケーススタディとして，上記の一般ユークリッド空間の位相表現を構成的数学に基づく形式体系で実装し，不動点定理の証明の実装からのプログラム抽出を試みる．
|
