Why is Church-Rosser so important for basing programming languages on lamdba-calculus?

Question

So, I know Church-Rosser has 2 thesis:

CR1: If $ E_1 \leftrightarrow E_2 $, then there exists an Expression E so $ E_1 \rightarrow E $ and $ E_2 \rightarrow E $

CR2: If $ E \rightarrow N $ (with N in normalform), then there exists a reduction row in normalorder (first reduce the left most ouuter most index) from E to N

from CR1 we learn that no expression can be converted to 2 different normalforms, so there is only one result for each function

from CR2 we learn that reduction in normalorder always finds the result (if their is one (no loop))

But i don't understand why these two are so important for basing a programming language on lambda-calculus. So my question is why are they?

Answer 1

Think of it as a sanity check. CR cones from the days when we were just figuring out what programming languages were. The Lambda calculus was new, and its basic properties were unknown.

CR says that Lambda Calculus behaves like you would expect: every expression can be evaluated to a unique value, or runs forever. We didn't know if the calculus was well behaved. We had to prove it.

Imagine that CR didn't hold, and that the order you evaluated an expression mattered. We would throw Lambda calculus away. It would be like saying $2+2$ could have more than one value.

CR also justifies the existence of lazy languages, showing that they behave at least as well as eager languages, sometimes better. Haskell certainly owes its existence in part to CR.