Quantitative analysis of existential theorems of reduction systems

2020 Fiscal Year Final Research Report

• Project/Area Number: 17K05343
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Foundations of mathematics/Applied mathematics
• Research Institution: Gunma University
• Principal Investigator: Fujita Kenetsu 群馬大学, 大学院理工学府, 准教授 (30228994)
• Co-Investigator(Kenkyū-buntansha): 倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Keywords: ラムダ計算 / グルジェゴルチック階層 / チャーチ・ロッサーの定理 / 箙 / 並行簡約 / 隣接行列 / 計算の複雑さ / 簡約列

Outline of Final Research Achievements

We performed a quantitative analysis of witnesses of the existential theorems such as Church--Rosser theorem and normalization theorem in reduction systems. Ketema--Simonsen posed an open problem about upper bounds on the size of Church--Rosser theorem in lambda-calculus (ACM Trans. on Computational Logic, 2013). On the contrary to their conjecture that upper bound functions should be in the 5th level of the Grzegorczyk hierarchy, we have proved that the upper bound function belongs to the 4th level of the hierarchy. This quantitative proof method is extended to typed systems such as Godel's system T, Girard's system F, and Pure Type Systems as well. We also invented a new proof method for confluence in the style of divide-and-conquer, by extending the so-called Z theorem.
Moreover, we established a neighbourhood and lattice model based on the duality between Kripke and algebraic models, and proved its completeness w.r.t. 2nd-order intuitionistic propositional logic.

Free Research Field

情報基礎理論

Academic Significance and Societal Importance of the Research Achievements

チャーチ・ロッサーの定理は，等式と計算についての基本定理であり，この複雑さについての未解決予想を計算理論の観点から解明した．さらに，計算の道筋を図的に表現する枠組の研究を行い，行列計算を応用して計算の道を数える方法についても研究した．これらの成果は論文としても出版しており，またWebページからも分かり易く情報発信を行なっている．
http://www.cs.gunma-u.ac.jp/~fujita/