I am afraid I am still confused.
> foo [] = ...
>
foo (x:xs) = ...
> There is an implied:
> foo _|_ = _|_
> The
right side cannot be anything but _|_. If it could, then that would imply
we could solve the halting problem:
in a proof, how I could say
the right side must be _|_ without defining foo _|_ = _|_ ? and in the case
of
> bad () =
_|_
> bad _|_ =
()
mean not every function
with a _|_ input will issue a _|_ output, so we have to say what result will be
issued by a _|_ input in the definitions of the functions if we want
to prove the equvalence between them?
However, in the case
of map f _|_ , I do believe
the result will be _|_ since it can not be anything else, but how I could prove
this? any clue?
ps, the definition of
map does not mention anything about _|_
.
Thanks
Raeck
Sent: Wednesday, December 31, 2008 10:43 PM
Subject: Re: [Haskell-cafe] bottom case in proof by
induction
On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <max.cs.2009@googlemail.com>
wrote:
thanks Luke,
so you mean the _|_ is necessary only when I have defined the
pattern _|_ such as
foo [] = []
foo
_|_ = _|_
foo (x:xs) = x( foo xs )
-- consider non-termination case
That is illegal Haskell. But another way of putting that is that
whenever you do any pattern matching, eg.:
foo [] = ...
foo (x:xs) =
...
There is an implied:
foo _|_ = _|_
The right side
cannot be anything but _|_. If it could, then that would imply we could
solve the halting problem:
halts () = True
halts _|_ =
False
Because _|_ is the denotation of a program which never
halts.
To do it a bit more domain-theoretically, I'll first cite the
result that every function has a fixed point. That is, for every f,
there is a function fix f, where fix f = f (fix f). (The fix function is
actually available in Haskell from the module Data.Function). Then let's
consider this bad function:
bad () = _|_ -- you can't
write _|_ in Haskell, but "undefined" or "let x = x in x" mean the same
thing
bad _|_ = ()
Then what is fix f? Well, it either
terminates or it doesn't, right? I.e. fix f = () or fix f =
_|_.
Taking into account that fix f = f (fix f):
If it does: fix
f = () = f () = _|_, a contradiction.
If it doesn't: fix f = _|_ = f _|_ =
(), another contradiction.
From a mathematical perspective, that's why
you can't pattern match on _|_.
From an operational perspective, it's
just that _|_ means "never terminates", and we can't determine that, because we
would try to run it "until it doesn't terminate", which is
meaningless...
Luke