[Haskell-cafe] equational reasoning

[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

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