2008/12/31 <span dir="ltr"><<a href="mailto:raeck@msn.com">raeck@msn.com</a>></span><br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div style="padding-right: 10px; padding-left: 10px; padding-top: 15px;" name="Compose message area">
<div><font face="Calibri">Dear all,</font></div>
<div><font face="Calibri"></font> </div>
<div><font face="Calibri">Happy New Year!</font></div>
<div><font face="Calibri"></font> </div>
<div><font face="Calibri">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:</font></div>
<div><font face="Calibri"></font> </div>
<div><font face="Calibri">foo [] = []</font></div>
<div><font face="Calibri">foo (x:xs) = x : (foo xs)</font></div></div></blockquote><div><br>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.<br>
<br>Let's say you wanted to see if foo is equivalent to id. <br><br>id x = x<br><br>We can do it without considering nontermination, by induction on the structure of the argument:<br><br> First, the <i>base case</i>: empty lists.<br>
foo [] = []<br> id [] = []<br> Just by looking at the definitions of each.<br><br> 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).<br><br> foo (x:xs) = x : foo xs<br>
foo xs = id xs by our the induction hypothesis, so <br> foo (x:xs) = x : id xs = x : xs<br> And then just by the definition of id:<br> id (x:xs) = x : xs<br><br>And we're done.<br><br>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. <br>
<br>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.<br>
<br>See <a href="http://en.wikibooks.org/wiki/Haskell/Denotational_semantics">http://en.wikibooks.org/wiki/Haskell/Denotational_semantics</a> for more about _|_.<br><br>Happy mathhacking,<br>Luke<br></div></div>