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

ラムダ計算の型問題に対する可解性・非可解性の特徴付け

研究課題

研究課題/領域番号 25400192
研究種目

基盤研究(C)

配分区分基金
応募区分一般
研究分野 数学基礎・応用数学
研究機関群馬大学

研究代表者

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

研究分担者 古森 雄一  千葉大学, 大学院理学研究科, 名誉教授 (10022302)
倉田 俊彦  法政大学, 経営学部, 教授 (40311899)
研究協力者 Schubert Aleksy  University of Warsaw, Institute of Informatics, Professor
鹿島 亮  東京工業大学, 情報理工学院, 准教授
中澤 巧爾  名古屋大学, 情報科学研究科, 准教授
松田 直祐  神奈川大学, 理学部, 助手
研究期間 (年度) 2013-04-01 – 2017-03-31
研究課題ステータス 完了 (2016年度)
配分額 *注記
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2015年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2014年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
キーワードラムダ計算 / 型検査問題 / 型推論問題 / 決定可能性 / チャーチ流 / カリー流 / チャーチ・ロッサーの定理 / 型検査 / 型推論 / 合流性
研究成果の概要

ラムダ式の定式化と型問題の決定可能性との依存関係を詳細に研究した.そのために,決定可能な定式化(チャーチ流)と決定不能な定式化(カリー流)との間に位置する中間的構造を持つラムダ式を系統分類的に導入した.そして,式のスタイルに順序関係を導入して,式のスタイルでパラメータ化された型問題の定式化を与えることができた.これにより,ラムダ式の基本問題や性質が,スタイルのパラメータで分類されて,問題の本質的条件を解明する枠組みが得られた.これらにより,ラムダ計算の型問題に対する可解性・非可解性の特徴づけを式のスタイルの観点から明らかにすることができた.

報告書

(5件)
  • 2016 実績報告書   研究成果報告書 ( PDF )
  • 2015 実施状況報告書
  • 2014 実施状況報告書
  • 2013 実施状況報告書
  • 研究成果

    (35件)

すべて 2017 2016 2015 2014 2013 その他

