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

Daniel Fischer daniel.is.fischer at web.de
Wed Dec 31 23:15:01 EST 2008

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

```