<!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> </DIV>
<DIV><FONT face=Calibri>> <FONT face="Times New Roman">foo [] = ...<BR>>
foo (x:xs) = ...<BR>> There is an implied:<BR>> foo _|_ = _|_<BR>> The
right side cannot be anything but _|_. 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> </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> </DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman">> bad () =
_|_ </FONT></FONT></DIV>
<DIV><FONT face=Calibri><FONT face="Times New Roman">> 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 in the definitions of the functions if we want
to prove the equvalence between them?</FONT></DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3></FONT> </DIV>
<DIV style="FONT: 10pt Tahoma"><FONT face=Calibri size=3>However, in the case
of </FONT><FONT face=Calibri size=3>map f _|_ , 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> </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> </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 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 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><<A
title="mailto:max.cs.2009@googlemail.com CTRL + Click to follow link"
href="mailto:max.cs.2009@googlemail.com">max.cs.2009@googlemail.com</A>></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> </DIV>
<DIV><FONT face=Calibri>so you mean the </FONT><FONT
face="Times New Roman"> _|_ is necessary only when I have defined the
pattern _|_ such as</FONT></DIV>
<DIV> </DIV>
<DIV><FONT face=Calibri>foo [] = []</FONT></DIV>
<DIV class=Ih2E3d>
<DIV><FONT face=Calibri>foo </FONT><FONT face="Times New Roman">
_|_ = _|_ </FONT></DIV>
<DIV>foo (x:xs) = x( foo xs )</DIV></DIV>
<DIV>-- consider non-termination case</DIV></DIV></BLOCKQUOTE>
<DIV><BR>That is illegal Haskell. 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 _|_. 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> 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:<BR><BR>bad () = _|_ -- 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? Well, it either
terminates or it doesn't, right? I.e. fix f = () or fix f =
_|_.<BR><BR>Taking into account that fix f = f (fix f):<BR>If it does: 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>