Explaining the Church-Rosser Theorem in basic terms

I would like to know how the Church-Rosser theorem is used within programming, specifically functional programming. I've looked up information but can only find sources referring to lambda calculus (limited knowledge) and beta-reductions.

If anyone could explain where lambda calculus comes into this and what reductions are, I think that would clear things up.

My initial thoughts of the Church-Rosser theorem is that it's to do with order of evalutation and execution of functions but I'm not entirely sure whether this is accurate information.

Thanks.

Note: I'm currently studying Standard ML

Solution

Your initial thoughts are fine.

The lambda calculus is the formal foundation on which functional programming is built.
The lambda calculus is a term rewriting system, and a reduction means following a rewrite rule.
The lambda calculus does not dictate a specific order of evaluation, so given a lambda expression where multiple reductions are possible, the Church-Rosser theorem says that you can pick either one. This gives functional programming language designers quite a lot of freedom to design their evaluation semantics. For example, in f (g x), assuming both are pure functions, whether you reduce f or g first are equivalent.

Wikipedia's description of the Church-Rosser theorem is:

[I]f there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions.

The example f (g x) where f is x² and g is 2x:
```
(λx.x*x) ((λy.y+y) 2)  ~β~>  ((λy.y+y) 2)*((λy.y+y) 2)
                       ~β~>  (2+2)*((λy.y+y) 2)
                       ~β~>  (2+2)*(2+2)

(λx.x*x) ((λy.y+y) 2)  ~β~>  (λx.x*x) (2+2)
                       ~β~>  (2+2)*(2+2)
```
In this example, the two distinct reductions are β-reduction on either of the lambdas, and one term among others that is reachable from both reductions is (2+2)*(2+2).