* Tillmann Rendel <ren...@cs.au.dk> [2009-02-19 22:43:24+0100] > 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe