| 研究課題/領域番号 |
20K14352
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 高知大学 (2022)
北陸先端科学技術大学院大学 (2020-2021) |
|---|
研究代表者 |
河井 達治 高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
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 位相空間論に内在する構成的意味を解明することを目的としている．
前年度までに，符号付きビット表現(三本木)のなす順序空間による実数位相の特徴付け，その高次元の拡張概念として重心細分に基づくユークリッド空間のpoint-free位相表現が得られている．
本年度は，これまでに得られていたコンパクト空間の分配束による表現を，局所コンパクト空間に拡張した．具体的には，局所コンパクト空間が最大値を必ずしも持たない分配束と羃等関係の組として表現できることを示した．さらに，この分配束による表現を，entailment systemの概念に基づく論理システムとして特徴付けた．これらの表現は，コンパクト空間の分配束による表現や連続束(continuous lattice)のentailment systemによる表現の自然な一般化である．これら一連の研究成果は論文としてまとめられており，現在，学術雑誌に投稿中（査読中）である．また，上記で得られた局所コンパクト空間の表現と既存のコンパクト空間の束表現を用いて，局所コンパクト空間の一点コンパクト化を定義し，このコンパクト化の概念が既存の位相空間論における一点コンパクト化と同値であることを示した．このコンパクト化は，局所コンパクト空間のentailment systemによる論理システムに一つのモデルを強制的に挿入する，という自然な考えに基づくものであり，一点コンパクト化の構成に新たな視点を加えるものである．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
コンパクト空間の分配束による表現を，局所コンパクト空間の束表現に拡張できたことは，一定の成果である．また一点コンパクト化定理により，この新たな局所コンパクト空間の表現と，これまでに得られていたコンパクト空間の分配束による表現を自然に関連付けることができたことも重要な成果であると考える．
一方，本年度は前年度に得られた一般のユークリッド空間の表現を用いて，Borsuk-Ulamの定理などの種々の不動点定理をpoint-free位相のレベルで形式化する計画であったが，現段階では，まだそのために最適な単体の定義を精査している状況である．また，証明支援システムを用いたプログラム抽出については，未だ具体的な実装には至っていない．今後の研究では，プログラム抽出のケーススタディーとして低次元空間における不動点定理の実装を考えている．
|
| 今後の研究の推進方策 |
次年度は，本年度に得られた局所コンパクト空間の一点コンパクト化の有用性を裏付けるための具体例（該当する空間の束表現を含む）を作成し，一点コンパクト化に関する一連の研究成果を論文としてまとめる．また，一般のユークリッド空間の位相表現のための自然な単体表現を確定し，これに基づき基本的な位相幾何学を整備し，その応用として種々の不動点定理をpoint-free位相のレベルで形式化する．一方，プログラム抽出のケーススタディとして，三角形分割による実数，及びユークリッド空間の位相表現をMinlogなどの構成的数学に基づく形式体系で実装する．そして，これらの命題の証明からのプログラムを抽出し，そのアルゴリズムを明らかにする．
|
