
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.mailarchive.com/[email protected]/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.unikl.de/TPHOLs2007/proceedings/B178.pdf
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

