On Upper Bounds on the Church-Rosser Theorem
Logic in Computer Science
2017-01-04 v1 Computational Complexity
Abstract
The Church-Rosser theorem in the type-free lambda-calculus is well investigated both for beta-equality and beta-reduction. We provide a new proof of the theorem for beta-equality with no use of parallel reductions, but simply with Takahashi's translation (Gross-Knuth strategy). Based on this, upper bounds for reduction sequences on the theorem are obtained as the fourth level of the Grzegorczyk hierarchy.
Keywords
Cite
@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}
}
Comments
In Proceedings WPTE 2016, arXiv:1701.00233