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

2018 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 – 2020-03-31
Keywordsラムダ計算 / チャーチ・ロッサーの定理 / グルジェゴルチック階層 / 並行変換 / 簡約列 / 計算の複雑さ
Outline of Annual Research Achievements

ラムダ計算や書換え系に代表される簡約システムの停止性,合流性などの存在定理を定量的に評価する一般的枠組みを構築することを目指して研究を行なった.そして,並行簡約と逐次簡約との関係を明示的に与えることでグルジェゴルチック階層に基づく一般的枠組みを構築することができた.これは,型無しラムダ計算に限らず,ゲーデルのシステムTやジラルのシステムF,Pure Type Systemsなど型のある計算体系でも同様に有効な枠組みであることが明らかになった.
これらの研究成果の一部は,Information and Computation(Elsevier)から研究論文として出版して,オープンアクセスとした.また,Swansea大学(イギリス),Chalmers工科大学(スウェーデン)でもそれぞれ発表を行なった.
こららの結果と関連する研究成果については,第49回書換え系研究集会(伊香保),第21回プログラミングおよびプログラミング言語ワークショップPPL2019(花巻),ラムダ計算と論理の早春セミナー(草津),日本数学会2019年度年会(東京工業大学)においてそれぞれ研究発表を行なった.
また,Munchen大学,Swansea大学,Chalmers大学の海外研究協力者とそれぞれ複数回にわたり建設的な研究討議を行って,定理証明システム,計算量,計算体系に関する有益な知見を得ることができた.
さらに,10年ほど前から継続して研究してきた計算モデルの束論的意味論に関して進展があり,その研究成果は研究分担者との共著論文にまとめて学会誌に現在投稿中である.また,研究実績の概要は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

チャーチ・ロッサーの定理に対して,簡約(reduction)と展開(expansion)の出現数の関数として合流点までの計算のステップ数の上限を一般的枠組みの中で与えることができた.
また,計算ステップ数の下限に関しては,海外研究協力者(Munchen大学)と研究討議を行って様々な知見を得ることができた.
さらに,計算モデルの束論的意味論に関しては大きな進展があり,その成果は研究分担者との共著論文としてまとめて現在投稿中である.

Strategy for Future Research Activity

本研究で得られた上限の一般的枠組みについては引き続き調査検討を重ねていく.また,計算のステップ数に限らず,計算の道の本数についてもその特徴を解析していく.
さらに,進展があった意味論的観点から計算量へのフィードバックを明らかにしていく.
これらの方策により,計算と論理の意味論的・証明論的視点から計算量を特徴付ける研究を推進していく.

Causes of Carryover

国際共同研究のために複数の国に滞在計画であり,そのために有効に使用できる.

  • Research Products

    (12 results)

All 2019 2018 Other

All Int'l Joint Research (3 results) Journal Article (3 results) (of which Peer Reviewed: 1 results,  Open Access: 1 results) Presentation (5 results) (of which Int'l Joint Research: 2 results) Remarks (1 results)

  • [Int'l Joint Research] Ludwig-Maximilians-Universitat Munchen(ドイツ)

    • Country Name
      GERMANY
    • Counterpart Institution
      Ludwig-Maximilians-Universitat Munchen
  • [Int'l Joint Research] Chalmers University of Technology(スウェーデン)

    • Country Name
      SWEDEN
    • Counterpart Institution
      Chalmers University of Technology
  • [Int'l Joint Research] Swansea Univeristy(英国)

    • Country Name
      UNITED KINGDOM
    • Counterpart Institution
      Swansea Univeristy
  • [Journal Article] The Church--Rosser theorem and quantitative analysis of witnesses2018

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

      Information and Computation

      Volume: 263 Pages: 52~56

    • DOI

      https://doi.org/10.1016/j.ic.2018.09.002

    • Peer Reviewed / Open Access
  • [Journal Article] The Church--Rosser theorem and analysis of reduction length2018

    • Author(s)
      K. Fujita
    • Journal Title

      Kyoto University, RIMS Kokyuroku

      Volume: 2083 Pages: 124--136

  • [Journal Article] Distributive Concrete Domains and Sheaves on DI-Domains2018

    • Author(s)
      Toshihiko Kurata
    • Journal Title

      Kyoto University, RIMS Kokyuroku

      Volume: 2083 Pages: 137--145

  • [Presentation] Z定理を用いたlambda mu計算の合流性証明2019

    • Author(s)
      Y. Honda, K. Nakazawa, K. Fujita
    • Organizer
      第21回プログラミングおよびプログラム言語ワークショップPPL2019
  • [Presentation] A formal system of reduction paths for parallel reduction2019

    • Author(s)
      K. Fujita
    • Organizer
      ラムダ計算と論理の早春セミナー
  • [Presentation] A formal system of reduction paths for parallel reduction2019

    • Author(s)
      K. Fujita
    • Organizer
      日本数学会2019年度年会
  • [Presentation] A constructive proof of the Church--Rosser theorem2018

    • Author(s)
      K. Fujita
    • Organizer
      Workship on Type Theory and Lambda Calculus (Chalmers University)
    • Int'l Joint Research
  • [Presentation] A constructive proof of the Church--Rosser theorem2018

    • Author(s)
      K. Fujita
    • Organizer
      End-of-Summer Logic Minisymposium (Seansea University)
    • Int'l Joint Research
  • [Remarks]

    • URL

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

URL: 

Published: 2019-12-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi