古典論理計算系から直観主義論理計算系への翻訳

• 研究課題/領域番号: 24650002
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: 情報学基礎
• 研究機関: 千葉大学
• 研究代表者: 桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
• 研究協力者: 佐藤 雅彦 ; 菊池 健太郎
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円); 2014年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2013年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2012年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
• キーワード: 古典論理 / 直観主義論理 / 簡約保存 / CPS変換 / 強正規化性 / C(G)PS変換 / intersection-union / intersection-product / 表示的意味

研究成果の概要

本研究では、古典論理の計算系から直観主義論理の計算系への簡約を保存する翻訳を与える。本研究で考察する古典論理の計算系は、lambda-bar-mu、名前呼びlambda-bar-mu-tilde、値呼びlambda-bar-mu-tildeおよびlambda-muであり、いくつかの簡単な翻訳を合成することにより、新規および既知の翻訳を統一的に導くことができる。そしてこれより上記の古典論理計算系の強正規化性を導くことができる。

研究成果

• [雑誌論文] A Translation of Intersection and Union Types for the λμ-Calculus (2014)
  • 著者名/発表者名: K. Kikuchi, T. Sakurai
  • 雑誌名: Lecture Note in Computer Science (Proceedings of 12th Asian Symposium on Programming Languages and Systems) 巻: LNCS 8858 ページ: 120-139
  • DOI: 10.1007/978-3-319-12736-1_7
  • ISBN: 9783319127354, 9783319127361
  • 査読あり / 謝辞記載あり
• [雑誌論文] Viewing λ-terms through Maps (2013)
  • 著者名/発表者名: M. Sato, R. Pollack, H. Schwichtenberg, T. Sakurai
  • 雑誌名: Indagationes Mathematicae 巻: 24 号: 4 ページ: 1073-1104
  • DOI: 10.1016/j.indag.2013.08.003
  • 査読あり
• [学会発表] A Translation of Intersection and Union Types for the λμ-Calculus (2014)
  • 著者名/発表者名: K. Kikuchi, T. Sakurai
  • 学会等名: Fifth International Workshop on Classical Logic and Computation (CL&C'14)
  • 発表場所: Vienna, Austria
  • 年月日: 2014-07-13
• [学会発表] Viewing λ-terms through Maps (2013)
  • 著者名/発表者名: M. Sato, R. Pollack, H. Schwichtenberg, T. Sakurai
  • 学会等名: TYPES Meeting 2013
  • 発表場所: Toulouse, France