A simplified proof of the Church-Rosser theorem. (English) Zbl 1338.03017

Summary: Takahashi translation \(\ast\) is a translation which means reducing all of the redexes in a \(\lambda\)-term simultaneously. In [J. Symb. Comput. 7, No. 2, 113–123 (1989; Zbl 0661.03008); Inf. Comput. 118, No. 1, 120–127 (1995; Zbl 0827.68060)], M. Takahashi gave a simple proof of the Church-Rosser confluence theorem by using the notion of parallel reduction and Takahashi translation. Our aim of this paper is to give a simpler proof of Church-Rosser theorem using only the notion of Takahashi translation.


03B40 Combinatory logic and lambda calculus
Full Text: DOI


[1] Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics, 2nd edition, North Holland, Amsterdam, 1984. · Zbl 0551.03007
[2] Hindley, J. R. and J. P. Seldin, Lambda-calculus and Combinators, An Introduction, Cambridge University Press, Cambridge, 2008. · Zbl 1149.03016
[3] Komori, Y. and F. Yamakawa, ‘The system of CLλ and a method to calculate \(β\) forms without \(β\)-reductions’, to appear. · Zbl 0827.68060
[4] Takahashi, M., Parallel reductions in λ-calculus, Journal of Symbolic Computation, 7, 113-123, (1989) · Zbl 0661.03008
[5] Takahashi, M., Parallel reductions in λ-calculus, Information and Computation, 118, 120-127, (1995) · Zbl 0827.68060
[6] Takahashi, M., Theory of Computation, Computability and Lambda Calculus, Kindai Kagaku Sha, Tokyo, 1991 (in Japanese). · Zbl 0827.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.