[Haskell-cafe] bottom case in proof by induction
Derek Elkins
derek.a.elkins at gmail.com
Wed Dec 31 23:16:38 EST 2008
On Wed, 2008-12-31 at 22:08 -0600, Jonathan Cast wrote:
> 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!
This isn't just a quirk of Haskell semantics. bad is not computable.
Period.
More information about the Haskell-Cafe
mailing list