On Upper Bounds on the Church-Rosser Theorem

Autor:	Fujita, Ken-etsu
Rok vydání:	2017
Předmět:	Computer Science - Logic in Computer Science Computer Science - Computational Complexity
Zdroj:	EPTCS 235, 2017, pp. 16-31
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.235.2
Popis:	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. Comment: In Proceedings WPTE 2016, arXiv:1701.00233
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1701.00637 Zobrazit plný text záznamu View this record from Arxiv