A Simplified Proof of the Church–Rosser Theorem

, &
Studia Logica 102 (1):175-183 (2014)
  Copy   BIBTEX

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

Categories

Keywords

Reprint years

DOI

10.1007/s11225-013-9470-y

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,894

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Church-Rosser property and intersection types.George Koletsos & George Stavrinos - 2008 - Australasian Journal of Logic 6:37-54.
An Abstract form of the church-rosser theorem. I.R. Hindley - 1969 - Journal of Symbolic Logic 34 (4):545-560.
A New Proof of the Church-Rosser Theorem.H. B. Curry - 1956 - Journal of Symbolic Logic 21 (4):377-378.
Remarks on the church-Rosser property.E. G. K. López-Escobar - 1990 - Journal of Symbolic Logic 55 (1):106-112.
Analytic proof systems for λ-calculus: the elimination of transitivity, and why it matters. [REVIEW]Pierluigi Minari - 2007 - Archive for Mathematical Logic 46 (5):385-424.
The Church Rosser theorem for strong reduction in combinatory logic.Kenneth Loewen - 1968 - Notre Dame Journal of Formal Logic 9 (4):299-302.
The Church-Rosser Property in Symmetric Combinatory Logic.Katalin Bimbó - 2005 - Journal of Symbolic Logic 70 (2):536 - 556.
Ward-takahashi identities and Noether’s theorem in quantum field theory.Michael Danos - 1997 - Foundations of Physics 27 (7):995-1009.
The Church-Rosser theorem for the typed $\lambda$-calculus with surjective pairing.Garrel Pottinger - 1981 - Notre Dame Journal of Formal Logic 22 (3):264-268.
On constructivity and the Rosser property: a closer look at some Gödelean proofs.Saeed Salehi & Payam Seraji - 2018 - Annals of Pure and Applied Logic 169 (10):971-980.

Analytics

Added to PP
2013-03-10

Downloads
56 (#428,852)

6 months
4 (#1,022,257)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references