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 |
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 |
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 > bad () = _|_ > bad _|_ = () 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? 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 _|_ . Thanks Raeck From: Luke Palmer Sent: Wednesday, December 31, 2008 10:43 PM To: Max.cs ; [hidden email] Subject: Re: [Haskell-cafe] bottom case in proof by induction On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <[hidden email]> wrote: thanks Luke, so you mean the _|_ is necessary only when I have defined the pattern _|_ such as foo [] = [] foo _|_ = _|_ foo (x:xs) = x( foo xs ) -- consider non-termination case That is illegal Haskell. But another way of putting that is that whenever you do any pattern matching, eg.: 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: halts () = True halts _|_ = False Because _|_ is the denotation of a program which never halts. To do it a bit more domain-theoretically, I'll first cite the result that every function has a fixed point. 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: bad () = _|_ -- you can't write _|_ in Haskell, but "undefined" or "let x = x in x" mean the same thing bad _|_ = () Then what is fix f? Well, it either terminates or it doesn't, right? I.e. fix f = () or fix f = _|_. Taking into account that fix f = f (fix f): If it does: fix f = () = f () = _|_, a contradiction. If it doesn't: fix f = _|_ = f _|_ = (), another contradiction. >From a mathematical perspective, that's why you can't pattern match on _|_. >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... Luke -------------- next part -------------- An HTML attachment was scrubbed... URL: http://www.haskell.org/pipermail/beginners/attachments/20090101/51738186/attachment.htm |
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 > |
In reply to this post by Luke Palmer-2
Luke Palmer wrote:
> 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. Would it in general also be interesting to look at foo == id for input (_|_:xs) and all other possible positions and combinations of positions for bottom? I wonder how many cases you need to take into consideration to have covered every possible situation. Martijn. |
In reply to this post by raeck@msn.com
On Thu, 2009-01-01 at 03:50 +0000, [hidden email] wrote:
> 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 _|_ = _|_ ? This definition is taken care of for you by the definition of Haskell pattern matching. If the first equation for a function has a pattern other than * a variable or * a lazy pattern (~p) for a given argument, then supplying _|_ for that argument /must/ (if the application is total) return _|_. By rule. (We say the pattern is strict, in this case). > and in the case of > > > bad () = _|_ > > bad _|_ = () Note that these equations (which are not in the right form for the Haskell equations that define Hasekll functions) aren't satisfied by any Haskell function! > mean not every function with a _|_ input will issue a _|_ output, True --- but we can say a couple of things: * For all Haskell functions f, if f _|_ is an application of a constructor C, then f x is an application of C (to some value), for all x. [1] * For all Haskell functions f, if f _|_ is a lambda expression, then f x is a lambda expression, for all x. The only other possibility for f _|_ is _|_. (Do you see why bad above is impossible?) > 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? You have to deduce what the value at _|_ will be. > 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? Appeal to the semantics of Haskell pattern matching. If you like, you can de-sugar the definition of map a little, to get map = \ f xn -> case xn of [] -> [] x:xn0 -> f x : map f xn0 And then you know that case _|_ of [] -> ... ... = _|_ whatever you fill in for the ellipses. (Do you see why this *must* be part of the language definition?) > ps, the definition of map does not mention anything about _|_ . The behavior of map f _|_ is fixed by the definition of Haskell pattern matching. jcc |
Free forum by Nabble | Edit this page |