[Haskell-cafe] bottom case in proof by induction

[Daniel Fischer]

Am Donnerstag, 1. Januar 2009 04:50 schrieb 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

Because _|_ is matched against a refutable pattern ([], in this case), so when 
foo is called with argument _|_, the runtime tries to match it against []. 
For that, it must reduce it far enough to know its top level constructor, 
which by definition of _|_ isn't possible, so the pattern match won't 
terminate, hence foo _|_ is a nonterminating computation, i.e. _|_.

>
> > bad () = _|_
> > bad _|_ = ()

You can't do that. You can only pattern-match against patterns, which _|_ 
isn't. 

>
> 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?

If you match against an irrefutable pattern (variable, wildcard or ~pattern), 
the matching succeeds without evaluating the argument, so then you can have 
functions which return a terminating value for nonterminating arguments:

lazyMap ~(x:xs) = [[],[x],xs]

*LazyTest> lazyMap undefined
[[],[*** Exception: Prelude.undefined
*LazyTest> lazyMap []
[[],[*** Exception: PrintPer.hs:28:0-28: Irrefutable pattern failed for 
pattern (x : xs)
*LazyTest> take 1 $ lazyMap undefined
[[]]




>
> 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 _|_ .

As above, evaluation of map f _|_ tries to match _|_ against [], which doesn't 
terminate.

>
> Thanks
> Raeck
>