2022 Fiscal Year Research-status Report
| Project/Area Number |
22K03401
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
木原 貴行 名古屋大学, 情報学研究科, 准教授 (80722701)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | 実現可能性トポス / Lawvere-Tierney位相 / Weihrauch次数 / チューリング次数 / 構成的数学 / 構成的逆数学 |
|---|
| Outline of Annual Research Achievements |
本年度は，計算論における神託概念がLawvere-Tierney位相とみなせるという観点を詳細に突き詰め，神託概念と真理値上の演算に関する多数の結果を得た．LT-位相の概念は，内的単調性，増強性，冪等性の3つの性質によって特徴付けられる．計算論における万能マシンの性質を抽象化することによって，内的単調性と関連する性質が現れることを明らかにし，内的単調性とWeihrauch還元可能性の関連性を明らかにした．同様の方法で，これに増強性を付加したものが点付きWeihrauch還元可能性，さらに冪等性を加えると一般Weihrauch還元可能性に対応することも明らかにした．また，LT-位相は部分トポスと対応することが知られているが，そのうち実効トポスの実現可能性部分トポスに対応する神託概念はSasso流のサブチューリング還元と対応することを明かした．
サブチューリング次数については，シンガポール南洋理工大学のKeng Meng Ng氏と共同研究を進め，サブチューリング次数（したがって実効トポスの実現可能性部分トポス）が非分配的な束をなし，結び既約次数を持ち，極小対が存在しない，など数々の次数論的性質を証明した．その中で，特に擬極小サブチューリング次数に関する様々な結果を得て，これを応用して，形式チャーチ提唱(CT)と拡張形式チャーチ提唱(ECT)を分離する最初のモデルの構築に成功し，構成的逆数学への様々な応用を示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
神託計算とLawvere-Tierney位相の詳細な分析が順調に進み，その結果として，LT-位相の3つの性質がそれぞれ計算論的に自然な意味を持つことが明らかになった．そして，実効トポスの実現可能性部分トポスに対応するLT-位相の計算論的対応物はSasso流サブチューリング次数となるが，この分析が想像以上に進展し，その非分配性証明や結び既約次数の存在等の数多くの非自明な結果を得るに至った．特に擬極小次数に関する結果を構成的数学のモデルの構成へと応用することに成功し，形式チャーチ提唱(CT)と拡張形式チャーチ提唱(ECT)の分離に成功したのは，想定外の結果であった．
|
| Strategy for Future Research Activity |
実効トポスの実現可能性部分トポスに対応する次数概念であるSasso流サブチューリング次数について，既に数多くの結果が得られているものの，まだ数多くの問題が残されているため，その研究を進める予定である．また，構成的数学の応用であるが，形式チャーチ提唱には様々な変種があるので，全パターンの組合せを分離する構成的数学のモデルを構成するのが今後の目標である．また，形式チャーチ提唱以外の他の重要な構成的原理についても分析を進めていく．
|
| Causes of Carryover |
2020年度から昨年度に掛けてのコロナ禍のために，その期間を含む別予算が，2021年度から2022年度に延長され，2022年dの研究費は延長分予算から優先的に支出をしていたため，本予算を使用する機会が無かった．
|
