Abstract
Takahashi translation * is a translation which means reducing all of the redexes in a λ-term simultaneously. In [4] and [5], 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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics, 2nd edition, North Holland, Amsterdam, 1984.
Hindley, J. R. and J. P. Seldin, Lambda-calculus and Combinators, An Introduction, Cambridge University Press, Cambridge, 2008.
Komori, Y. and F. Yamakawa, ‘The system of CLλ and a method to calculate β forms without β-reductions’, to appear.
Takahashi M.: Parallel reductions in λ-calculus. Journal of Symbolic Computation 7, 113–123 (1989)
Takahashi M.: Parallel reductions in λ-calculus. Information and Computation 118, 120–127 (1995)
Takahashi, M., Theory of Computation, Computability and Lambda Calculus, Kindai Kagaku Sha, Tokyo, 1991 (in Japanese).
Author information
Authors and Affiliations
Corresponding author
Additional information
Dedicated to the memory of the late Professor Kazuo Matsumoto
Rights and permissions
About this article
Cite this article
Komori, Y., Matsuda, N. & Yamakawa, F. A Simplified Proof of the Church–Rosser Theorem. Stud Logica 102, 175–183 (2014). https://doi.org/10.1007/s11225-013-9470-y
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-013-9470-y