<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META http-equiv=Content-Type content=text/html;charset=iso-8859-1>
<META content="MSHTML 6.00.6001.18183" name=GENERATOR></HEAD>
<BODY id=MailContainerBody 
style="PADDING-RIGHT: 10px; PADDING-LEFT: 10px; PADDING-TOP: 15px" leftMargin=0 
topMargin=0 CanvasTabStop="true" name="Compose message area">
<DIV>I am afraid I am still confused.</DIV>
<DIV><FONT face=Calibri></FONT>&nbsp;</DIV>
<DIV><FONT face=Calibri>&gt; <FONT face="Times New Roman">foo [] = ...<BR>&gt; 
foo (x:xs) = ...<BR>&gt; There is an implied:<BR>&gt; foo _|_ = _|_<BR>&gt; The 
right side cannot be anything but _|_.&nbsp; If it could, then that would imply 
we could solve the halting problem:</FONT></FONT></DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman"></FONT></FONT>&nbsp;</DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman">in a proof, how I could say 
the right side must be _|_ without defining foo _|_ = _|_ ? and in the case 
of</FONT></FONT></DIV>
<DIV><FONT face=Calibri><FONT face=Calibri></FONT></FONT>&nbsp;</DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman">&gt; bad () = 
_|_&nbsp;&nbsp;&nbsp;</FONT></FONT></DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman">&gt; bad _|_ = 
()</FONT></DIV>
<DIV><BR></DIV></FONT>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>mean not every function 
with a _|_ input will issue a _|_ output, so we have to say what result will be 
issued by a _|_ input&nbsp;in the definitions of&nbsp;the functions if we want 
to prove the equvalence between them?</FONT></DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3></FONT>&nbsp;</DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>However, in the case 
of&nbsp;&nbsp; </FONT><FONT face=Calibri size=3>map f _|_&nbsp; , I do believe 
the result will be _|_ since it can not be anything else, but how I could prove 
this? any clue? </FONT></DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3></FONT>&nbsp;</DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>ps, the definition of 
map </FONT><FONT face=Calibri size=3>does not mention anything about _|_ 
.</FONT></DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3></FONT>&nbsp;</DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>Thanks</FONT></DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>Raeck</FONT></DIV>
<DIV style="FONT: 10pt Tahoma">
<DIV><FONT face=Calibri size=3></FONT><BR></DIV>
<DIV style="BACKGROUND: #f5f5f5">
<DIV style="font-color: black"><B>From:</B> <A 
title="mailto:lrpalmer@gmail.com&#10;CTRL + Click to follow link" 
href="mailto:lrpalmer@gmail.com">Luke Palmer</A> </DIV>
<DIV><B>Sent:</B> Wednesday, December 31, 2008 10:43 PM</DIV>
<DIV><B>To:</B> <A title=max.cs.2009@googlemail.com 
href="mailto:max.cs.2009@googlemail.com">Max.cs</A> ; <A 
title="mailto:raeck@msn.com&#10;CTRL + Click to follow link" 
href="mailto:raeck@msn.com">raeck@msn.com</A> </DIV>
<DIV><B>Subject:</B> Re: [Haskell-cafe] bottom case in proof by 
induction</DIV></DIV></DIV>
<DIV><BR></DIV>On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <SPAN dir=ltr>&lt;<A 
title="mailto:max.cs.2009@googlemail.com&#10;CTRL + Click to follow link" 
href="mailto:max.cs.2009@googlemail.com">max.cs.2009@googlemail.com</A>&gt;</SPAN> 
wrote:<BR>
<DIV class=gmail_quote>
<BLOCKQUOTE class=gmail_quote 
style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
  <DIV style="PADDING-RIGHT: 10px; PADDING-LEFT: 10px; PADDING-TOP: 15px" 
  name="Compose message area">
  <DIV><FONT face=Calibri>thanks Luke,</FONT></DIV>
  <DIV><FONT face=Calibri></FONT>&nbsp;</DIV>
  <DIV><FONT face=Calibri>so you mean the&nbsp;</FONT><FONT 
  face="Times New Roman"> _|_&nbsp; is necessary only when I have defined the 
  pattern&nbsp; _|_&nbsp; such as</FONT></DIV>
  <DIV>&nbsp;</DIV>
  <DIV><FONT face=Calibri>foo [] = []</FONT></DIV>
  <DIV class=Ih2E3d>
  <DIV><FONT face=Calibri>foo&nbsp;</FONT><FONT face="Times New Roman"> 
  _|_&nbsp; =&nbsp; _|_ </FONT></DIV>
  <DIV>foo (x:xs) = x(&nbsp;foo xs&nbsp;)</DIV></DIV>
  <DIV>-- consider non-termination case</DIV></DIV></BLOCKQUOTE>
<DIV><BR>That is illegal Haskell.&nbsp; But another way of putting that is that 
whenever you do any pattern matching, eg.:<BR><BR>foo [] = ...<BR>foo (x:xs) = 
...<BR><BR>There is an implied:<BR><BR>foo _|_ = _|_<BR><BR>The right side 
cannot be anything but _|_.&nbsp; If it could, then that would imply we could 
solve the halting problem:<BR><BR>halts () = True<BR>halts _|_ = 
False<BR><BR>Because _|_ is the denotation of a program which never 
halts.<BR><BR>To do it a bit more domain-theoretically, I'll first cite the 
result that <I>every function has a fixed point.</I>&nbsp; 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).&nbsp; Then let's 
consider this bad function:<BR><BR>bad () = _|_&nbsp;&nbsp;&nbsp; -- you can't 
write _|_ in Haskell, but "undefined" or "let x = x in x" mean the same 
thing<BR>bad _|_ = () <BR><BR>Then what is fix f?&nbsp; Well, it either 
terminates or it doesn't, right?&nbsp; I.e. fix f = () or fix f = 
_|_.<BR><BR>Taking into account that fix f = f (fix f):<BR>If it does:&nbsp; fix 
f = () = f () = _|_, a contradiction.<BR>If it doesn't: fix f = _|_ = f _|_ = 
(), another contradiction.<BR><BR>From a mathematical perspective, that's why 
you can't pattern match on _|_.<BR><BR>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...<BR><BR>Luke<BR></DIV></DIV></BODY></HTML>