Godel's system T and computational complexity hierarchy

哥德尔系统 T 和计算复杂度层次结构

• 批准号: 20K03711
• 负责人: 藤田 憲悦
• 金额: $ 2.75万
• 依托单位: Gunma University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K03711/
• 关键词: ラムダ計算; 合流性; チャーチ・ロッサーの定理; 定量的評価; カリー・ハワード同型; 直観主義論理; スペクトラル空間モデル; ブーロスの論理パズル; Z定理; 数理パズル; 形式化; 型付ラムダ計算; 位相的・束論的意味論; ゲーデルのシステムT; 計算的複雑さ; 型付きラムダ計算; グルジェゴルチック階層

全ての問題の根幹に関わる基本的性質の一つとして計算の複雑さの問題がある．この問題を証明と形式化された計算との関係から研究を行った．特に，カリー・ハワード同型と証明の形式化の観点から，グリベンコの定理，ゲーデル・ゲンツェンの変換，コルモゴロフの変換，黒田の変換の二重否定による埋め込みとプログラム変換との対応をラムダ・ミュー計算を使って形式化を行い統一的にまとめてチュートリアルを行った．この結果は，数理解析研究所講究録（数理論理学とその応用）から発表した．また，抽象書換系の合流性とZ性について，合成的Z定理の観点からサーベーを行って，その結果を数理解析研究所講究録（証明と計算の理論と応用）から赤坂，中澤との共著論文として発表した．さらに，従来のZ定理では困難であるが，合成的Z定理を使って値呼び計算体系の合流性を示した．従来手法では停止性とHindley-Rosenの補題から証明されていたが，合成的Z定理を適用すると停止性から独立に証明可能となった．本結果は，Mathematical Structures in Computer Science (Cambridge University Press) から，中澤，今川との共著論文として発表した．一方，直観主義論理の代数的モデルに関するこれまでの成果（Fundamenta Informaticae 2019年）をさらに再構築して，Stoneの表現定理より，完全分配代数的束に基づく代数的モデルでも完全性が証明できることを数理解析研究所講究録（証明と計算の理論と応用）から発表して，今後の更なる進展の足がかりを作った．また，George Boolosの論理バズルを一般化して，表示的意味論の観点から考察を与えた．そして，数理解析研究所にて，倉田との共同研究として発表を行なった．

The root of the problem is related to the basic nature of the problem. The problem of formalization and calculation is studied. In particular, the formalization of the proof of the same type of transformation, the transformation of the transformation, the transformation of the black field, the double negation of the transformation, the calculation of the transformation, the formalization of the transformation, the unification of the transformation, the transformation, the transformation. The results of this study are recorded in the Institute of Mathematical Analysis (Mathematical Theory and Application). The convergence and Z properties of abstract book transformation system, the Z theorem of composition, the results of mathematical analysis research institute, etc.(proof and calculation theory and application), Akasaka, Nakazawa, etc. Today, the Z-theorem has been difficult to come by, and the synthetic Z-theorem has demonstrated the value and confluence of computing systems. The Z-theorem of composition is applicable. The stopping property is independent. This result is contrary to Mathematical Structures in Computer Science (Cambridge University Press). The results of the algebra of direct algebraic logic (Fundamenta Informatics 2019) are being reconstructed and Stone's representation theorem is being re-constructed. The completeness of the algebra of complete distributive algebra is being proved. The research on mathematical analysis is focusing on the record (proof and calculation theory and application). George Boolos 'logic is generalized and the meaning of expression is discussed. Institute of Mathematical Analysis, Kurata Institute of Mathematical Analysis

项目成果

合流性とZ定理について

关于汇合和 Z 定理

• 发表时间: 2021
• 作者: R.Akasaka;K.Fujita;K.Nakazawa
• 通讯作者: K.Nakazawa

Fujita Kenetsu

藤田健越

A category-like structure of computational paths for parallel reduction

用于并行归约的计算路径的类类别结构

• 发表时间: 2020
• 期刊: 京都大学数理解析研究所講究録
• 作者: K. Fujita

研究者情報

研究员信息

Confluence proofs of lambda-mu-calculi by Z theorem

Z 定理的 lambda-mu 演算的汇合证明

• DOI: 10.1007/s11225-020-09931-0
• 发表时间: 2021
• 期刊: Studia Logica
• 影响因子: 0.7
• 作者: Y. Honda;K. Nakawaza;K. Fujita
• 通讯作者: K. Fujita