User loginNavigation 
Haskell and logicQuestion What,if anything, prevents the execution of a Haskell term from being a proof in equational logic? Below are some things thay may impede treating Haskell as a logical system with terms being true equations. Any feedback on these reasons would be welcome. Are they are valid reasons? What is their possible impact? Are there more reason? Reason (1) There are some equations that are not expressible in Haskell e.g. mirror (mirror x) = x . 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 Torrini et al discusses specifying order. 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. They conclude that such axiomatizations are not possible in Haskell. Reason (2) According to Thompson the equations in Miranda (and I assume Haskell) are not pure mathematical equations due to *where* and other reasons. According to Danielsson the fact that they are not always structurally equations does not prevent functional programmers from Kieburtz states that neither the syntax nor type system discriminate between values and latent computations. 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 (like Maude or CafeOBJ ). By Patrick Browne at 20091214 21:43  LtU Forum  previous forum topic  next forum topic  other blogs  4472 reads

Browse archivesActive forum topics
New forum topics

Recent comments
12 min 55 sec ago
32 min 11 sec ago
37 min 1 sec ago
56 min 53 sec ago
1 hour 3 min ago
1 hour 10 min ago
1 hour 12 min ago
1 hour 19 min ago
1 hour 22 min ago
2 hours 9 min ago