On 27 Dec 2007, at 8:38 PM, Albert Y. C. Lai wrote:
Achim Schneider wrote:
[n..] == [m..], the first thing I notice is n == m && n+1 == m+1 , which already expresses all of infinity in one instance and can be trivially cancelled to n == m , which makes the whole darn thing only _|_ if n or m is _|_, which no member of [n..] can be as long as n isn't or 1 or + has funny ideas. I finally begin to understand my love and hate relationship with formalisms: It involves cuddling with fixed points while protecting them from evil data and fixed points they don't like as well as reduction strategies that don't see their full beauty.
There is a formalism that says [n..]==[n..] is true. (Look for co- induction, observational equivalence, bismulation, ...)
But, of course, any formalism that says [n..]==[n..] = True interprets (==) as either not a monotone or not a continuous function. Saying that [n..] = [n..] for some equivalence relation doesn't say anything about the value of the Haskell expression [n..] == [n..]. jcc