On Jan 23, 2007, at 2:09 PM, Brandon S. Allbery KF8NH wrote:
Can someone explain to me, given that (a) I'm not particularly expert at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a bit fuzzybrained of late:
Given that _|_ represents in some sense any computation not representable in and/or not consistent with Haskell,
I'm not sure you've got quite the right notion of what bottom "means." There are lots of computations that are representable in Haskell that are equivalent to _|_. _|_ is just a name we give to the class of computations that don't act right (terminate).
why/how is reasoning about Haskell program behavior in the presence of _|_ *not* like reasoning about logic behavior in the presence of (p^~p)->q?
You seem to be talking around the edges of the Curry-Howard isomorphism. C-H basically says that there is a correspondence between typed lambda calculi and some logical system. Types correspond to logical formulas and lambda terms correspond to proofs. However, a system like Haskell's (where every type is inhabited) corresponds to an inconsistent logic (one where every well- formed statement is provable). That just means that the logic system corresponding to Haskell's type system isn't a very useful one. However, we don't reason _about_ Haskell using that logic, so its not really a problem. Its possible, however, that I don't understand your question. The formula (p^~p)->q (AKA, proof by contradiction) is valid most classical and constructive logics that I know of, so I'm not quite sure what you're getting at. Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG