Verification of Properties of Classical Calculi

2023 Fiscal Year Final Research Report

• Project/Area Number: 17K00005
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Chiba University
• Principal Investigator: SAKURAI Takafumi 千葉大学, 大学院理学研究院, 教授 (60183373)
• Co-Investigator(Kenkyū-buntansha): 菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
• Project Period (FY): 2017-04-01 – 2024-03-31
• Keywords: ラムダ計算 / α同値 / 古典論理 / 証明検証系 / minlog

Outline of Final Research Achievements

The purpose of this research is to study various properties of computational systems based on classical logic. But, in the process of first proving the properties of traditional lambda calculus, which is the foundation of this, using the verification system minlog, we realized that there is a new proof of the well-known theorem that α-reduction becomes an equivalence relation. The symmetry law is the most difficult to prove when proving that an equivalence relation exists, but by closely analyzing the renaming required when performing α-reduction, we can accurately determine the order in which variable collision avoidance occurs. Then, we can decompose the variable renaming required for collision avoidance into simpler ones, and by tracing them in reverse, we can construct an α-reduction that reverses the α-reduction of interest.

Free Research Field

計算の論理と意味、プログラム意味論

Academic Significance and Societal Importance of the Research Achievements

伝統的ラムダ計算は20世紀初頭から研究されており、現代の多くの計算系の土台になるものである。伝統的ラムダ計算においてα簡約が同値関係になるという基本的な定理は古くからよく知られており様々な方法で証明されているが、それにも関わらずまだ新しい証明があることは驚きであった。α簡約では変数の衝突を防ぐために変数の名前替えを行うが、それは代入の特別な場合とみなすことができ、代入の過程を詳しく把握することにより変数の名前替えを単純なものに分解し、それを利用してα簡約の性質を考えるというアプローチは今までに見られなかったアイディアであり、変数の名前替えについて新しい知見を得ることができた。