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