すべて 国際共同研究 (2件) 雑誌論文 (13件) (うち査読あり 8件、 謝辞記載あり 3件、 オープンアクセス 2件) 学会発表 (14件) (うち国際学会 1件、 招待講演 1件) 備考 (6件)

  • [国際共同研究] Warsow University(Poland)

    • 関連する報告書
      2016 実績報告書
  • [国際共同研究] Warsaw University(Poland)

    • 関連する報告書
      2015 実施状況報告書
  • [雑誌論文] On Upper Bounds on the Church-Rosser Theorem2017

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

      Electronic Proceedings in Theoretical Computer Science

      巻: Vol. 235

    • 関連する報告書
      2016 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Reduction Rules for Intuitionistic lambda-rho-calculus2015

    • 著者名/発表者名
      K. Fujita, R. Kashima, Y. Komori, N. Matsuda
    • 雑誌名

      Studia Logica

      巻: 103 号: 6 ページ: 1225-1244

    • DOI

      10.1007/s11225-015-9616-1

    • 関連する報告書
      2015 実施状況報告書
    • 査読あり
  • [雑誌論文] On styles of lambda2-terms --Extended abstract --2015

    • 著者名/発表者名
      K. Fujita
    • 雑誌名

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

      巻: 1950

    • 関連する報告書
      2015 実施状況報告書
    • オープンアクセス / 謝辞記載あり
  • [雑誌論文] On Sheaves Categorically Equivalent to Distributive Concrete Domains2015

    • 著者名/発表者名
      倉田俊彦
    • 雑誌名

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

      巻: 1950

    • 関連する報告書
      2015 実施状況報告書
    • オープンアクセス
  • [雑誌論文] On sheaves categorically equivalent to distributive concrete domains2015

    • 著者名/発表者名
      倉田俊彦
    • 雑誌名

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

      巻: --

    • 関連する報告書
      2014 実施状況報告書
  • [雑誌論文] Existential type systems between Church and Curry style (type-free style)2014

    • 著者名/発表者名
      K. Fujita, A. Schubert
    • 雑誌名

      Theoretical Computer Science

      巻: 549 ページ: 17-35

    • DOI

      10.1016/j.tcs.2014.05.019

    • 関連する報告書
      2014 実施状況報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] A note on subject reduction in (->, E)-Curry with respect to complete developments2014

    • 著者名/発表者名
      A. Scuhbert and K. Fujita
    • 雑誌名

      Information Processing Letters

      巻: 114 号: 1-2 ページ: 72-75

    • DOI

      10.1016/j.ipl.2013.07.027

    • 関連する報告書
      2013 実施状況報告書
    • 査読あり
  • [雑誌論文] ラムダ計算の型問題について--数学基礎論からプログラミング言語の構造へ--2014

    • 著者名/発表者名
      藤田憲悦
    • 雑誌名

      数学

      巻: 66

    • NAID

      130006882589

    • 関連する報告書
      2013 実施状況報告書
    • 査読あり
  • [雑誌論文] A Simplified Proof of the Church-Rosser Theorem2014

    • 著者名/発表者名
      Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa
    • 雑誌名

      Studia Logica

      巻: 102 号: 1 ページ: 175-183

    • DOI

      10.1007/s11225-013-9470-y

    • 関連する報告書
      2013 実施状況報告書
    • 査読あり
  • [雑誌論文] Decidable structures between Church-style and Curry-style2013

    • 著者名/発表者名
      K. Fujita and A. Schubert
    • 雑誌名

      Leibniz International Proceedings in Informatics

      巻: 21

    • 関連する報告書
      2013 実施状況報告書
    • 査読あり
  • [雑誌論文] On fine structures between Church-style and Curry-style lambda2-terms2013

    • 著者名/発表者名
      藤田憲悦
    • 雑誌名

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

      巻: 1832

    • 関連する報告書
      2013 実施状況報告書
  • [雑誌論文] Sheaf-theoretical representation of concrete domains2013

    • 著者名/発表者名
      倉田俊彦
    • 雑誌名

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

      巻: 1832 ページ: 8-18

    • 関連する報告書
      2013 実施状況報告書
  • [雑誌論文] Lambda rho-calculus II2013

    • 著者名/発表者名
      Yuich Komori
    • 雑誌名

      Tsukuba Journal of Mathematics

      巻: 37

    • 関連する報告書
      2013 実施状況報告書
    • 査読あり
  • [学会発表] 高階逐次アルゴリズムの分解について2017

    • 著者名/発表者名
      倉田俊彦
    • 学会等名
      日本数学会
    • 発表場所
      首都大学東京
    • 年月日
      2017-03-25
    • 関連する報告書
      2016 実績報告書
  • [学会発表] On the Church-Rosser theorem2016

    • 著者名/発表者名
      K. Fujita
    • 学会等名
      Mathematical Society of Japan
    • 発表場所
      Kansai University
    • 年月日
      2016-09-18
    • 関連する報告書
      2016 実績報告書
  • [学会発表] Compositional Z: confluence proofs for permutative conversion2016

    • 著者名/発表者名
      K. Nakazawa and K. Fujita
    • 学会等名
      JAIST JSPS Core-to-Core Program
    • 発表場所
      Kyoto University
    • 年月日
      2016-09-16
    • 関連する報告書
      2016 実績報告書
  • [学会発表] Church-Rosser theorem and Compositional Z-property2016

    • 著者名/発表者名
      K. Fujita and K. Nakazawa
    • 学会等名
      Japan Society of Software Science and Technology
    • 発表場所
      Tohoku University
    • 年月日
      2016-09-06
    • 関連する報告書
      2016 実績報告書
  • [学会発表] On upper bound on the Church-Rosser theorem2016

    • 著者名/発表者名
      K. Fujita
    • 学会等名
      3rd Workshop on Rewriting Techniques for Program Transformation and Evaluation
    • 発表場所
      University of Porto
    • 年月日
      2016-06-23
    • 関連する報告書
      2016 実績報告書
    • 国際学会
  • [学会発表] 定理証明とモデル検査2016

    • 著者名/発表者名
      藤田憲悦
    • 学会等名
      電子情報通信学会2016年総合大会
    • 発表場所
      九州大学
    • 年月日
      2016-03-16
    • 関連する報告書
      2015 実施状況報告書
    • 招待講演
  • [学会発表] Compositional Z: Confluence Proofs for Permutative Conversion2015

    • 著者名/発表者名
      K. Nakazawa, K. Fujita
    • 学会等名
      日本ソフトウェア科学会
    • 発表場所
      早稲田大学
    • 年月日
      2015-09-08
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] 置換簡約を含むラムダ計算の合流性2015

    • 著者名/発表者名
      中澤巧爾,藤田憲悦
    • 学会等名
      第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)
    • 発表場所
      松山市
    • 年月日
      2015-03-04 – 2015-03-06
    • 関連する報告書
      2014 実施状況報告書
  • [学会発表] On styles of lambda2-terms2014

    • 著者名/発表者名
      K. Fujita
    • 学会等名
      RIMS研究集会「証明論・計算論とその周辺」
    • 発表場所
      京都大学数理解析研究所
    • 年月日
      2014-12-24 – 2014-12-26
    • 関連する報告書
      2014 実施状況報告書
  • [学会発表] On sheaves categorically equivalent to distributive concrete domains2014

    • 著者名/発表者名
      倉田俊彦
    • 学会等名
      RIMS研究集会「証明論・計算論とその周辺」
    • 発表場所
      京都大学数理解析研究所
    • 年月日
      2014-12-24 – 2014-12-26
    • 関連する報告書
      2014 実施状況報告書
  • [学会発表] 分配具象領域と領域層の圏論的同等性に関する考察2014

    • 著者名/発表者名
      倉田俊彦
    • 学会等名
      日本数学会秋季総合分科会
    • 発表場所
      広島大学
    • 年月日
      2014-09-28
    • 関連する報告書
      2014 実施状況報告書
  • [学会発表] ラムダ計算の型問題を支配する本質的情報について

    • 著者名/発表者名
      藤田憲悦
    • 学会等名
      日本ソフトウェア科学会第30回大会
    • 発表場所
      東京大学
    • 関連する報告書
      2013 実施状況報告書
  • [学会発表] Intermediate lambda-terms between Church and Curry

    • 著者名/発表者名
      K. Fujita and A. Schubert
    • 学会等名
      日本数学会2014年度年会
    • 発表場所
      学習院大学
    • 関連する報告書
      2013 実施状況報告書
  • [学会発表] Sheaf-theoretical representation of concrete domains

    • 著者名/発表者名
      倉田俊彦
    • 学会等名
      日本数学会秋季総合分科会
    • 発表場所
      愛媛大学
    • 関連する報告書
      2013 実施状況報告書
  • [備考] Research

    • URL

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

    • 関連する報告書
      2016 実績報告書 2015 実施状況報告書
  • [備考] Conference, Workshop, Meeting

    • URL

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

    • 関連する報告書
      2015 実施状況報告書 2014 実施状況報告書
  • [備考] ラムダ計算と論理の早春セミナー

    • URL

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

    • 関連する報告書
      2015 実施状況報告書 2014 実施状況報告書
  • [備考] Resarch

    • URL

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

    • 関連する報告書
      2014 実施状況報告書
  • [備考] Research

    • URL

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

    • 関連する報告書
      2013 実施状況報告書
  • [備考] Conference, Workshop, Meeting

    • URL

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

    • 関連する報告書
      2013 実施状況報告書

URL: 

公開日: 2014-07-25   更新日: 2019-07-29  

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

Powered by NII kakenhi