On Upper Bounds on the Church-Rosser Theorem
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1701.00637v1 |
| Summary: | 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. |
|---|---|
| ISSN: | 2075-2180 |