Jonathan Cast | 1 Jan 05:08 2009

Re: bottom case in proof by induction

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
(Continue reading)

Derek Elkins | 1 Jan 05:16 2009
Picon

Re: bottom case in proof by induction

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 _|_ = ()
> 
(Continue reading)


Gmane