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