| 研究課題/領域番号 |
20K03711
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 情報学部, 准教授 (30228994)
|
|---|
| 研究分担者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | ラムダ計算 / チャーチ・ロッサーの定理 / 2階直観主義論理 / 決定不能 / 論理パズル / ブーロース / カリー・ハワード同型 / Z特性 / 合流性 / 定量的評価 / 直観主義論理 / スペクトラル空間モデル / ブーロスの論理パズル / Z定理 / 数理パズル / 形式化 / 型付ラムダ計算 / 位相的・束論的意味論 / ゲーデルのシステムT / 計算的複雑さ / 型付きラムダ計算 / グルジェゴルチック階層 |
|---|
| 研究開始時の研究の概要 |
全ての問題に関わる基本的性質の一つとして計算の複雑さがある．本課題の核心は，計算量・計算可能性を本質的に特徴づけている基本概念は何か？という根本問題である．そのために，証明と形式化された計算との関係からこの問題を研究する．本研究では，計算量的階層に対応する計算体系と健全・完全な意味論を構築する．これにより，証明と計算の相互関係の一層の深化を図り，計算量の基本問題を深く追求する礎を築くことを目指す．
|
| 研究実績の概要 |
計算の複雑さに関する基本性質として，「計算可能性と計算量の問題を特徴付けている基本概念は何か」という根本問題がある．この問題を証明と形式化された計算の観点から研究を行った．
まず，Church-Rosserの定理のモジュール性に基づく証明のために，合成的Z定理を活用した新手法を導入した．これにより，分割統治法的な技法により，合流性を証明する方法を開発することができた．この結果は京都大学数理解析研究所研究集会「証明論と計算論の最前線」で研究発表を行なった．そして，現在，論文として作成中である（女屋，藤田，中澤の共著論文）．また，2階直観主義論理のモデルについても共同研究をして，その研究成果を同研究集会でも発表した．そして，その結果も共著論文として作成中である（倉田，藤田の共著論文）．
加えて，ブーロース流の論理パズルに関して，論理的推論の観点から研究をして，京都大学数理解析研究所研究集会「群・代数・言語と計算機科学の周辺領域」で研究発表を行った．そして，ここ３年間の研究成果も併せて論文としてまとめている（本多，藤田の共著論文）．
さらに，シャルマース工科大学（スウェーデン）に滞在をして，P. Dybjerとカリー・ハワード同型に関する国際共同研究をおこなった．その後，ワルシャワ大学（ポーランド）に滞在をして２階直観主義命題論理の証明可能性が決定不能であることに関する国際共同研究を行った．そして，新しい決定不能の結果が得られたので，A. Schubert, P. Urzyczyn, K. Zdanowskiとの共著論文としてその成果を投稿していたが，論文が受理されて，Journal of Applied Non-Classical Logicから査読付き論文として出版された．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
学会・研究集会等で３件の研究発表を行った．また，国際共同研究で得られた成果を査読付きジャーナルから出版することができた．
|
| 今後の研究の推進方策 |
2024年に出版された査読付き論文の成果について，国際共同研究を継続して決定不能性の証明を精査していく．さらに，2008年にワルシャワ大学で特定国派遣研究者として共同研究してきた型推論と型検査の問題の全容がおおよそ解明されたので，共著論文としてまとめる．また，２階直観主義論理のモデルに関する研究が，大きく進展しつつあるので積極的に推進していく方針である．
|
