• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2019 Fiscal Year Research-status Report

簡約システムの存在定理に関する定量的性質の解明

Research Project

Project/Area Number 17K05343
Research InstitutionGunma University

Principal Investigator

藤田 憲悦  群馬大学, 大学院理工学府, 准教授 (30228994)

Co-Investigator(Kenkyū-buntansha) 倉田 俊彦  法政大学, 経営学部, 教授 (40311899)
Project Period (FY) 2017-04-01 – 2021-03-31
Keywordsラムダ計算 / チャーチ・ロッサーの定理 / グルジェゴルチック階層 / 並行変換 / 簡約列 / 隣接行列 / 箙 / 計算の複雑さ
Outline of Annual Research Achievements

ラムダ計算や書き換え系に代表される簡約システムの停止性や合流性などの存在定理の複雑さを定量的に評価する一般的な枠組みを構築することを目指して研究を行った.そして,箙から計算の道を帰納的に生成する形式的体系を与えることができた.この体型に基づくと,生成される計算の道は転置とテンソル積を使うことでシステマティックに行列表現に落とし込むことができる.これにより,計算の道の本数を隣接行列の行列計算で機械的に数えることができた.この結果は,Theoretical Computer Science (Elsevier)から研究論文として出版された.なお,この論文は今後オープンアクセスを予定している.
さらに,高階の計算モデルと束論的意味論に関して大きな進展があり,完全な意味論を構築することに成功した.この結果を研究分担者との共著による研究論文にまとめて,Fundamenta Informaticae (IOS Press)からオープンアクセスとして出版した.
これらの研究成果と関連する結果については,日本数学会2019年度秋季総合分科会(金沢大学),京都大学数理解析研究所 RIMS共同研究 「証明論とその周辺」,第52回項書換え系研究集会,日本数学会2020年度年会(日本大学理工学部,但し社会情勢のために開催は中止されたがアブストラクトは出版された)においてそれぞれ研究発表を行った.
また,研究実績の概要は次のWebページ
http://www.cs.gunma-u.ac.jp/~fujita/
からも公開して最新の情報を発信している.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

簡約システムの存在定理に関する定量的性質の解明のために,これまでにチャーチ・ロッサーの定理の観点から,簡約列の長さとその道の本数を評価することができた.
そして,雑誌論文6件(その内,査読付き3件),国際会議発表4件,国内学会・研究会等の発表8件を行い研究を実施してきた.

Strategy for Future Research Activity

本研究で得られた結果の最適性についても引き続き検証を重ねていく.そして,ゲーデルの体型など他の計算体系に対しても本手法を適用してその汎用性を確認していく.
この方策により,計算と論理の意味論的観点,証明論的観点から研究を俯瞰的に推進していく.

Causes of Carryover

研究目的を精緻に達成するために,日本数学会,研究集会への参加,および研究発表を予定していた.しかし,社会情勢によりこれらの学会と研究会が中止に追い込まれた.今後の学会,研究会において当初に予定されていた研究発表を行っていく計画である.

  • Research Products

    (9 results)

All 2020 2019 Other

All Journal Article (2 results) (of which Peer Reviewed: 2 results,  Open Access: 2 results) Presentation (6 results) Remarks (1 results)

  • [Journal Article] A formal system of reduction paths for parallel reduction2020

    • Author(s)
      Fujita Ken-etsu
    • Journal Title

      Theoretical Computer Science

      Volume: 813 Pages: 327~340

    • DOI

      10.1016/j.tcs.2020.01.002

    • Peer Reviewed / Open Access
  • [Journal Article] Neighbourhood and Lattice Models of Second-Order Intuitionistic Propositional Logic2019

    • Author(s)
      Kurata Toshihiko、Fujita Ken-etsu
    • Journal Title

      Fundamenta Informaticae

      Volume: 170 Pages: 223~240

    • DOI

      10.3233/FI-2019-1861

    • Peer Reviewed / Open Access
  • [Presentation] George Boolos' "The Hardest Logic Puzzle Ever" Revisited2020

    • Author(s)
      K. Fujita
    • Organizer
      第52回TRS研究集会
  • [Presentation] George Boolos' "The Hardest Logic Puzzle Ever" Revisited2020

    • Author(s)
      K. Fujita
    • Organizer
      日本数学会2020年度年会(日本大学理工学部)
  • [Presentation] Equational theory and reduction rules of reduction paths2019

    • Author(s)
      K. Fujita
    • Organizer
      日本数学会2019年度秋季総合分科会(金沢大学)
  • [Presentation] ラムダ計算の簡約グラフについて2019

    • Author(s)
      富岡峻士,藤田憲悦
    • Organizer
      京都大学数理解析研究所 RIMS共同研究 「証明論とその周辺」
  • [Presentation] A category-like structure of computational paths for parallel reduction2019

    • Author(s)
      K. Fujita
    • Organizer
      京都大学数理解析研究所 RIMS共同研究 「証明論とその周辺」
  • [Presentation] Confluence Proof of λμ Calculus by Z Theorem2019

    • Author(s)
      本多雄樹,中澤巧爾,藤田憲悦
    • Organizer
      京都大学数理解析研究所 RIMS共同研究 「証明論とその周辺」
  • [Remarks] 藤田研究室

    • URL

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

URL: 

Published: 2021-01-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi