[Haskell-cafe] bottom case in proof by induction

[raeck at msn.com]

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 at msn.com 
Subject: Re: [Haskell-cafe] bottom case in proof by induction


On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <max.cs.2009 at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090101/51738186/attachment.htm