Re: [Haskell-cafe] bottom case in proof by induction

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 From: Luke Palmer Sent: Wednesday, December 31, 2008 10:43 PM To: Max.cs ; raeck@msn.com Subject: Re: [Haskell-cafe] bottom case in proof by induction On Wed, Dec 31, 2008 at 3:28 PM, Max.cs 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