Godel's system T and computational complexity hierarchy
| 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 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| 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 | ラムダ計算 / 合流性 / チャーチ・ロッサーの定理 / 定量的評価 / カリー・ハワード同型 / 直観主義論理 / スペクトラル空間モデル / ブーロスの論理パズル / Z定理 / 数理パズル / 形式化 / 型付ラムダ計算 / 位相的・束論的意味論 / ゲーデルのシステムT / 計算的複雑さ / 型付きラムダ計算 / グルジェゴルチック階層 |
|---|
| Outline of Research at the Start |
全ての問題に関わる基本的性質の一つとして計算の複雑さがある．本課題の核心は，計算量・計算可能性を本質的に特徴づけている基本概念は何か？という根本問題である．そのために，証明と形式化された計算との関係からこの問題を研究する．本研究では，計算量的階層に対応する計算体系と健全・完全な意味論を構築する．これにより，証明と計算の相互関係の一層の深化を図り，計算量の基本問題を深く追求する礎を築くことを目指す．
|
| Outline of Annual Research Achievements |
全ての問題の根幹に関わる基本的性質の一つとして計算の複雑さの問題がある．この問題を証明と形式化された計算との関係から研究を行った．特に，カリー・ハワード同型と証明の形式化の観点から，グリベンコの定理，ゲーデル・ゲンツェンの変換，コルモゴロフの変換，黒田の変換の二重否定による埋め込みとプログラム変換との対応をラムダ・ミュー計算を使って形式化を行い統一的にまとめてチュートリアルを行った．この結果は，数理解析研究所講究録（数理論理学とその応用）から発表した．
また，抽象書換系の合流性とZ性について，合成的Z定理の観点からサーベーを行って，その結果を数理解析研究所講究録（証明と計算の理論と応用）から赤坂，中澤との共著論文として発表した．さらに，従来のZ定理では困難であるが，合成的Z定理を使って値呼び計算体系の合流性を示した．従来手法では停止性とHindley-Rosenの補題から証明されていたが，合成的Z定理を適用すると停止性から独立に証明可能となった．本結果は，Mathematical Structures in Computer Science (Cambridge University Press) から，中澤，今川との共著論文として発表した．
一方，直観主義論理の代数的モデルに関するこれまでの成果（Fundamenta Informaticae 2019年）をさらに再構築して，Stoneの表現定理より，完全分配代数的束に基づく代数的モデルでも完全性が証明できることを数理解析研究所講究録（証明と計算の理論と応用）から発表して，今後の更なる進展の足がかりを作った．
また，George Boolosの論理バズルを一般化して，表示的意味論の観点から考察を与えた．そして，数理解析研究所にて，倉田との共同研究として発表を行なった．
|
| 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定理に関する調査研究，及び，合成的Z定理を活用した合流性の新証明の発表を行なった．また，2階直観主義論理の代数的モデルと位相モデルの関係を明確にする考察も与えることができた．さらに，論理パズルを一般化して，表示的意味論の観点からその解法についての考察も与えた．
以上について，研究会等で研究発表とチュートリアルを合計２件行い，また，学術雑誌，講究録など合計５編の研究論文を発表してきた．
|
| Strategy for Future Research Activity |
証明の形式化の観点から，証明と計算の相互作用を深化させて，計算量の基本問題を多面的角度から追求するために，型付き計算体系の型理論が様々な特徴量でパラメータ化された形式的体系を構築していく．今後の研究については，特に，2階直観主義論理の非可解性に関する証明，及び直観主義論理の代数的モデルと位相的モデルの一般的な対応枠組みについての研究を重点的に推進していく方策である．
|
Report
(3 results)
Research Products
(23 results)
