2020 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 | 型付ラムダ計算 / 直観主義論理 / 位相的・束論的意味論 / チャーチ・ロッサーの定理 / 合流性 / ゲーデルのシステムT / 形式化 / 計算的複雑さ |
|---|
| Outline of Annual Research Achievements |
計算の複雑さに関わる基本性質として，計算可能性・計算量の問題を本質的に特徴付けている基本概念は何か？という根本問題がある．この問題を，証明と形式化された計算との関係から研究を行なった．特に，Church--Rosserの定理の複雑さの解析のために，Z定理を拡張した分割統治的な新手法を導入した．これにより，ラムダ・ミュー計算の名前呼び・値呼びなどの様々な体系の合流性を統一的な枠組みで証明することができた．この結果は，本田，中澤，藤田の共著の査読付き論文としてまとめて，Studia Logica（Springer Nature）から出版した．
また，並行簡約における計算の軌跡を帰納的に生成する圏論的なシステムを箙の観点から導入した．これにより，計算の軌跡はテンソル積により行列表現でコード化できて，隣接行列の計算による機械的な評価につながった．さらに，計算の軌跡をグラフとして表現した簡約グラフに関する基礎研究も行った．M. V. Zilliは，1984年のTheoretical Computer Scienceの論文で，無限に多くのボトルネックを持つ簡約グラフに関する基本定理を与えていたが，これには反例があることが発見された．これらの研究成果は，京都大学数理解析研究所RIMS共同研究にて研究発表を行い，数理解析研究所講究録から２本の研究論文として出版した．
加えて，Smullyan流の論理パズルの論理式による形式化についても研究を行った．この成果は，日本数学会2020年度秋季総合分科会，および京都大学数理解析研究所RIMS共同研究において，それぞれ研究発表を行なった．この結果は，研究論文としてまとめて出版すべき準備を進めている．
以上の研究実績の概要は，次のWebページ
http://www.cs.gunma-u.ac.jp/~fujita/
からも公開して分かり易く情報を発信している．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
Church--Rosserの定理に関係して，合流性に関する基本定理をZ定理の拡張の枠組みで統一的に証明することができた．
また，計算の軌跡をグラフとして表現している簡約グラフに関する基本研究を行なった．
さらに，Raymond Smullyan的な論理パズルの論理式を活用した形式化に関する興味深い考察を与えルことができた．
以上について，研究論文３件（その内，査読付き論文１件），国内学会・研究会等の研究発表２件を行い研究を遂行してきた．
|
| Strategy for Future Research Activity |
証明と計算の相互関係の深化を図り，計算量の基本問題を多面的な角度から深く追求するために，型付き計算体系の型理論が，ソートの階層，型の階層でパラメータ化された形式的体系を構築していく．そして，証明と形式化された計算との深遠な関係についての研究を継続していく．
|
| Causes of Carryover |
学会，研究会への参加を予定していたが，社会情勢のよりオンライン開催となった．今後の開催については，参加，研究発表を積極的に行なっていく計画である．
|
Research Products
(6 results)
