pbrowne wrote:
2) What, if anything, prevents the execution of a Haskell term from being a proof in equational logic?
I have done some checking to try to answer my own question. The answer *seems* to be that there *seems* to be three things that prevent Haskell terms being true equations. Any feedback on these three reason would be welcome. If they are valid reasons, what is their possible impact? Pat --------------------Reason (1)------------------ There are some equations that are not expressible in Haskell. Quoting form: http://www.mail-archive.com/haskell-cafe@haskell.org/msg64843.html Is there any way to achieve such a proof in Haskell itself?
GHC appears to reject equations such has mirror (mirror x) = x mirror (mirror(Node x y z)) = Node x y z
Eugene Kirpichov Fri, 25 Sep 2009 04:19:32 -0700 It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed. Another example from [5]. A partial order that is also linear is called a total order. The class linorder of total orders is specified using the usual total order axioms. Of course, such axiomatizations are not possible in Haskell. --------------------Reason (2)------------------ According to Thompson [1] the equations in Miranda (and I assume Haskell) are not pure mathematical equations due to *where* and other reasons. According to Danielsson [2] the fact that they are not always structurally equations does not prevent functional programmers from using them as if they were valid equations. Danielsson show that this informal *fast and loose* use of equational axioms and theorems is *morally correct*. In particular, it is impossible to transform a terminating program into a looping one. These results justify the informal reasoning that functional programmers use. --------------------Reason (3)------------------ There is no formal specification for the meaning of a Haskell program (i.e. its meaning is not defined in a logic). At the level of precise logical specification and logical interoperability this could be a problem (e.g. semantic web likes logic). This should not be a problem for programming tasks, after all most languages like Java do not have a formal semantic definition in logic (ML, Maude[3] and CafeOBJ[4] do). [1]A Logic for Miranda, Revisited (1994) by Simon Thompson http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.149 [2] Fast and Loose Reasoning is Morally Correct - Danielsson, Hughes http://citeseer.ist.psu.edu/733155.html [3] http://maude.cs.uiuc.edu/ [4] http://www.ldl.jaist.ac.jp/cafeobj/ [5]Translating Haskell to Isabelle: Torrini, Lueth,Maeder,Mossakowski http://es.cs.uni-kl.de/TPHOLs-2007/proceedings/B-178.pdf