| 研究課題/領域番号 |
20K14352
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
河井 達治 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00824343)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| キーワード | 構成的数学 / 位相空間論 / point-freeトポロジー / 不動点定理 / 実現可能解釈 / 測度論 / プログラム抽出 |
|---|
| 研究実績の概要 |
本研究は，1.分配束に基づく新たな位相空間の概念を提案し，2.この概念に基づく命題の証明からプログラム抽出によりアルゴリズムを抽出することを通して，point-free位相空間論に内在する構成的意味を解明することを目的とする．このために，新たに導入する位相空間の概念を用いて測度論や線形位相空間論を定式化することにより，構成的解析学を高次の位相空間の観点から再構築する．また，不動点定理や作用素の拡張定理のpoint-free位相空間論における適切な定式化を提示し，証明からのプログラム抽出を通して，命題の構成的意味を位相のレベルで解明する．
前年度は，実数の位相を符号付きビット表現(三本木)による順序空間により特徴付け，その表現を用いて中間値の定理，及びBrouwerの不動点定理をpoint-free位相により定式化し，これらの命題の証明を与えた．本年度は，上記の実数表現と位相幾何学の単体分割による空間表現との関係を調査し，符号付きビット表現が本質的には1-単体の重心細分と同値であることを示した．この知見を高次元に拡張することにより，重心細分に基づくユークリッド空間，及び高次元球体のpoint-free位相による特徴付けを得ることができた．これにより，Brouwerの不動点定理やBorsuk-Ulamの定理などの高次元球体（球面）に関する命題と，Spernerの補題やTuckerの補題などの離散数学における命題との関連を，より明確に捉えることができるようになった．また，この重心分割に基づく位相表現は，今後，point-free位相において位相幾何学を展開するための基盤となることが期待される．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
前年度の実数空間のpoint-free位相の表現をユークリッド空間に拡張できたこと，また，そのpoint-free表現が本質的には実数空間の三角形分割の重心細分により与えられることを示すことができたことは，一定の成果である．これらの結果は，当初予見していた研究の方向性とは若干異なるが，point-free位相空間論と位相幾何学の密接な関係を示唆するものであり，より詳細な調査に値するものであると考える．一方，測度論，線形位相空間論の定式化については，基本的な例を題材とした調査研究に留まっている．また，証明支援システムを用いたプログラム抽出については，予備調査により大方の見通しは立ててはいるが，具体的な実装には至っていない．
|
| 今後の研究の推進方策 |
次年度は，測度空間，線形位相空間などの分配束による表現を与える．まずは，本年度までに実施した，幾つかの例（空間）に基づく調査研究を分配束による表現としてまとめる．そして，そのれらの具体例における表現を，一般の測度空間，線形位相空間に拡張することを試みる．また，本年度に得られた三角形分割の重心細分に基づくユークリッド空間の表現を，単体写像の概念に基づく関数空間の表現へと拡張する．そして，単体複体の理論において最も基本的な命題である単体近似定理をpoint-free位相空間論において定式化する．さらに，単体近似定理に基づき，Brouwerの不動点定理をはじめとする種々の不動点定理をpoint-free位相のレベルで形式化する．一方，プログラム抽出のケーススタディとして，三角形分割によるユークリッド空間の位相表現，及び種々の不動点定理をMinlogなどの構成的数学に基づく証明支援システム上で形式化する．そして，これらの命題の証明からプログラムを抽出し，そのアルゴリズムを明らかにする．
|
| 次年度使用額が生じた理由 |
前年度に引き続きコロナウイルスの影響により，予定していた海外の研究機関における長期滞在や国際会議への参加が中止となり，海外旅費を使用しなかったのが理由である。次年度は，新型コロナウイルスの感染状況にもよるが，海外の研究機関における長期滞在や国際会議への参加，及び，参考文献の購入のために使用する予定である．
|
