Nope! This is a sloppy terminology that Karl blamed on Barendrecht I think.
Confluence is that if A ->* B and A ->* C then there exists a D such that B ->* D and C ->* D. Church Rosser is the property that if B is convertible to C by an arbitrary series of beta reductions and expansions, then there is a D such that B ->* D and C ->* D. Church Rosser proves all sorts of things, such as the uniqueness of normal forms (when they exist) all by itself.
Obviously, Church Rosser implies confluence (just expand B to A, and then reduce A to C - so B and C are convertible and have a common descendent). In some settings, I'm pretty sure we prove Church Rosser by proving confluence, but this leads to really unfortunate non-proofs in a lot of situations for reasons that are difficult to describe non-graphically.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2009-09-15 02:52 pm (UTC)From:Confluence is that if A ->* B and A ->* C then there exists a D such that B ->* D and C ->* D. Church Rosser is the property that if B is convertible to C by an arbitrary series of beta reductions and expansions, then there is a D such that B ->* D and C ->* D. Church Rosser proves all sorts of things, such as the uniqueness of normal forms (when they exist) all by itself.
Obviously, Church Rosser implies confluence (just expand B to A, and then reduce A to C - so B and C are convertible and have a common descendent). In some settings, I'm pretty sure we prove Church Rosser by proving confluence, but this leads to really unfortunate non-proofs in a lot of situations for reasons that are difficult to describe non-graphically.