Godel's system T and computational complexity hierarchy

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

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