Re: bottom case in proof by induction
Daniel Fischer <daniel.is.fischer <at> web.de>
2009-01-01 04:15:01 GMT
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 _|_
> 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