Classical logic and infinite phenomena in computation

• Project/Area Number: 15K00012
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Nagoya University
• Principal Investigator: Nakazawa Koji 名古屋大学, 情報学研究科, 准教授 (80362581)
• Project Period (FY): 2015-04-01 – 2018-03-31
• Project Status: Completed (Fiscal Year 2017)
• Budget Amount: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
• Keywords: ラムダ計算 / 古典論理 / 合流性 / ラムダ・ミュー計算 / カット除去 / 交叉型

Outline of Final Research Achievements

The results of this project are the following: (1) We study some fundamental properties of the Lambda-mu calculus, which is a computational model of programming language with stream data. In particular, We propose a new proof technique, called the compositional Z theorem, to prove confluence of the calculus. (2) We show that the compositional Z theorem can be widely applied to prove confluence of several calculi with permutation-like reduction, such as the lambda calculus with direct sum, the lambda calculus with explicit substitutions, and the call-by-value lambda calculus with permutation rules. (3) We propose an intersection-type system for a calculus corresponding to the classical sequent calculus, which reflects the symmetry of classical logic. We show that the system is complete and can characterize the strong normalization.

Research Products

• [Journal Article] Compositional Z: Confluence proofs for permutative conversion (2016)
  • Author(s): Koji Nakazawa and Ken-etsu Fujita
  • Journal Title: Studia Logica Volume: 104 Issue: 6 Pages: 1205-1224
  • DOI: 10.1007/s11225-016-9673-0
  • NAID: 120005971246
  • Peer Reviewed / Acknowledgement Compliant
• [Presentation] Z for call-by-value (2017)
  • Author(s): Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa
  • Organizer: 6th International Workshop on Cofluence (IWC 2017)
  • Int'l Joint Research
• [Presentation] Church-Rosser theorem and compositional Z-property (2016)
  • Author(s): Ken-etsu Fujita and Koji Nakazawa
  • Organizer: 日本ソフトウェア科学会第33回大会
  • Place of Presentation: 東北大学
  • Year and Date: 2016-09-06
• [Presentation] Intersection and Union Type Assignment and Polarised lambda-bar-mu-mu-tilde (2016)
  • Author(s): Takeshi Tsukada and Koji Nakazawa
  • Organizer: 第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
  • Place of Presentation: 岡山
  • Year and Date: 2016-03-08
• [Presentation] Characterizing trees for lambda-mu terms (2016)
  • Author(s): Koji Nakazawa
  • Organizer: 8th International Workshop on Higher-Order Rewriting (HOR 2016)
  • Place of Presentation: ポルト，ポルトガル
  • Int'l Joint Research
• [Presentation] Compositional Z: Confluence Proofs for Permutative Conversion (2015)
  • Author(s): Koji Nakazawa and Ken-etsu Fujita
  • Organizer: 第32回日本ソフトウェア科学会大会
  • Place of Presentation: 東京
  • Year and Date: 2015-09-10
• [Presentation] Lambda Calculi and Confluence from A to Z (2015)
  • Author(s): Koji Nakazawa
  • Organizer: 4th International Workshop on Confluence (IWC2015)
  • Place of Presentation: Berlin
  • Year and Date: 2015-08-02
  • Int'l Joint Research / Invited