Quantitative analysis of existential theorems of reduction systems
| 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
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
チャーチ・ロッサーの定理は，等式と計算についての基本定理であり，この複雑さについての未解決予想を計算理論の観点から解明した．さらに，計算の道筋を図的に表現する枠組の研究を行い，行列計算を応用して計算の道を数える方法についても研究した．これらの成果は論文としても出版しており，またWebページからも分かり易く情報発信を行なっている．
http://www.cs.gunma-u.ac.jp/~fujita/
|
Report
(5 results)
Research Products
(42 results)
