2023 Fiscal Year Research-status Report
Godel's system T and computational complexity hierarchy
| Project/Area Number |
20K03711
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 情報学部, 准教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | ラムダ計算 / チャーチ・ロッサーの定理 / 2階直観主義論理 / 決定不能 / 論理パズル / ブーロース / カリー・ハワード同型 / Z特性 |
|---|
| Outline of Annual Research Achievements |
計算の複雑さに関する基本性質として，「計算可能性と計算量の問題を特徴付けている基本概念は何か」という根本問題がある．この問題を証明と形式化された計算の観点から研究を行った．
まず，Church-Rosserの定理のモジュール性に基づく証明のために，合成的Z定理を活用した新手法を導入した．これにより，分割統治法的な技法により，合流性を証明する方法を開発することができた．この結果は京都大学数理解析研究所研究集会「証明論と計算論の最前線」で研究発表を行なった．そして，現在，論文として作成中である（女屋，藤田，中澤の共著論文）．また，2階直観主義論理のモデルについても共同研究をして，その研究成果を同研究集会でも発表した．そして，その結果も共著論文として作成中である（倉田，藤田の共著論文）．
加えて，ブーロース流の論理パズルに関して，論理的推論の観点から研究をして，京都大学数理解析研究所研究集会「群・代数・言語と計算機科学の周辺領域」で研究発表を行った．そして，ここ３年間の研究成果も併せて論文としてまとめている（本多，藤田の共著論文）．
さらに，シャルマース工科大学（スウェーデン）に滞在をして，P. Dybjerとカリー・ハワード同型に関する国際共同研究をおこなった．その後，ワルシャワ大学（ポーランド）に滞在をして２階直観主義命題論理の証明可能性が決定不能であることに関する国際共同研究を行った．そして，新しい決定不能の結果が得られたので，A. Schubert, P. Urzyczyn, K. Zdanowskiとの共著論文としてその成果を投稿していたが，論文が受理されて，Journal of Applied Non-Classical Logicから査読付き論文として出版された．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
学会・研究集会等で３件の研究発表を行った．また，国際共同研究で得られた成果を査読付きジャーナルから出版することができた．
|
| Strategy for Future Research Activity |
2024年に出版された査読付き論文の成果について，国際共同研究を継続して決定不能性の証明を精査していく．さらに，2008年にワルシャワ大学で特定国派遣研究者として共同研究してきた型推論と型検査の問題の全容がおおよそ解明されたので，共著論文としてまとめる．また，２階直観主義論理のモデルに関する研究が，大きく進展しつつあるので積極的に推進していく方針である．
|
| Causes of Carryover |
コロナ禍の影響と関連する事情が数年に渡り，ようやく昨年度より国際共同研究を実際に再開することができたが，今年度は，研究発表，研究打ち合わせなどの旅費も順次に活用していく計画である．
|
