Church-Rosser Made Easy
| dc.contributor.author | Kozen, Dexter | |
| dc.date.accessioned | 2010-02-05T21:27:36Z | |
| dc.date.available | 2010-02-05T21:27:36Z | |
| dc.date.issued | 2010-02-05T21:27:36Z | |
| dc.description.abstract | The Church-Rosser theorem states that the lambda-calculus is confluent under alpha- and beta-reductions. The standard proof of this result is due to Tait and Martin-Loef. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the beta-eta-calculus. | en_US |
| dc.description.sponsorship | National Science Foundation CCF-0635028 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/14402 | |
| dc.language.iso | en_US | en_US |
| dc.subject | lambda-calculus | en_US |
| dc.subject | Church-Rosser theorem | en_US |
| dc.title | Church-Rosser Made Easy | en_US |
| dc.type | article | en_US |
Files
Original bundle
1 - 1 of 1
Loading...
- Name:
- ChurchRosser.pdf
- Size:
- 291.4 KB
- Format:
- Adobe Portable Document Format
- Description:
- Main article