Haskell and logic

Question

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
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.

Kieburtz states that neither the syntax nor type system discriminate between values and latent computations.
To prove some property of a Haskell program the verification logic must support such distinctions. To address this shortcomming of Haskell Kieburtz has included P-Logic in the Programatica Project to provide a verification logic for Haskell

--------------------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 ).

Symbolic and type-based

Symbolic and type-based analyses are greatly hindered by Haskell's potential for non-termination, which allows all types to be occupied by 'bottom'.

As you note with Reason (1), Haskell also doesn't readily support the expression of axioms or relationships between them - assertions or assumptions over domains regarding which a proof is to occur. OBJ and Maude do a better job here.

That isn't to say Haskell cannot be used for proofs. But Haskell isn't offering much support for proving interesting things. Haskell offers none of the support for providing and verifying proof / evaluation strategies and such offered by real proof systems - these proof strategies are absolutely necessary to make proof-systems achieve practical performance and reduce developer overhead for anything non-trivial.

Reason (3) does not seem to be a valid one. I may err, but I cannot think of any logic with a formal specification of meaning (except in terms of another logic... I suspect there'd be some sort of regression problem attempting to ground any logic).

By dmbarbour at Mon, 2009-12-14 21:54 | login or register to post comments

Reason (3) does not seem to be a valid one.

It is nice to know a)the axioms of a particular logical systems and b)how closely a language adheres to those axioms.
For example, the distinction between the operational and logical semantics of CafeOBJ can be seen in 4.2 of Logical Semantics for CafeOBJ

Also see

Logical Foundations of CafeOBJ,

and CafeOBJ Report

Are there similar documents for Haskell?

By Patrick Browne at Thu, 2009-12-17 11:23 | login or register to post comments

You might want to look at Pure

Pure performs equational reasoning directly with reduction rules, and is not limited to lambda calculus / constructor discipline. Unlike Haskell, it is eager by default and dynamically typed. You can type

> mirror (mirror x) = x;
> mirror 2;
mirror 2
> mirror (mirror 2);
2

The second result shows that mirror 2 is in normal form. Note that there are no layout rules in Pure, so you must use ; as a terminator.

By johnwcowan at Mon, 2009-12-14 23:53 | login or register to post comments

Where is the logic in Haskell?

There is a lot of research on Haskell that involves logic (e.g. Patricia Johann ). There are also proposals on how to provide a logic for Haskell (e.g. P-logic ). However, the body of the Haskell report does not include the word logic at all

By Patrick Browne at Tue, 2009-12-15 21:04 | login or register to post comments

Haskell 98 Report

This document is intentionally written in the style you seem to be pointing out as a weakness. I think the Haskell Report makes perfect sense from the standpoint of a "base language" for functional programming research.

Maude and CafeOBJ are vastly different, and more similar in precision to Standard ML.

Maude is also an interesting comparison to Haskell, though. Through the use of reflecting on terms to specify rewriting, you can build new languages within Maude that have their own semantics. All this without changing the compiler. For example, the paper Principles of Mobile Maude demonstrates this flexibility fairly well.

By Z-Bo at Fri, 2009-12-18 18:27 | login or register to post comments

Lambda the Ultimate

User login

Navigation