[Haskell-cafe] Propositional logic implementation

[Holger Siegel]

On Sunday 11 January 2009 01:44:50 Andrew Wagner wrote:
> Nice Idea, though I don't know that I want something that extensive. I was
> more looking for whether there was a better way I could define the
> algebraic data type.

Let's have a look at your definitions from http://hpaste.org/13807#a1 :

> data Sentence = Atomic Atom | Complex Complex

The distinction between atomic expressions and complex expressions seems to be 
merely academic: None of your functions actually distinguishes between them. 
Thus, I suggest that you move the constructors of type Atom and Complex to 
type Sentence.

The only place where type Atom is used is in the following declaration:

> newtype Model = Model [Atom]

But a close look at function true :: Model -> Sentence -> Bool reveals that it 
is sufficient to make a model a list of symbols. Therefore, we modify type Model 
to

type Model = [Symbol]

If Symbol was an instance of type class Ord, we could even move from lists to 
sets:

import qualified Data.Set as Set
type Model = Set.Set Symbol

Then function symbols could also return sets of symbols, allowing for a much 
more efficient implementation via Set.union instead of List.nub and List.++:

symbols :: Sentence -> Set.Set Symbol

> data Atom = T | F | Symbol Symbol deriving Eq

In function symbols you need to distinguish between symbols and other values 
of type Atom. With your current definition, function symbol must evaluate every 
atom to a concrete truthvalue. We can avoid this by defining Atom as

data Atom = Const Bool | Symbol Symbol deriving Eq

> data Symbol = A | B | C | P | Q | R | X | Y | Z | Label String deriving Eq

I don't like two things about this definition:
1) There are two kinds of symbols, but there is no clear distinction between 
them. Instead, String-type labels are modelled as one special case of a 
symbol.
2) You enumerate characters explicitly. Instead, you could use type Char for 
single-character symbols. 

If you define symbols by

type Symbol = Either Char String

then you have a clear distinction between single-character symbols and labels, 
and you also get the above-mentioned instance of typeclass Ord for free.

> data Complex = Not Sentence
>             | Sentence :/\: Sentence
>             | Sentence :\/: Sentence
>             | Sentence :=>: Sentence
>             | Sentence :<=>: Sentence

There are some opportunities to reduce the number of constructors in this 
declaration. Constructor :=>: can easily be replaced by a function

(==>) :: Sentence -> Sentence -> Sentence
a ==> b  = Not a :/\: b

You can even define true, false, negation, conjunction and disjunction in terms 
of a newly introduced constructor

  Nand [Sentence]

so that

false = Nand []
true = Nand [false]

Operator <=> can also be expressed in terms of Nand, but that would lead to 
duplicated work in function symbol and function true. Thus, we keep 
constructor :<=>:.

The resulting declarations are

data Sentence = Nand [Sentence]
              | Sentence :<=>: Sentence
              | Symbol Symbol

type Symbol = Either Char String

type Model = Set.Set Symbol

This will reduce your boilerplate code to a minimum. :)

Regards,
Holger