| 研究課題/領域番号 |
20K03711
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 情報学部, 准教授 (30228994)
|
|---|
| 研究分担者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | ラムダ計算 / 合流性 / チャーチ・ロッサーの定理 / 定量的評価 / カリー・ハワード同型 / 直観主義論理 / スペクトラル空間モデル / ブーロスの論理パズル |
|---|
| 研究実績の概要 |
全ての問題の根幹に関わる基本的性質の一つとして計算の複雑さの問題がある．この問題を証明と形式化された計算との関係から研究を行った．特に，カリー・ハワード同型と証明の形式化の観点から，グリベンコの定理，ゲーデル・ゲンツェンの変換，コルモゴロフの変換，黒田の変換の二重否定による埋め込みとプログラム変換との対応をラムダ・ミュー計算を使って形式化を行い統一的にまとめてチュートリアルを行った．この結果は，数理解析研究所講究録（数理論理学とその応用）から発表した．
また，抽象書換系の合流性とZ性について，合成的Z定理の観点からサーベーを行って，その結果を数理解析研究所講究録（証明と計算の理論と応用）から赤坂，中澤との共著論文として発表した．さらに，従来のZ定理では困難であるが，合成的Z定理を使って値呼び計算体系の合流性を示した．従来手法では停止性とHindley-Rosenの補題から証明されていたが，合成的Z定理を適用すると停止性から独立に証明可能となった．本結果は，Mathematical Structures in Computer Science (Cambridge University Press) から，中澤，今川との共著論文として発表した．
一方，直観主義論理の代数的モデルに関するこれまでの成果（Fundamenta Informaticae 2019年）をさらに再構築して，Stoneの表現定理より，完全分配代数的束に基づく代数的モデルでも完全性が証明できることを数理解析研究所講究録（証明と計算の理論と応用）から発表して，今後の更なる進展の足がかりを作った．
また，George Boolosの論理バズルを一般化して，表示的意味論の観点から考察を与えた．そして，数理解析研究所にて，倉田との共同研究として発表を行なった．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
カリー・ハワード同型と証明の形式化に関するチュートリアル，合成的Z定理に関する調査研究，及び，合成的Z定理を活用した合流性の新証明の発表を行なった．また，2階直観主義論理の代数的モデルと位相モデルの関係を明確にする考察も与えることができた．さらに，論理パズルを一般化して，表示的意味論の観点からその解法についての考察も与えた．
以上について，研究会等で研究発表とチュートリアルを合計２件行い，また，学術雑誌，講究録など合計５編の研究論文を発表してきた．
|
| 今後の研究の推進方策 |
証明の形式化の観点から，証明と計算の相互作用を深化させて，計算量の基本問題を多面的角度から追求するために，型付き計算体系の型理論が様々な特徴量でパラメータ化された形式的体系を構築していく．今後の研究については，特に，2階直観主義論理の非可解性に関する証明，及び直観主義論理の代数的モデルと位相的モデルの一般的な対応枠組みについての研究を重点的に推進していく方策である．
|
| 次年度使用額が生じた理由 |
代表者の業務の多忙，親族の介護，身内の不幸，代表者の入院，世界的な社会情勢等を考慮して，国際共同研究を延期した．
次年度については，渡航先の外国機関とも調整をして未解決問題の共同研究，共著論文の完成に向けて使用計画と準備が定まり，遂行中である．
|
| 備考 |
書籍情報
https://www.coronasha.co.jp/np/isbn/9784339029239/
|
