Authors: | Ghilezan, Silvia Kunčak, Viktor |
Title: | Confluence of untyped lambda calculus via simple types | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Volume: | 2202 | First page: | 38 | Last page: | 49 | Conference: | 7th Italian Conference on Theoretical Computer Science, ICTCS 2001; Torino; Italy; 4 October 2001 through 6 October 2001 | Issue Date: | 1-Jan-2001 | Rank: | M21 | ISBN: | 978-3-540-45446-5 | ISSN: | 0302-9743 | DOI: | 10.1007/3-540-45446-2_3 | Abstract: | We present a new proof of confluence of the untyped lambda calculus by reducing the confluence of β-reduction in the untyped lambda calculus to the confluence of β-reduction in the simply typed lambda calculus. This is achieved by embedding typed lambda terms into simply typed lambda terms. Using this embedding, an auxiliary reduction, and β-reduction on simply typed lambda terms we define a new reduction on all lambda terms. The transitive closure of the reduction defined is β-reduction on all lambda terms. This embedding allows us to use the confluence of β-reduction on simply typed lambda terms and thus prove the confluence of the reduction defined. As a consequence we obtain the confluence of β-reduction in the untyped lambda calculus. |
Publisher: | Springer Link |
Show full item record
SCOPUSTM
Citations
1
checked on Sep 8, 2024
Page view(s)
2
checked on Sep 7, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.