2020 Fiscal Year Research-status Report
Notion of space based on distributive lattices and its computational content
| Project/Area Number |
20K14352
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
河井 達治 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00824343)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | 構成的数学 / 位相空間論 / pointfreeトポロジー / 不動点定理 / 実現可能解釈 / 測度論 / プログラム抽出 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、1. 分配束に基づく新たな位相空間の概念を提案し，2.この概念に基づく命題の証明からプログラム抽出によりアルゴリズムを抽出することを通して，point-free位相空間に内在する構成的意味を解明することである．この目的ために，新たに導入する位相空間の概念を用いて測度論や線形位相空間論を定式化することにより，構成的解析学を高次の位相空間の観点から再構築する．また，不動点定理や作用素の拡張定理のpoint-free位相空間論における適切な定式化を与え，それら命題の証明からのプログラム抽出によりアルゴリズムを抽出することにより，命題の構成的意味を位相のレベルで解明する．
2020年度は，まずケーススタディとして実数位相の分配束による特徴付けを与えた．そして，その実数表現を用いて中間値の定理とBrouwerの不動点定理をpoint-free位相により定式化し，その証明を与えた．具体的には，1．実数の位相を符号付きビット表現（三本木）のなす順序構造により特徴付けた．2.中間値の定理をこの実数表現を用いて定式化し，鳩の巣原理に基づく証明を与えた．3. 1の実数表現を高次元に拡張することによりBrouwerの不動点定理を定式化し，Hexゲームの必勝戦略に基づく証明を与えた．これらの研究を通して，中間値の定理・Brouwerの不動点定理の構成的意味が，本質的には鳩の巣原理やHexゲームの必勝戦略であることを明らかにした．また，これらの研究で得られた実数表現を構成的逆数学に応用し，Fanの定理を閉区間上実関数の連続モジュラスの一様連続性により特徴付けた．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
初年度は，ケーススタディとはいえ，実数位相の分配束による特徴付けを与え，中間値の定理とBrouwerの不動点定理のpoint-free位相による定式化と，それらの構成的意味を明らかにできたことは一定の成果である．一方，初年度にある程度進展を予定していた，測度論，線形位相空間論，位相群をはじめとする位相代数論に現われる空間の分配束による表現については，既存の文献調査にとどまっている．
|
| Strategy for Future Research Activity |
次年度は，測度空間，線形位相空間，位相群をはじめとする位相代数などの分配束による表現を与える．また，これらの分配束による位相表現を用いて，構成的解析学において重要な位置を占める測度論と線形位相空間論の主要な部分を位相空間の観点から再構築する．さらに，プログラム抽出のケーススタディとして，本年度に得られた実数位相の表現，その表現を用いた中間値の定理・Brouwerの不動点定理を構成的形式体系TCFの実装であるMinlogシステム上で形式化する．そして，これらの命題の証明からプログラムを抽出することにより，その構成的意味を明らかにする．
|
| Causes of Carryover |
新型コロナウイルスの影響により，当初予定していた海外の研究機関における長期滞在や国際会議への参加が中止となり，海外旅費を使用しなかったのが理由である。次年度の予算は、新型コロナウイルスの感染状況にもよるが，海外の研究機関での長期滞在や国際会議への参加のために使用する予定である．
|
