bottom case in proof by induction

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

bottom case in proof by induction

raeck@msn.com
Dear all,

Happy New Year!

I am learning the Induction Proof over Haskell, I saw some proofs for the equivalence of two functions will have a case called 'bottom' but some of them do no have.  What kind of situation we should also include the bottom case to the proof? How about the functions do not have the 'bottom' input such as:

foo [] = []
foo (x:xs) = x : (foo xs)

thank you,

Raeck
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20081231/8c98ba3c/attachment.htm
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] bottom case in proof by induction

Luke Palmer-2
2008/12/31 <[hidden email]>

>  Dear all,
>
> Happy New Year!
>
> I am learning the Induction Proof over Haskell, I saw some proofs for the
> equivalence of two functions will have a case called 'bottom' but some of
> them do no have.  What kind of situation we should also include the bottom
> case to the proof? How about the functions do not have the 'bottom' input
> such as:
>
> foo [] = []
> foo (x:xs) = x : (foo xs)
>

Okay, I'm not sure what you mean by bottom.  You could either mean the base
case, or you could mean bottom -- non-terminating inputs -- as in domain
theory.

Let's say you wanted to see if foo is equivalent to id.

id x = x

We can do it without considering nontermination, by induction on the
structure of the argument:

  First, the *base case*: empty lists.
    foo [] = []
    id [] = []
  Just by looking at the definitions of each.

 Now the inductive case.  Assume that foo xs = id xs, and show that foo
(x:xs) = id (x:xs), for all x (but a fixed xs).

 foo (x:xs) = x : foo xs
  foo xs = id xs  by our  the induction hypothesis, so
  foo (x:xs) = x : id xs = x : xs
 And then just by the definition of id:
  id (x:xs) = x : xs

And we're done.

Now, maybe you meant bottom as in nontermination.  In this case, we have to
prove that they do the same thing when given _|_ also.  This requires a
deeper understanding of the semantics of the language, but can be done
here.

First, by simple definition, id _|_ = _|_.  Now let's consider foo _|_.  The
Haskell semantics say that pattern matching on _|_ yields _|_, so foo _|_ =
_|_. So they are equivalent on _|_ also.  Thus foo and id are exactly the
same function.

See http://en.wikibooks.org/wiki/Haskell/Denotational_semantics for more
about _|_.

Happy mathhacking,
Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20081231/71a112a0/attachment.htm
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] bottom case in proof by induction

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

> bad () = _|_  
> bad _|_ = ()


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?

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 _|_ .

Thanks
Raeck


From: Luke Palmer
Sent: Wednesday, December 31, 2008 10:43 PM
To: Max.cs ; [hidden email]
Subject: Re: [Haskell-cafe] bottom case in proof by induction


On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <[hidden email]> wrote:

  thanks Luke,

  so you mean the  _|_  is necessary only when I have defined the pattern  _|_  such as

  foo [] = []
  foo  _|_  =  _|_
  foo (x:xs) = x( foo xs )
  -- consider non-termination case

That is illegal Haskell.  But another way of putting that is that whenever you do any pattern matching, eg.:

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:

halts () = True
halts _|_ = False

Because _|_ is the denotation of a program which never halts.

To do it a bit more domain-theoretically, I'll first cite the result that every function has a fixed point.  That is, for every f, there is a function fix f, where fix f = f (fix f). (The fix function is actually available in Haskell from the module Data.Function).  Then let's consider this bad function:

bad () = _|_    -- you can't write _|_ in Haskell, but "undefined" or "let x = x in x" mean the same thing
bad _|_ = ()

Then what is fix f?  Well, it either terminates or it doesn't, right?  I.e. fix f = () or fix f = _|_.

Taking into account that fix f = f (fix f):
If it does:  fix f = () = f () = _|_, a contradiction.
If it doesn't: fix f = _|_ = f _|_ = (), another contradiction.

>From a mathematical perspective, that's why you can't pattern match on _|_.

>From an operational perspective, it's just that _|_ means "never terminates", and we can't determine that, because we would try to run it "until it doesn't terminate", which is meaningless...

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20090101/51738186/attachment.htm
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] bottom case in proof by induction

Daniel Fischer-4
Am Donnerstag, 1. Januar 2009 04:50 schrieb [hidden email]:

> 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
>

Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] bottom case in proof by induction

Martijn van Steenbergen-2
In reply to this post by Luke Palmer-2
Luke Palmer wrote:
> First, by simple definition, id _|_ = _|_.  Now let's consider foo _|_.  
> The Haskell semantics say that pattern matching on _|_ yields _|_, so
> foo _|_ = _|_. So they are equivalent on _|_ also.  Thus foo and id are
> exactly the same function.

Would it in general also be interesting to look at foo == id for input
(_|_:xs) and all other possible positions and combinations of positions
for bottom? I wonder how many cases you need to take into consideration
to have covered every possible situation.

Martijn.
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] bottom case in proof by induction

Bugzilla from jonathanccast@fastmail.fm
In reply to this post by raeck@msn.com
On Thu, 2009-01-01 at 03:50 +0000, [hidden email] 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