Brandon S. Allbery KF8NH wrote: > That's not quite what I was trying to say. (p^~p)->q is equivalent > to _|_ in the sense that once you derive/compute (respectively) it, > the "world" in which it exists breaks. (I don't think formal logic > can have a Haskell-like _|_, but deriving (p^~p)->q is close to it in > effect.)
Here's a couple of papers you might like... "Fast and Loose Reasoning is Morally Correct" http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf "Precise Reasoning About Non-strict Functional Programs How to Chase Bottoms, and How to Ignore Them" http://www.cs.chalmers.se/~nad/publications/danielsson-lic.pdf "Total Functional Programming" http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf Greg Buchholz _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
