2021 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 – 2023-03-31
|
| Keywords | ラムダ計算 / 合流性 / Z定理 / チャーチ・ロッサーの定理 / スペクトラル空間モデル / 直観主義論理 / 数理パズル / 形式化 |
|---|
| Outline of Annual Research Achievements |
計算の複雑さに関する基本的性質として，計算可能性・計算量の問題を本質的に特徴付けている基本概念は何かという根本問題がある．この問題を証明と形式化された計算との関係から研究を行った．Church―Rosserの定理のシステマチックな証明のために，Z定理を拡張した分割統治的な手法を導入した．この手法により，値呼びラムダ計算の合流性の証明を与えることができた．この結果は，査読付き論文として現在投稿中である（中澤，藤田，今川の共著論文）．
また，２階直観主義論理のスペクトラル空間モデルについての研究も継続して行い，完全性と健全性の証明を構築中である．この研究成果は，京都大学数理解析研究所RISM研究集会（証明と計算の理論と応用）と日本数学会2022年度年会（数学基礎論）においてそれぞれ研究発表を行なった．加えて，形式化・記号化に関して，スマリヤン・ブーロース流の論理パズルの形式化を行なって，論理式による特徴付けを明らかにした．さらに，その問題の数学的な一般化についても研究を行った．この結果は，日本数学会2021年度秋季総合分科会（数学基礎論）と京都大学数理解析研究所RIMS共同研究（論理・代数系・言語と計算機科学の周辺領域）でそれぞれ研究発表を行なった．これに関連して，数理パズル，ゲーデルの完全性定理，カリー・ハワード同型に関する内容をまとめて専門書として出版した．また，第24回プログラミングおよびプログラミング言語ワークショップ（日本ソフトウェア科学会PPL2022）でプログラム委員会委員を務めて，査読と情報収集などにあたった．
以上の研究成果の概要は次のWebページ
http://www.cs.gunma-u.ac.jp/~fujita/
からも公開しており，研究成果の内容を分かりやすく情報発信している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
値呼びラムダ計算の合流性の証明をZ定理の拡張の方針で与えることができた．
２階直観主義論理のスペクトラル空間モデルの完全性と健全性定理の証明方針が明らかになってきた．
スマリヤン・ブーロース流の論理パズルの形式化を行なって，論理式による特徴付けを明らかにした．この成果も含めて，数理論理学の専門書を出版した．
以上について，学会・研究会等において５件の研究発表を行って，研究を遂行してきた．
|
| Strategy for Future Research Activity |
形式化の観点から，証明と計算の相互作用の深化を図り，計算量の基本問題を多面的角度から追求するために，型付き計算体系の型理論が，ソートの階層，型の階層でパラメータ化された形式的体系を構築していく．これにより，証明と形式化された計算との深淵な関係についての研究を継続していく．
|
| Causes of Carryover |
学会，研究会などがオンラインに制限されたことによる．今後は状況を注視しつつ，研究発表，研究打ち合わせなどの旅費も活用していく計画である．
|
