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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
