[Haskell-cafe] bottom case in proof by induction
Jonathan Cast
jonathanccast at fastmail.fm
Wed Dec 31 23:08:57 EST 2008
On Thu, 2009-01-01 at 03:50 +0000, raeck at msn.com wrote:
> 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 _|_ = _|_ ?
This definition is taken care of for you by the definition of Haskell
pattern matching. If the first equation for a function has a pattern
other than
* a variable or
* a lazy pattern (~p)
for a given argument, then supplying _|_ for that argument /must/ (if
the application is total) return _|_. By rule. (We say the pattern is
strict, in this case).
> and in the case of
>
> > bad () = _|_
> > bad _|_ = ()
Note that these equations (which are not in the right form for the
Haskell equations that define Hasekll functions) aren't satisfied by any
Haskell function!
> mean not every function with a _|_ input will issue a _|_ output,
True --- but we can say a couple of things:
* For all Haskell functions f, if f _|_ is an application of a
constructor C, then f x is an application of C (to some value), for all
x. [1]
* For all Haskell functions f, if f _|_ is a lambda expression, then f
x is a lambda expression, for all x.
The only other possibility for f _|_ is _|_.
(Do you see why bad above is impossible?)
> 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?
You have to deduce what the value at _|_ will be.
> 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?
Appeal to the semantics of Haskell pattern matching. If you like, you
can de-sugar the definition of map a little, to get
map = \ f xn -> case xn of
[] -> []
x:xn0 -> f x : map f xn0
And then you know that
case _|_ of
[] -> ...
...
= _|_
whatever you fill in for the ellipses. (Do you see why this *must* be
part of the language definition?)
> ps, the definition of map does not mention anything about _|_ .
The behavior of map f _|_ is fixed by the definition of Haskell pattern
matching.
jcc
More information about the Haskell-Cafe
mailing list