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... Show more

January 3, 2017

Loading full text...

Similar articles

Loading recommendations...

x1

On Upper Bounds on the Church-Rosser Theorem

Click on play to start listening