Confluence and Church-Rosser

Okay, I'm back to post about confluence and the Church-Rosser property, as I threatened yesterday. This is a complaint about something I found very annoying when I was in graduate school; it's related to yesterday's complaint about type-1 and type-2 errors in statistics, but slightly different in that it's not about names for two things that don't help you know which names which, but rather about two names that one is supposed to keep straight even though they both name the same thing.

In lambda-calculi, and other rewriting systems with which I am less familiar, one defines a reduction relation on terms that is supposed to capture the idea of a single step of computation or simplification, like replacing "2+3" with "5". (These are expressions of arithmetic, not lambda-calculus, but never mind. I'll use arithmetic expressions again below.) Reduction relations are almost never reflexive (that would be zero steps of computation), transitive (more than one step) or symmetric (counting a backward step as a forward step), but it does make sense to look at the notion of "equivalence" that comes from thinking of things as equivalent if one can be reduced to the other. The equivalence relation induced by reduction, called conversion or convertibility, is the reflexive, symmetric, transitive closure of reduction -- which is to say that two terms are convertible if one can be transformed into the other by a sequence of zero or more steps each of which is a reduction either forwards or backwards. So, if "2+3" reduces to "5" and "9-4" also reduces to "5", the expressions "2+3" and "9-4" are convertible and we can think of them as having the same meaning.

In general, if A reduces in zero or more steps to B, and C also reduces in zero or more steps to B, then we can say that B is a "common reduct" of A and C. Clearly, any two terms with a common reduct are by definition convertible. The question is, do any two convertible terms have a common reduct?

[Why is this question important? Among other reasons, because if so, and you have two terms that you can show do not have a common reduct, you will know they are not convertible. Otherwise, it would be hard to be sure.]

In the lambda-calculus, the answer is yes. This fact was proven by Church and Rosser in 1936 and is called the Church-Rosser Theorem. For rewrite systems other than the untyped lambda-calculus, the answer obviously depends on what the reduction relation actually is. A reduction relation for which any two convertible terms have a common reduct can be said to have the Church-Rosser property.

OK. It turns out that the key to proving the Church-Rosser property, at least for the lambda calculus, is to prove the following: If there is more than one way to reduce a term A, say to B1 or to B2, in zero or more steps, then there exists some term C such that both B1 and B2 can be reduced in zero or more steps to C. More generally, we can say: any two terms with a common "source" also have a common reduct. So if two different people are trying to reduce A and their paths ever diverge, taking one to B1 and the other to B2, then it doesn't really matter because they will eventually "flow back together" at C. This property is called confluence.

So here's where I have a problem. It turns out that the property I refer to as CR above (convertible terms have a common reduct) and the property I just called confluence (terms with a common source have a common reduct) are equivalent. (The CR->confluence direction is obvious, as any terms with a common source are convertible; the proof of other direction left as an exercise. Hint: induction on the number of steps in the conversion.) Because they're equivalent, it's always hard to know whether I have the names the right way around. I was pretty sure this is the way I learned them in grad school, and it's consistent with MathWorld's definitions of confluence and Church-Rosser, but Wikipedia has it differently, as does at least one legitimate book I looked in while writing this.

What's my point? The point is that I resent having had to devote precious brain cells to remembering which is which of two different ways to say the same goddamn thing. It seems like a pretty small thing and not worth bothering to resent, but there it is.