0
$\begingroup$

I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \Rightarrow p$ the conjunction was split giving $a \Rightarrow p$ and $w \Rightarrow p$ and then the contrapositive rule was applied giving $\neg p \Rightarrow \neg a$ and $\neg p \Rightarrow \neg w$. I then translated those propositions into Haskell conditional equations.

Is the Haskell representation a reasonable transformation? Is there a relation between the execution of the Haskell expression not e a proof of theorem $\neg e$?

Natural language

If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent evil, he would be ineffective; if he were unwilling to prevent evil, he would be malevolent. Superman does not prevent evil. If Superman exists, he is neither ineffective nor malevolent. Therefore Superman does not exist.

Formalize

$a$: Superman is able to prevent evil.

$w$: Superman is willing to prevent evil.

$i$: Superman is ineffective.

$m$: Superman is malevolent.

$p$: Superman prevents evil.

$e$: Superman exists.

S0 : $a \land w \Rightarrow p$

S1 : $(\neg a \Rightarrow i) \land (\neg w \Rightarrow \neg m)$

S2 : $\neg p$

S3 : $e \Rightarrow \neg i \land \neg m$

module SUPERMAN where
 a::Bool
 w::Bool
 i::Bool
 p::Bool
 e::Bool

 a | (not p) = False  -- S0a
 w | (not p)  = False -- S0b
 i | (not a) = True   -- S1a
 m | (not w) = True   -- S1b
 p = False            -- S2
 e | (i || m) = False -- S3
-- Theorems (not e), (i || m), and (i && a) all hold
$\endgroup$
  • 3
    $\begingroup$ Is there an important reason to use Haskell? You might find it helpful if I point you to Prolog for these kind of tasks. $\endgroup$ – Sandro Lovnički Dec 21 '18 at 22:56
  • 1
    $\begingroup$ @SandroLovnički I am researching specific claims made about Haskell and proofs e.g. an earlier question $\endgroup$ – Patrick Browne Dec 22 '18 at 0:40
  • 2
    $\begingroup$ Haskell is a programming language, not a proof assistant / theorem prover, or a system for automated reasoning over logical theories. At most, given boolean values for variables, it can compute boolean expressions, essentially applying truth tables, like most programming languages can. $\endgroup$ – chi Dec 22 '18 at 9:15
  • $\begingroup$ @chi So the relation between the execution and a proof is that with Haskell (or other language) we can compute a truth table? Is this TT a model or interpretation of the original propositions? $\endgroup$ – Patrick Browne Dec 22 '18 at 9:54
4
$\begingroup$

Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding evaluation of Boolean values instead of proofs, and these are two completely different things.

When people speak about "Haskell proving things" they mean the following: given a type t which represents a proposition $T$ via the propositions as types translation, does there exists a Haskell program p of type t which corresponds to a proof of $T$?

Example: the proposition $((A \land B \Rightarrow C) \Rightarrow (A \Rightarrow B) \Rightarrow (A \Rightarrow C)$ corresponds to the (polymorphic) type ((a,b) -> c) -> (a -> b) -> (a -> c). The program \ f g x -> f (x, g x) has this type, and therefore corresponds to a proof of the proposition. The kind of logic that can be represented in this way is intuitionistic.

However, because Haskell has general recursion, not every Haskell program corresponds to a proof, and in fact Haskell cannot be considered as a proof system. It is a programming language. A better choice is Agda or Idris.

You are translating propositions into Boolean algebra which you then encode using the Haskell datatype Bool. You are therefore misusing the phrase "prove in Haskell". At best you are trying to evaluate Boolean expressions, which is not the same thing. You defined, in a somewhat convoluted way, a (partial) evaluation strategy that evaluates various Boolean propositions. It's not a very good one, for instance if you change p = True line to p = False, your program fails to evaluate a.

This has nothing whatsoever to do with Haskell because it is not specific to it. You can do the exact same thing in just about any programming language, and even in Excel. However, as was suggested already twice, prolog seems to be the most appropriate tool for the problem at hand. You are not "researching" Haskell here. I believe we already tried to explain this to you in the previous question you linked to. I hope it gets across this time.

$\endgroup$
  • $\begingroup$ I am aware of the type level reasoning and the role of Prolog and I completely agree with your comments. There is a body of researchers who have made what I believe to be exaggerated claims about Haskell, claiming that Haskell can represent theories that can be proved. My posts are attempts to look for any evidence of these claims. $\endgroup$ – Patrick Browne Dec 22 '18 at 11:01
  • 1
    $\begingroup$ What does "Haskell can represent theories that can be proved" mean? And who are these mysterious researchers? $\endgroup$ – Andrej Bauer Dec 22 '18 at 21:56
  • $\begingroup$ Not sure. More statements I am unsure of: Axioms expressed in Haskell, types as theories, I do understand Goguen's version, Haskell as an algebraic specification language and prove the correctness $\endgroup$ – Patrick Browne Dec 23 '18 at 10:34
  • $\begingroup$ In particular I have difficulty in understanding Werner Kuhn's approach to Haskell see an earlier question. $\endgroup$ – Patrick Browne Dec 23 '18 at 11:08
  • 1
    $\begingroup$ @PatrickBrowne: I am not impressed by that paper. They are confused by the word "constructive". The statement $\exists y . y^2 = x$ has a constructive proof, but they claim it is non-constructive. They do not seem to know the difference between "constructive" and "has an operational semantics". They do not address the fact that Haskell only supports expression of very specific equations that are executable (for instance, they cannot express something as simple as commutativity). The baby examples are just an intro to Haskell programming, far from anything realistic. And so on. $\endgroup$ – Andrej Bauer Jan 23 at 7:19

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.