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 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. Regarding Church-Rosser. First, it says that if you can reduce term P into both P and Q, then there exists a term R so that both P and Q can be reduced to it. That doesn't mean that your particular evaluation order will ever do this reduction. Instead, it may keep doing other reductions forever. Second, who says Church-Rosser holds for Haskell? Tillmann