• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2021 年度 実施状況報告書

ゲーデルのシステムTと計算量的階層に関する研究

研究課題

研究課題/領域番号 20K03711
研究機関群馬大学

研究代表者

藤田 憲悦  群馬大学, 情報学部, 准教授 (30228994)

研究分担者 倉田 俊彦  法政大学, 経営学部, 教授 (40311899)
研究期間 (年度) 2020-04-01 – 2023-03-31
キーワードラムダ計算 / 合流性 / Z定理 / チャーチ・ロッサーの定理 / スペクトラル空間モデル / 直観主義論理 / 数理パズル / 形式化
研究実績の概要

計算の複雑さに関する基本的性質として,計算可能性・計算量の問題を本質的に特徴付けている基本概念は何かという根本問題がある.この問題を証明と形式化された計算との関係から研究を行った.Church―Rosserの定理のシステマチックな証明のために,Z定理を拡張した分割統治的な手法を導入した.この手法により,値呼びラムダ計算の合流性の証明を与えることができた.この結果は,査読付き論文として現在投稿中である(中澤,藤田,今川の共著論文).
また,2階直観主義論理のスペクトラル空間モデルについての研究も継続して行い,完全性と健全性の証明を構築中である.この研究成果は,京都大学数理解析研究所RISM研究集会(証明と計算の理論と応用)と日本数学会2022年度年会(数学基礎論)においてそれぞれ研究発表を行なった.加えて,形式化・記号化に関して,スマリヤン・ブーロース流の論理パズルの形式化を行なって,論理式による特徴付けを明らかにした.さらに,その問題の数学的な一般化についても研究を行った.この結果は,日本数学会2021年度秋季総合分科会(数学基礎論)と京都大学数理解析研究所RIMS共同研究(論理・代数系・言語と計算機科学の周辺領域)でそれぞれ研究発表を行なった.これに関連して,数理パズル,ゲーデルの完全性定理,カリー・ハワード同型に関する内容をまとめて専門書として出版した.また,第24回プログラミングおよびプログラミング言語ワークショップ(日本ソフトウェア科学会PPL2022)でプログラム委員会委員を務めて,査読と情報収集などにあたった.
以上の研究成果の概要は次のWebページ
http://www.cs.gunma-u.ac.jp/~fujita/
からも公開しており,研究成果の内容を分かりやすく情報発信している.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

値呼びラムダ計算の合流性の証明をZ定理の拡張の方針で与えることができた.
2階直観主義論理のスペクトラル空間モデルの完全性と健全性定理の証明方針が明らかになってきた.
スマリヤン・ブーロース流の論理パズルの形式化を行なって,論理式による特徴付けを明らかにした.この成果も含めて,数理論理学の専門書を出版した.
以上について,学会・研究会等において5件の研究発表を行って,研究を遂行してきた.

今後の研究の推進方策

形式化の観点から,証明と計算の相互作用の深化を図り,計算量の基本問題を多面的角度から追求するために,型付き計算体系の型理論が,ソートの階層,型の階層でパラメータ化された形式的体系を構築していく.これにより,証明と形式化された計算との深淵な関係についての研究を継続していく.

次年度使用額が生じた理由

学会,研究会などがオンラインに制限されたことによる.今後は状況を注視しつつ,研究発表,研究打ち合わせなどの旅費も活用していく計画である.

  • 研究成果

    (10件)

すべて 2022 2021 その他

すべて 雑誌論文 (2件) (うち査読あり 1件) 学会発表 (5件) 図書 (1件) 備考 (2件)

  • [雑誌論文] Confluence Proofs of Lambda-Mu-Calculi by Z Theorem2021

    • 著者名/発表者名
      Honda Yuki、Nakazawa Koji、Fujita Ken-etsu
    • 雑誌名

      Studia Logica

      巻: 109 ページ: 917~936

    • DOI

      10.1007/s11225-020-09931-0

    • 査読あり
  • [雑誌論文] On formalization of logic puzzles a la Smullyan2021

    • 著者名/発表者名
      Kenetsu Fujita
    • 雑誌名

      京都大学数理解析研究所講究録

      巻: 2193 ページ: 18~24

  • [学会発表] Spectral Spaces for Models of Intuitionistic Logic2022

    • 著者名/発表者名
      T.Kurata, K.Fujita
    • 学会等名
      日本数学会2022年度年会
  • [学会発表] A general form on the logic puzzle of Boolos2022

    • 著者名/発表者名
      K.Fujita, T.Kurata
    • 学会等名
      京都大学数理解析研究所RIMS共同研究 (Logic, Algebraic System, Language and Related Areas in Computer Science)
  • [学会発表] 合流性とZ定理について2021

    • 著者名/発表者名
      R.Akasaka, K.Fujita, K.Nakazawa
    • 学会等名
      京都大学数理解析研究所RIMS共同研究(証明論と計算の理論と応用)
  • [学会発表] Spectral spaces for models of intuitonistic logic2021

    • 著者名/発表者名
      T.Kurata, K.Fujita
    • 学会等名
      京都大学数理解析研究所RIMS共同研究(証明論と計算の理論と応用)
  • [学会発表] On formalization of logic puzzles a la George Boolos2021

    • 著者名/発表者名
      K.Fujita, T.Kurata
    • 学会等名
      日本数学会2021年度秋季総合分科会(数学基礎論)
  • [図書] 数理パズルで楽しく学べる論理学2022

    • 著者名/発表者名
      藤田 憲悦
    • 総ページ数
      200
    • 出版者
      コロナ社
    • ISBN
      978-4-339-02923-9
  • [備考] 研究者情報

    • URL

      https://researchers-info.st.gunma-u.ac.jp/ei_fujita_kenetsu/

  • [備考] 藤田研究室

    • URL

      http://www.cs.gunma-u.ac.jp/~fujita/

URL: 

公開日: 2022-12-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi