Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Church-Rosser Made Easy

Church-Rosser Made Easy

File(s)
ChurchRosser.pdf (291.4 KB)
Main article
Permanent Link(s)
https://hdl.handle.net/1813/14402
Collections
Computing and Information Science Technical Reports
Author
Kozen, Dexter
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.

Sponsorship
National Science Foundation CCF-0635028
Date Issued
2010-02-05T21:27:36Z
Keywords
lambda-calculus
•
Church-Rosser theorem
Type
article

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance