Re: [Haskell-cafe] bottom case in proof by induction
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 ; raeck@msn.com Subject: Re: [Haskell-cafe] bottom case in proof by induction On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <max.cs.2009@googlemail.com> 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
On Thu, 2009-01-01 at 03:50 +0000, raeck@msn.com 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
Am Donnerstag, 1. Januar 2009 04:50 schrieb raeck@msn.com:
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
participants (3)
-
Daniel Fischer -
Jonathan Cast -
raeck＠msn.com