On Upper Bounds on the Church-Rosser Theorem

Ken-etsu Fujita
(Gunma University)

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.

In Horatiu Cirstea and Santiago Escobar: Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Porto, Portugal, 23rd June 2016, Electronic Proceedings in Theoretical Computer Science 235, pp. 16–31.
Published: 1st January 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.235.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org