# bottom case in proof by induction

6 messages
Open this post in threaded view
|

## bottom case in proof by induction

 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
Open this post in threaded view
|

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

 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
Open this post in threaded view
|

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

Open this post in threaded view
|

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

 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 >