| Project/Area Number |
20K03711
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 情報学部, 准教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2021: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | ラムダ計算 / チャーチ・ロッサーの定理 / 2階直観主義論理 / 決定不能 / 論理パズル / ブーロース / カリー・ハワード同型 / Z特性 / 合流性 / 定量的評価 / 直観主義論理 / スペクトラル空間モデル / ブーロスの論理パズル / Z定理 / 数理パズル / 形式化 / 型付ラムダ計算 / 位相的・束論的意味論 / ゲーデルのシステムT / 計算的複雑さ / 型付きラムダ計算 / グルジェゴルチック階層 |
|---|
| Outline of Research at the Start |
全ての問題に関わる基本的性質の一つとして計算の複雑さがある．本課題の核心は，計算量・計算可能性を本質的に特徴づけている基本概念は何か？という根本問題である．そのために，証明と形式化された計算との関係からこの問題を研究する．本研究では，計算量的階層に対応する計算体系と健全・完全な意味論を構築する．これにより，証明と計算の相互関係の一層の深化を図り，計算量の基本問題を深く追求する礎を築くことを目指す．
|
| 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年にワルシャワ大学で特定国派遣研究者として共同研究してきた型推論と型検査の問題の全容がおおよそ解明されたので，共著論文としてまとめる．また，２階直観主義論理のモデルに関する研究が，大きく進展しつつあるので積極的に推進していく方針である．
|
