There's no (valid) formalism that says that [n..]==[n..] is True.<br>The formalism says that [n..] and [n..] are equal. But being equal does not mean that the Haskell (==) function returns True.<br>The (==) function is just an approximation of semantic equality (by necessity).
<br><br> -- Lennart<br><br><div class="gmail_quote">On Dec 28, 2007 3:38 AM, Albert Y. C. Lai <<a href="mailto:email@example.com">firstname.lastname@example.org</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d">Achim Schneider wrote:<br>> [n..] == [m..],<br>><br>> the first thing I notice is<br>><br>> n == m && n+1 == m+1<br>><br>> , which already expresses all of infinity in one instance and can be
<br>> trivially cancelled to<br>><br>> n == m<br>><br>> , which makes the whole darn thing only _|_ if n or m is _|_, which no<br>> member of [n..] can be as long as n isn't or 1 or + has funny ideas.
<br>><br>> I finally begin to understand my love and hate relationship with<br>> formalisms: It involves cuddling with fixed points while protecting<br>> them from evil data and fixed points they don't like as well as
<br>> reduction strategies that don't see their full beauty.<br><br></div>There is a formalism that says [n..]==[n..] is true. (Look for<br>co-induction, observational equivalence, bismulation, ...)<br><br>There is a formalism that says [n..]==[n..] is _|_.
<br><br>We know of implemented programming languages that can give an answer<br>according to the latter formalism.<br><br>If you know of an implemented programming language that can give an<br>answer according to the former formalism, and not just for the obvious
<br>[n..] but also map f xs == map g xs (for example), please spread the news.<br><br>So it comes down to which formalism, not whether formalism.<br><br>I have long known the problem with informalisms. They are full of "I
<br>know", "obviously", and "ought to be". It is too tempting to take your<br>wit for granted. When you make a deduction, you don't easily see whether<br>it is one of a systemtic family of deductions or you are just cunning.
<br>You only see what you can do; you don't see what you can't do, much less<br>what you can't make a computer do.<br><br>Formalisms do not tolerate such self-deception. You think something<br>ought to be obvious? Write them down as axioms. Now with all your
<br>obviousness nailed down black on white, you have a solid ground on which<br>to ask: what can be done, what can't be done, what can be done on a<br>computer, how practical is it? Humility and productivity are thus restored.
<br><div><div></div><div class="Wj3C7c">_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">