On Dec 28, 2007 3:38 AM, Albert Y. C. Lai <
trebla@vex.net> 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.