On Jan 23, 2007, at 14:48 , Robert Dockins wrote:
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.
I'm not expressing myself well, and I don't have the terminology or enough understanding of things like category theory or formal logic to express myself at all clearly. :(
I am modeling _|_ in Haskell as a "failed" computation: either a nonterminating computation, or an impossible operation (e.g. head []). Once you have an actualized _|_ (or a possible one, as when you apply seq to a computation which may be _|_), your entire computation is suspect.
I am modeling (p^~p)->q in logic as a "failed" production: once you have produced it, your entire logical production is suspect.
It seems to me that the recent discussions about forcing strictness are deliberately introducing the equivalent of (p^~p)->q, and it's not clear to me that you can really reason about the resulting behavior. The recent discussions which have seq (or alternatives) leading to theoretical difficulties seem to bear this out.
-- brandon s. allbery [linux,solaris,freebsd,perl] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon university KF8NH _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
