古典論理の構文論的双対性とその計算論的意味

• 研究課題/領域番号: 18700008
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 京都大学
• 研究代表者: 中澤 巧爾 京都大学, 大学院・情報学研究科, 助教 (80362581)
• 研究期間 (年度): 2006 – 2008
• 研究課題ステータス: 完了 (2008年度)
• 配分額: 2,510千円 (直接経費: 2,300千円、間接経費: 210千円); 2008年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2007年度: 700千円 (直接経費: 700千円); 2006年度: 900千円 (直接経費: 900千円)
• キーワード: 古典論理 / シーケント計算 / カット除去 / 自然演繹 / カリーハワード同型 / 存在型 / 型検査 / 型推論 / 決定問題 / CPS変換 / 置換簡約 / 一般除去規則 / 自然演出繹 / 証明正規化 / 強正規化性 / 合流性

研究概要

本研究では以下の結果を得た。(1) 直観主義シーケント計算のカット除去として、自然演繹の証明正規化と同型であるものを提案した。(2) 存在型を持つ型付きラムダ計算における型検査問題、型推論問題が決定不能であることを証明した。

研究成果

• [雑誌論文] Type Checking and Inference for Polymorphic and Existential Types. (2009)
  • 著者名/発表者名: Koji Nakazawa and Makoto Tatsuta
  • 雑誌名: Computing : The Australasian Theory Symposium (CATS2009) (CD-ROM)
  • 査読あり
• [雑誌論文] Type Checking and Inference for Polymorphic and Existential Types (2009)
  • 著者名/発表者名: K. Nakazawa and M. Tatsuta
  • 雑誌名: Computing : The Australasian Theory Symposium (CATS'09) (CD-ROM)
  • 査読あり
• [雑誌論文] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. (2008)
  • 著者名/発表者名: Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
  • 雑誌名: Computer Science Logic (CSL' 08), Lecture Notes in Computer Science 5213 ページ: 478-492
  • 査読あり
• [雑誌論文] Strong Normalization of Classical Natural Deduction with Disjunctns (2008)
  • 著者名/発表者名: Koji Nakazawa and Makoto Tatsuta
  • 雑誌名: Annals of Pure and Applied Logic 153 ページ: 21-37
  • 査読あり
• [雑誌論文] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence (2008)
  • 著者名/発表者名: K. Nakazawa, M. Tatsuta, Y. Kameyama, and H. Nakano
  • 雑誌名: Computer Science Logic (CSL'09) ページ: 478-492
  • 査読あり
• [雑誌論文] Strong normalization of classical natural deduction with disjunctions (2008)
  • 著者名/発表者名: Koji Nakazawa and Makoto Tatsuta
  • 雑誌名: Annals of Pure and Applied Logic 153 ページ: 21-37
  • 査読あり
• [雑誌論文] An Isomorphism between Cut-Elimination Procedure and Proof Reduction (2007)
  • 著者名/発表者名: Koji Nakazawa
  • 雑誌名: Typed Lambda Calculi and Applications (TLCA' 07), Lecture Notes in Computer Science 4583 ページ: 336-350
  • 査読あり
• [雑誌論文] An Isomorphism Between Cut-Elimination Procedure and Proof Reduction (2007)
  • 著者名/発表者名: Koji Nakazawa
  • 雑誌名: Typed Lambda Calculi and Applications (TLCA2007) ページ: 336-350
  • 査読あり
• [雑誌論文] An isomorphism between cut-elimination procedure and proof reduction (2007)
  • 著者名/発表者名: Koji Nakazawa
  • 雑誌名: Typed Lambda Calculi and Applications (TLCA'07) (To appear)
• [雑誌論文] Strong Normalization Proofs by CPS-Translations (2006)
  • 著者名/発表者名: Satoshi Ikeda and Koji Nakazawa
  • 雑誌名: Information Processing Letters 99 ページ: 163-170
  • 査読あり
• [雑誌論文] Strong normalization proofs by CPS-translations (2006)
  • 著者名/発表者名: Satoshi Ikeda, Koji Nakazawa
  • 雑誌名: Information Processing Letters 99 ページ: 163-170
• [学会発表] 存在型に対する型検査問題と型推論問題の同値性 (2009)
  • 著者名/発表者名: 加藤祐輝, 中澤巧爾
  • 学会等名: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), ポスター
• [学会発表] An Isomorphism between Cut-Elimination Procedure and Proof Reduction (2007)
  • 著者名/発表者名: Koji Nakazawa
  • 学会等名: SCORE Summer Workshop on Symbolic Computation and Software Verification
• [学会発表] trong Cut-Elimination and CPS-Translations. (In T. Kutsia and M. Marin, eds.) (2007)
  • 著者名/発表者名: Koji Nakazawa
  • 学会等名: Austria-Japan Workshop on Symbolic Computation and Software Verification, No. 07-09 in RISC-Linz Report Series,