论 Church-Rosser 定理的上界
计算机科学中的逻辑
2017-01-04 v1 计算复杂性
摘要
无类型 lambda 演算中的 Church-Rosser 定理在 beta 等式与 beta 归约方面均已得到充分研究。我们为 beta 等式提供了一个不使用并行归约、而仅利用 Takahashi 翻译（Gross-Knuth 策略）的该定理新证明。基于此，得出了该定理归约序列的上界为 Grzegorczyk 层级的第四层。
引用
@article{arxiv.1701.00637,
title = {On Upper Bounds on the Church-Rosser Theorem},
author = {Ken-etsu Fujita},
journal= {arXiv preprint arXiv:1701.00637},
year = {2017}
}
备注
In Proceedings WPTE 2016, arXiv:1701.00233