* Tillmann Rendel
Roman Cheplyaka schrieb:
Evaluation order matters for operational semantics, not for axiomatic. And even in operational semantics Church–Rosser theorem should prevent getting different results (e.g. 0 and error) for different evaluation orders.
Let's consider
omega = omega const omega 42
I guess you meant "const 42 omega".
which is evaluated to 42 in Haskell, but is nonterminating in an strict language. I would expect every kind of semantics to account for this difference.
It's slightly different. I understand that error ".." and omega have the same denotation, but the difference is that omega does not have normal form and error ".." is in normal form. So non-termination of "const 42 omega" in a strict language is not surprising (we know that strict evaluation does not always find normal form, even if it exists), but "const 42 (error ...) = error ..." means that different evaluation orders give us different normal forms, which is denied by Church-Rosser.
Second, who says Church-Rosser holds for Haskell?
Now I see that exceptions magic can break it. Is this what you mean? -- Roman I. Cheplyaka :: http://ro-che.info/ "Don't let school get in the way of your education." - Mark Twain