There&#39;s no (valid) formalism that says that [n..]==[n..] is True.<br>The formalism says that [n..] and [n..] are equal.&nbsp; 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>&nbsp; -- Lennart<br><br><div class="gmail_quote">On Dec 28, 2007 3:38 AM, Albert Y. C. Lai &lt;<a href="mailto:trebla@vex.net">trebla@vex.net</a>&gt; 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>&gt; [n..] == [m..],<br>&gt;<br>&gt; the first thing I notice is<br>&gt;<br>&gt; n == m &amp;&amp; n+1 == m+1<br>&gt;<br>&gt; , which already expresses all of infinity in one instance and can be
<br>&gt; trivially cancelled to<br>&gt;<br>&gt; n == m<br>&gt;<br>&gt; , which makes the whole darn thing only _|_ if n or m is _|_, which no<br>&gt; member of [n..] can be as long as n isn&#39;t or 1 or + has funny ideas.
<br>&gt;<br>&gt; I finally begin to understand my love and hate relationship with<br>&gt; formalisms: It involves cuddling with fixed points while protecting<br>&gt; them from evil data and fixed points they don&#39;t like as well as
<br>&gt; reduction strategies that don&#39;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 &quot;I
<br>know&quot;, &quot;obviously&quot;, and &quot;ought to be&quot;. It is too tempting to take your<br>wit for granted. When you make a deduction, you don&#39;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&#39;t see what you can&#39;t do, much less<br>what you can&#39;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&#39;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">
http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br></div></div></blockquote></div><br>