There's no (valid) formalism that says that [n..]==[n..] is True. The formalism says that [n..] and [n..] are equal. But being equal does not mean that the Haskell (==) function returns True. The (==) function is just an approximation of semantic equality (by necessity).
-- Lennart On Dec 28, 2007 3:38 AM, Albert Y. C. Lai <[EMAIL PROTECTED]> 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, ...) > > There is a formalism that says [n..]==[n..] is _|_. > > We know of implemented programming languages that can give an answer > according to the latter formalism. > > If you know of an implemented programming language that can give an > answer according to the former formalism, and not just for the obvious > [n..] but also map f xs == map g xs (for example), please spread the news. > > So it comes down to which formalism, not whether formalism. > > I have long known the problem with informalisms. They are full of "I > know", "obviously", and "ought to be". It is too tempting to take your > wit for granted. When you make a deduction, you don't easily see whether > it is one of a systemtic family of deductions or you are just cunning. > You only see what you can do; you don't see what you can't do, much less > what you can't make a computer do. > > Formalisms do not tolerate such self-deception. You think something > ought to be obvious? Write them down as axioms. Now with all your > obviousness nailed down black on white, you have a solid ground on which > to ask: what can be done, what can't be done, what can be done on a > computer, how practical is it? Humility and productivity are thus > restored. > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
