boolsimplifier-0.1.8: Simplification tools for simple propositional formulas.

Copyright (c) Gershom Bazerman, Jeff Polakow 2011 BSD 3 Clause gershomb@gmail.com experimental None Haskell98

Data.BoolSimplifier

Description

Machinery for representing and simplifying simple propositional formulas. Type families are used to maintain a simple normal form, taking advantage of the duality between "And" and "Or". Additional tools are provided to pull out common atoms in subformulas and otherwise iterate until a simplified fixpoint. Full and general simplification is NP-hard, but the tools here can take typical machine-generated formulas and perform most simplifications that could be spotted and done by hand by a reasonable programmer.

While there are many functions below, only `qAtom`, `andq`(s), `orq`(s), and `qNot` need be used directly to build expressions. `simplifyQueryRep` performs a basic simplification, `simplifyIons` works on expressions with negation to handle their reduction, and `fixSimplifyQueryRep` takes a function built out of any combination of basic simplifiers (you can write your own ones taking into account any special properties of your atoms) and runs it repeatedly until it ceases to reduce the size of your target expression.

The general notion is either that you build up an expression with these combinators directly, simplify it further, and then transform it to a target semantics, or that an expression in some AST may be converted into a normal form expression using such combinators, and then simplified and transformed back to the original AST.

Here are some simple interactions:

```Prelude Data.BoolSimplifier> (qAtom "A") `orq` (qAtom "B")
QOp | fromList [QAtom Pos "A",QAtom Pos "B"] fromList []```
```Prelude Data.BoolSimplifier> ppQueryRep \$ (qAtom "A") `orq` (qAtom "B")
"(A | B)"```
```Prelude Data.BoolSimplifier> ppQueryRep \$ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A"))
"(A)"```
```Prelude Data.BoolSimplifier> ppQueryRep \$ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))
"((A | B) & (A | C))"```
```Prelude Data.BoolSimplifier> ppQueryRep \$ simplifyQueryRep \$ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))
"((A | (B & C)))"```

Synopsis

# Documentation

data QOrTyp Source

Instances

 Show QOrTyp QNot QOrTyp PPConstQR QOrTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QOrTyp QOrTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QOrTyp PPQueryRep (QueryRep QOrTyp (Ion String)) type QNeg QOrTyp = QAndTyp type QFlipTyp QOrTyp = QAndTyp

data QAndTyp Source

Instances

 Show QAndTyp QNot QAndTyp PPConstQR QAndTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QAtomTyp Ord a => CombineQ a QAndTyp QOrTyp Ord a => CombineQ a QAndTyp QAndTyp PPQueryRep (QueryRep QAndTyp (Ion String)) type QNeg QAndTyp = QOrTyp type QFlipTyp QAndTyp = QOrTyp

data QAtomTyp Source

Instances

 QNot QAtomTyp HasClause fife QAtomTyp Ord a => CombineQ a QAtomTyp QAtomTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QAndTyp QAtomTyp PPQueryRep (QueryRep QAtomTyp (Ion String)) type QNeg QAtomTyp = QAtomTyp

type family QFlipTyp t :: * Source

disjunction is the dual of conjunction and vice-versa

Instances

 type QFlipTyp QAndTyp = QOrTyp type QFlipTyp QOrTyp = QAndTyp

data QueryRep qtyp a where Source

A formula is either an atom (of some type, e.g. `String`).

A non-atomic formula (which is either a disjunction or a conjunction) is n-ary and consists of a `Set` of atoms and a set of non-atomic subformulas of dual connective, i.e. the non-atomic subformulas of a disjunction must all be conjunctions. The type system enforces this since there is no `QFlipTyp` instance for `QAtomTyp`.

Constructors

 QAtom :: Ord a => a -> QueryRep QAtomTyp a QOp :: (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a

Instances

 Eq a => Eq (QueryRep qtyp a) Ord a => Ord (QueryRep qtyp a) Show a => Show (QueryRep qtyp a) PPQueryRep (QueryRep qtyp String) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a) Source

qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp a Source

convenience constructors, not particularly smart

class PPQueryRep a where Source

pretty printer class

Methods

ppQueryRep :: a -> String Source

Instances

 PPQueryRep (QueryRep qtyp String) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

qop :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a Source

smart constructor for `QOp` does following optimization: a /\ (a \/ b) <-> a, or dually: a \/ (a /\ b) <-> a

extractAtomCs :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep qtyp a) -> (Set (QueryRep qtyp a), Set (QueryRep QAtomTyp a)) Source

class HasClause fife qtyp where Source

QueryReps can be queried for clauses within them, and clauses within them can be extracted.

Methods

hasClause :: QueryRep fife a -> QueryRep qtyp a -> Bool Source

stripClause :: QueryRep qtyp a -> QueryRep fife a -> QueryRep fife a Source

Instances

 (~) * (QFlipTyp fife) qtyp => HasClause fife qtyp HasClause fife QAtomTyp

andqs :: Ord a => CombineQ a qtyp QAndTyp => [QueryRep qtyp a] -> QueryRep QAndTyp a Source

convenience functions

orqs :: Ord a => CombineQ a qtyp QOrTyp => [QueryRep qtyp a] -> QueryRep QOrTyp a Source

class CombineQ a qtyp1 qtyp2 where Source

smart constructors for `QueryRep`

Methods

andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp a Source

orq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp a Source

Instances

 Ord a => CombineQ a QAtomTyp QAtomTyp Ord a => CombineQ a QAtomTyp QOrTyp Ord a => CombineQ a QAtomTyp QAndTyp Ord a => CombineQ a QOrTyp QAtomTyp Ord a => CombineQ a QOrTyp QOrTyp Ord a => CombineQ a QOrTyp QAndTyp Ord a => CombineQ a QAndTyp QAtomTyp Ord a => CombineQ a QAndTyp QOrTyp Ord a => CombineQ a QAndTyp QAndTyp

simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a Source

(a /\ b) \/ (a /\ c) \/ d <-> (a /\ (b \/ c)) \/ d (and also the dual)

getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a, Set (QueryRep fife a), Set (QueryRep fife a)) Source

Given a set of QueryReps, extracts a common clause if possible, returning the clause, the terms from which the clause has been extracted, and the rest.

getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a, Set (QueryRep fife a), Set (QueryRep fife a)) Source

fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a Source

Takes any given simplifier and repeatedly applies it until it ceases to reduce the size of the query reprepresentation.

data Ion a Source

We can wrap any underying atom dype in an Ion to give it a "polarity" and add handling of "not" to our simplification tools.

Constructors

 Neg a Pos a

Instances

 Eq a => Eq (Ion a) Ord a => Ord (Ion a) Show a => Show (Ion a) PPQueryRep (QueryRep QAtomTyp (Ion String)) PPQueryRep (QueryRep QAndTyp (Ion String)) PPQueryRep (QueryRep QOrTyp (Ion String))

qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a) Source

class PPConstQR qtyp where Source

Methods

ppConstQR :: QueryRep qtyp a -> String Source

Instances

 PPConstQR a PPConstQR QAndTyp PPConstQR QOrTyp

class QNot qtyp where Source

Associated Types

type QNeg qtyp Source

Methods

qNot :: QueryRep qtyp (Ion a) -> QueryRep (QNeg qtyp) (Ion a) Source

Instances

 QNot QAtomTyp QNot QAndTyp QNot QOrTyp

simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a) Source

``` a  /\  (b \/ ~b)  /\  (c \/ d)   <->   a /\ (c \/ d)
a  /\  ~a         /\  (b \/ c)   <->   False
(a \/ ~a)  /\  (b \/ ~b)  <->   True  (*)```

and duals

`N.B. 0-ary \/ is False and 0-ary /\ is True`

maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> a Source