[Haskell-cafe] bottom case in proof by induction

[Luke Palmer]

2008/12/31 <raeck at 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)
>

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/haskell-cafe/attachments/20081231/71a112a0/attachment.htm