atp-haskell-1.7: src/Data/Logic/ATP/Prop.hs
-- | Basic stuff for propositional logic: datatype, parsing and
-- printing. 'IsPropositional' is a subclass of 'IsLiteral' of
-- formula types that support binary combinations.
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Logic.ATP.Prop
( -- * binary operations
BinOp(..), binop
-- * Propositional formulas
, IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)
, (⇒), (==>), (⊃), (→)
, (⇔), (<=>), (↔), (<==>)
, (∧), (·)
, (∨)
, foldPropositional
, zipPropositional
, convertPropositional
, convertToPropositional
, precedencePropositional
, associativityPropositional
, prettyPropositional
, showPropositional
, onatomsPropositional
, overatomsPropositional
-- * Restricted propositional formula class
, JustPropositional
-- * Interpretation of formulas.
, eval
, atoms
-- * Truth Tables
, TruthTable(TruthTable)
, onallvaluations
, truthTable
-- * Tautologies and related concepts
, tautology
, unsatisfiable
, satisfiable
-- * Substitution
, psubst
-- * Dualization
, dual
-- * Simplification
, psimplify
, psimplify1
-- * Normal forms
, nnf
, nenf
, list_conj
, list_disj
, mk_lits
, allsatvaluations
, dnfSet
, purednf
, simpdnf
, rawdnf
, dnf
, purecnf
, simpcnf
, cnf'
, cnf_
, trivial
-- * Instance
, Prop(P, pname)
, PFormula(F, T, Atom, Not, And, Or, Imp, Iff)
-- * Tests
, testProp
) where
import Data.Foldable as Foldable (null)
import Data.Function (on)
import Data.Data (Data)
import Data.List as List (groupBy, intercalate, map, sortBy)
import Data.Logic.ATP.Formulas (atom_union, fromBool, IsAtom,
IsFormula(AtomOf, asBool, true, false, atomic, overatoms, onatoms), prettyBool)
import Data.Logic.ATP.Lib ((|=>), distrib, fpf, setAny)
import Data.Logic.ATP.Lit ((.~.), (¬), convertLiteral, convertToLiteral, IsLiteral(foldLiteral', naiveNegate, foldNegation),
JustLiteral, LFormula, negate, positive, )
import Data.Logic.ATP.Pretty (Associativity(InfixN, InfixR, InfixA), Doc, HasFixity(precedence, associativity),
Precedence, Pretty(pPrint, pPrintPrec), prettyShow, Side(Top, LHS, RHS, Unary), testParen, text,
notPrec, andPrec, orPrec, impPrec, iffPrec, leafPrec, boolPrec)
import Data.Map.Strict as Map (Map)
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
import Data.Set as Set (empty, filter, fromList, intersection, isProperSubsetOf, map,
minView, partition, Set, singleton, toAscList, union)
import Data.String (IsString(fromString))
import Data.Typeable (Typeable)
import Prelude hiding (negate, null)
import Text.PrettyPrint.HughesPJClass (maybeParens, PrettyLevel, vcat)
import Test.HUnit
-- | Implication synonyms. Note that if the -XUnicodeSyntax option is
-- turned on the operator ⇒ can not be declared/used as a function -
-- it becomes a reserved special character used in type signatures.
(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula
(⇒) = (.=>.)
(⊃) = (.=>.)
(==>) = (.=>.)
(→) = (.=>.)
infixr 3 .=>., ⇒, ⊃, ==>, →
-- | If-and-only-if synonyms
(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula
(<=>) = (.<=>.)
(<==>) = (.<=>.)
(⇔) = (.<=>.)
(↔) = (.<=>.)
infixl 2 .<=>., <=>, <==>, ⇔, ↔
-- | And/conjunction synonyms
(∧), (·) :: IsPropositional formula => formula -> formula -> formula
(∧) = (.&.)
(·) = (.&.)
infixl 5 .&., ∧, ·
-- | Or/disjunction synonyms
(∨) :: IsPropositional formula => formula -> formula -> formula
(∨) = (.|.)
infixl 4 .|., ∨
data BinOp
= (:<=>:)
| (:=>:)
| (:&:)
| (:|:)
deriving (Eq, Ord, Data, Typeable, Show, Enum, Bounded)
-- | Combine formulas with a 'BinOp'.
binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
binop f1 (:<=>:) f2 = f1 .<=>. f2
binop f1 (:=>:) f2 = f1 .=>. f2
binop f1 (:&:) f2 = f1 .&. f2
binop f1 (:|:) f2 = f1 .|. f2
-- |A type class for propositional logic. If the type we are writing
-- an instance for is a zero-order (aka propositional) logic type
-- there will generally by a type or a type parameter corresponding to
-- atom. For first order or predicate logic types, it is generally
-- easiest to just use the formula type itself as the atom type, and
-- raise errors in the implementation if a non-atomic formula somehow
-- appears where an atomic formula is expected (i.e. as an argument to
-- atomic or to the third argument of foldPropositional.)
class IsLiteral formula => IsPropositional formula where
-- | Disjunction/OR
(.|.) :: formula -> formula -> formula
-- | Conjunction/AND. @x .&. y = (.~.) ((.~.) x .|. (.~.) y)@
(.&.) :: formula -> formula -> formula
-- | Equivalence. @x .<=>. y = (x .=>. y) .&. (y .=>. x)@
(.<=>.) :: formula -> formula -> formula
-- | Implication. @x .=>. y = ((.~.) x .|. y)@
(.=>.) :: formula -> formula -> formula
-- | A fold function that distributes different sorts of formula
-- to its parameter functions, one to handle binary operators, one
-- for negations, and one for atomic formulas. See examples of its
-- use to implement the polymorphic functions below.
foldPropositional' :: (formula -> r) -- ^ fold on some higher order formula
-> (formula -> BinOp -> formula -> r) -- ^ fold on a binary operation formula. Functions
-- of this type can be constructed using 'binop'.
-> (formula -> r) -- ^ fold on a negated formula
-> (Bool -> r) -- ^ fold on a boolean formula
-> (AtomOf formula -> r) -- ^ fold on an atomic formula
-> formula -> r
-- | An alternative fold function for binary combinations of formulas
foldCombination :: (formula -> r) -- other
-> (formula -> formula -> r) -- disjunction
-> (formula -> formula -> r) -- conjunction
-> (formula -> formula -> r) -- implication
-> (formula -> formula -> r) -- equivalence
-> formula -> r
-- | Deconstruct a 'JustPropositional' formula.
foldPropositional :: JustPropositional pf =>
(pf -> BinOp -> pf -> r) -- ^ fold on a binary operation formula
-> (pf -> r) -- ^ fold on a negated formula
-> (Bool -> r) -- ^ fold on a boolean formula
-> (AtomOf pf -> r) -- ^ fold on an atomic formula
-> pf -> r
foldPropositional = foldPropositional' (error "JustPropositional failure")
-- | Combine two 'JustPropositional' formulas if they are similar.
zipPropositional :: (JustPropositional pf1, JustPropositional pf2) =>
(pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) -- ^ Combine two binary operation formulas
-> (pf1 -> pf2 -> Maybe r) -- ^ Combine two negated formulas
-> (Bool -> Bool -> Maybe r) -- ^ Combine two boolean formulas
-> (AtomOf pf1 -> AtomOf pf2 -> Maybe r) -- ^ Combine two atomic formulas
-> pf1 -> pf2 -> Maybe r -- ^ Result is Nothing if the formulas don't unify
zipPropositional co ne tf at fm1 fm2 =
foldPropositional co' ne' tf' at' fm1
where
co' l1 op1 r1 = foldPropositional (co l1 op1 r1) (\_ -> Nothing) (\_ -> Nothing) (\_ -> Nothing) fm2
ne' x1 = foldPropositional (\_ _ _ -> Nothing) (ne x1) (\_ -> Nothing) (\_ -> Nothing) fm2
tf' x1 = foldPropositional (\_ _ _ -> Nothing) (\_ -> Nothing) (tf x1) (\_ -> Nothing) fm2
at' a1 = foldPropositional (\_ _ _ -> Nothing) (\_ -> Nothing) (\_ -> Nothing) (at a1) fm2
-- | Convert any instance of 'JustPropositional' to any 'IsPropositional' formula.
convertPropositional :: (JustPropositional pf1, IsPropositional pf2) =>
(AtomOf pf1 -> AtomOf pf2) -- ^ Convert an atomic formula
-> pf1 -> pf2
convertPropositional ca pf =
foldPropositional co ne tf (atomic . ca) pf
where
co p (:&:) q = (convertPropositional ca p) .&. (convertPropositional ca q)
co p (:|:) q = (convertPropositional ca p) .|. (convertPropositional ca q)
co p (:=>:) q = (convertPropositional ca p) .=>. (convertPropositional ca q)
co p (:<=>:) q = (convertPropositional ca p) .<=>. (convertPropositional ca q)
ne p = (.~.) (convertPropositional ca p)
tf = fromBool
-- | Convert any instance of 'IsPropositional' to a 'JustPropositional' formula. Typically the
-- ho (higher order) argument calls error if it encounters something it can't handle.
convertToPropositional :: (IsPropositional formula, JustPropositional pf) =>
(formula -> pf) -- ^ Convert a higher order formula
-> (AtomOf formula -> AtomOf pf) -- ^ Convert an atomic formula
-> formula -> pf
convertToPropositional ho ca fm =
foldPropositional' ho co ne tf (atomic . ca) fm
where
co p (:&:) q = (convertToPropositional ho ca p) .&. (convertToPropositional ho ca q)
co p (:|:) q = (convertToPropositional ho ca p) .|. (convertToPropositional ho ca q)
co p (:=>:) q = (convertToPropositional ho ca p) .=>. (convertToPropositional ho ca q)
co p (:<=>:) q = (convertToPropositional ho ca p) .<=>. (convertToPropositional ho ca q)
ne p = (.~.) (convertToPropositional ho ca p)
tf = fromBool
-- | Implementation of 'precedence' for any 'JustPropostional' type.
precedencePropositional ::JustPropositional pf => pf -> Precedence
precedencePropositional = foldPropositional co (\_ -> notPrec) (\_ -> boolPrec) precedence
where
co _ (:&:) _ = andPrec
co _ (:|:) _ = orPrec
co _ (:=>:) _ = impPrec
co _ (:<=>:) _ = iffPrec
associativityPropositional :: JustPropositional pf => pf -> Associativity
associativityPropositional = foldPropositional co (const InfixA) (const InfixN) associativity
where
co _ (:&:) _ = InfixA
co _ (:|:) _ = InfixA
co _ (:=>:) _ = InfixR
co _ (:<=>:) _ = InfixA -- yes, InfixA: (a<->b)<->c == a<->(b<->c)
-- | Implementation of 'pPrint' for any 'JustPropostional' type.
prettyPropositional :: forall pf. JustPropositional pf =>
Side -> PrettyLevel -> Rational -> pf -> Doc
prettyPropositional side l r fm =
maybeParens (testParen side r (precedence fm) (associativity fm)) $ foldPropositional co ne tf at fm
where
co :: pf -> BinOp -> pf -> Doc
co p (:&:) q = prettyPropositional LHS l (precedence fm) p <> text "∧" <> prettyPropositional RHS l (precedence fm) q
co p (:|:) q = prettyPropositional LHS l (precedence fm) p <> text "∨" <> prettyPropositional RHS l (precedence fm) q
co p (:=>:) q = prettyPropositional LHS l (precedence fm) p <> text "⇒" <> prettyPropositional RHS l (precedence fm) q
co p (:<=>:) q = prettyPropositional LHS l (precedence fm) p <> text "⇔" <> prettyPropositional RHS l (precedence fm) q
ne p = text "¬" <> prettyPropositional Unary l (precedence fm) p
tf x = prettyBool x
at x = pPrintPrec l r x
-- | Implementation of 'show' for any 'JustPropositional' type. For clarity, show methods fully parenthesize
showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS
showPropositional side parentPrec fm =
showParen (testParen side parentPrec (precedence fm) (associativity fm)) $ foldPropositional co ne tf at fm
where
co p (:&:) q = showPropositional LHS (precedence fm) p . showString " .&. " . showPropositional RHS (precedence fm) q
co p (:|:) q = showPropositional LHS (precedence fm) p . showString " .|. " . showPropositional RHS (precedence fm) q
co p (:=>:) q = showPropositional LHS (precedence fm) p . showString " .=>. " . showPropositional RHS (precedence fm) q
co p (:<=>:) q = showPropositional LHS (precedence fm) p . showString " .<=>. " . showPropositional RHS (precedence fm) q
ne p = showString "(.~.) " . showPropositional Unary (succ (precedence fm)) p
tf x = showsPrec (precedence fm) x
at x = showString "atomic " . showsPrec (precedence fm) x
-- | Implementation of 'onatoms' for any 'JustPropositional' type.
onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf
onatomsPropositional f fm =
foldPropositional co ne tf at fm
where
co p op q = binop (onatomsPropositional f p) op (onatomsPropositional f q)
ne p = (.~.) (onatomsPropositional f p)
tf flag = fromBool flag
at x = atomic (f x)
-- | Implementation of 'overatoms' for any 'JustPropositional' type.
overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r
overatomsPropositional f fof r0 =
foldPropositional co ne (const r0) (flip f r0) fof
where
co p _ q = overatomsPropositional f p (overatomsPropositional f q r0)
ne fof' = overatomsPropositional f fof' r0
-- | An instance of IsPredicate.
data Prop = P {pname :: String} deriving (Eq, Ord)
-- Because of the IsString instance, the Show instance can just be a String.
instance Show Prop where
show (P {pname = s}) = show s
instance IsAtom Prop
-- Allows us to say "q" instead of P "q" or P {pname = "q"}
instance IsString Prop where
fromString = P
instance Pretty Prop where
pPrint = text . pname
instance HasFixity Prop where
precedence (P _) = leafPrec
-- | An instance of IsPropositional.
data PFormula atom
= F
| T
| Atom atom
| Not (PFormula atom)
| And (PFormula atom) (PFormula atom)
| Or (PFormula atom) (PFormula atom)
| Imp (PFormula atom) (PFormula atom)
| Iff (PFormula atom) (PFormula atom)
deriving (Eq, Ord, Read, Data, Typeable)
-- Build a Haskell expression for this formula
instance (IsPropositional (PFormula atom), Show atom) => Show (PFormula atom) where
showsPrec p x = showPropositional Top p x -- . showString " :: PFormula Prop"
instance IsAtom atom => HasFixity (PFormula atom) where
precedence = precedencePropositional
associativity = associativityPropositional
instance IsAtom atom => IsFormula (PFormula atom) where
type AtomOf (PFormula atom) = atom
asBool T = Just True
asBool F = Just False
asBool _ = Nothing
true = T
false = F
atomic = Atom
overatoms = overatomsPropositional
onatoms = onatomsPropositional
instance IsAtom atom => IsPropositional (PFormula atom) where
(.|.) = Or
(.&.) = And
(.=>.) = Imp
(.<=>.) = Iff
foldPropositional' _ co ne tf at fm =
case fm of
Imp p q -> co p (:=>:) q
Iff p q -> co p (:<=>:) q
And p q -> co p (:&:) q
Or p q -> co p (:|:) q
_ -> foldLiteral' (error "IsPropositional PFormula") ne tf at fm
foldCombination other dj cj imp iff fm =
case fm of
Or a b -> a `dj` b
And a b -> a `cj` b
Imp a b -> a `imp` b
Iff a b -> a `iff` b
_ -> other fm
instance IsAtom atom => IsLiteral (PFormula atom) where
naiveNegate = Not
foldNegation normal inverted (Not x) = foldNegation inverted normal x
foldNegation normal _ x = normal x
foldLiteral' ho ne tf at fm =
case fm of
T -> tf True
F -> tf False
Atom a -> at a
Not l -> ne l
_ -> ho fm
instance IsAtom atom => Pretty (PFormula atom) where
pPrintPrec = prettyPropositional Top
-- | Class that indicates a formula type *only* supports Propositional
-- features - it has no way to represent quantifiers.
class IsPropositional formula => JustPropositional formula
instance IsAtom atom => JustPropositional (PFormula atom)
-- | Interpretation of formulas.
eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool
eval fm v =
foldPropositional co ne tf at fm
where
co p (:&:) q = (eval p v) && (eval q v)
co p (:|:) q = (eval p v) || (eval q v)
co p (:=>:) q = not (eval p v) || (eval q v)
co p (:<=>:) q = (eval p v) == (eval q v)
ne p = not (eval p v)
tf = id
at = v
-- | Recognizing tautologies.
tautology :: JustPropositional pf => pf -> Bool
tautology fm = onallvaluations (&&) (eval fm) (\_s -> False) (atoms fm)
-- | Related concepts.
unsatisfiable :: JustPropositional pf => pf -> Bool
unsatisfiable = tautology . (.~.)
satisfiable :: JustPropositional pf => pf -> Bool
satisfiable = not . unsatisfiable
onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
onallvaluations cmb subfn v ats =
case minView ats of
Nothing -> subfn v
Just (p, ps) ->
let v' t q = (if q == p then t else v q) in
cmb (onallvaluations cmb subfn (v' False) ps) (onallvaluations cmb subfn (v' True) ps)
-- | Return the set of propositional variables in a formula.
atoms :: IsFormula formula => formula -> Set (AtomOf formula)
atoms fm = atom_union singleton fm
data TruthTable a = TruthTable [a] [TruthTableRow] deriving (Eq, Show)
type TruthTableRow = ([Bool], Bool)
-- | Code to print out truth tables.
truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf)
truthTable fm =
TruthTable atl (onallvaluations (<>) mkRow (const False) ats)
where
ats = atoms fm
mkRow v = [(List.map v atl, eval fm v)]
atl = Set.toAscList ats
instance Pretty atom => Pretty (TruthTable atom) where
pPrint (TruthTable ats rows) = vcat (List.map (text . intercalate "|" . center) rows'')
where
center :: [String] -> [String]
center cols = Prelude.map (uncurry center') (zip colWidths cols)
center' :: Int -> String -> String
center' width s = let (q, r) = divMod (width - length s) 2 in replicate q ' ' ++ s ++ replicate (q + r) ' '
hdrs = List.map prettyShow ats ++ ["result"]
rows'' = hdrs : List.map (uncurry replicate) (zip colWidths (repeat '-')) : rows'
rows' :: [[String]]
rows' = List.map (\(cols, result) -> List.map prettyShow (cols ++ [result])) rows
cellWidths :: [[Int]]
cellWidths = List.map (List.map length) (hdrs : rows')
colWidths :: [Int]
colWidths = List.map (foldl1 max) (transpose cellWidths)
transpose :: [[a]] -> [[a]]
transpose [] = []
transpose ([] : xss) = transpose xss
transpose ((x:xs) : xss) = (x : [h | (h:_) <- xss]) : transpose (xs : [ t | (_:t) <- xss])
-- | Make sure the precedence and associativity implied by the Haskell
-- infix/infixl/infixr declarations matches the precedence and
-- associativity implied by the HasFixity instances. It would be nice
-- to define one in terms of the other, but I don't know how to query
-- the precedence and associativity of an operator, and I don't know
-- how to (successfully) generate an infix/infixl/infixr declaration
-- using template haskell (the obvious thing didn't work:
--
-- $(pure [InfixD (Fixity quantPrec TH.InfixR) '(∀)])
-- | Tests precedence handling in pretty
-- printer. 1. Need to test: associativity of like operators
-- 2. precedence of every pair of adjacent operators 3. Stuff about
-- infix operators
test00 :: Test
test00 =
{-
TestList [testPrecedence, testAssociativity]
where
testPrecedence :: Test
testPrecedence =
TestList (
-}
TestList (List.map (\(input, expected) -> TestCase $ assertEqual "precedence" (text expected) (pPrint input))
[( p .&. (q .|. r) , "p∧(q∨r)" ),
( (p .&. q) .|. r , "(p∧q)∨r" ),
( p .&. q .|. r , "(p∧q)∨r" ),
( p .|. q .&. r , "p∨(q∧r)" ),
( p .&. q .&. r , "p∧q∧r" ),
( p .|. q .|. r , "p∨q∨r" ),
( (p .=>. q) .=>. r , "(p⇒q)⇒r" ),
( p .=>. (q .=>. r) , "p⇒q⇒r" ),
( p .=>. q .=>. r , "p⇒q⇒r" )])
where
byPrec :: IsPropositional formula => [[(Rational, formula -> formula -> formula)]]
byPrec = groupBy ((==) `on` fst) . sortBy (compare `on` fst) $ binops
-- All the operators we will test, with the 'Precedence' value
-- we assigned. we need to make sure the 'Precedence' value
-- matches the values in the infix/infixl/infixr declarations.
binops :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
binops = ands ++ ors ++ imps ++ iffs
where
ands :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
ands = List.map (andPrec,) [(.&.), (∧), (·)]
ors :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
ors = List.map (orPrec,) [(.|.), (∨)]
imps :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
imps = List.map (impPrec,) [(.=>.), (⇒), (==>), (→), (⊃)]
iffs :: IsPropositional formula => [(Rational, formula -> formula -> formula)]
iffs = List.map (iffPrec,) [(.<=>.), (<=>), (⇔), (↔)]
preops :: IsPropositional formula => [(Rational, formula -> formula)]
preops = nots
where
nots :: IsPropositional formula => [(Rational, formula -> formula)]
nots = List.map (notPrec,) [(.~.), (¬)]
(p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))
-- What about these?
-- (∴)
{-
test00 = TestCase $ assertEqual "parenthesization" expected (List.map prettyShow input)
(input, expected) = unzip [( p .&. (q .|. r) , "p∧(q∨r)" ),
( (p .&. q) .|. r , "(p∧q)∨r" ),
( p .&. q .|. r , "(p∧q)∨r" ),
( p .|. q .&. r , "p∨(q∧r)" ),
( p .&. q .&. r , "p∧q∧r" ),
( (p .=>. q) .=>. r , "(p⇒q)⇒r" ),
( p .=>. (q .=>. r) , "p⇒q⇒r" ),
( p .=>. q .=>. r , "p⇒q⇒r" )]
-}
test01 :: Test
test01 =
let fm = atomic "p" .=>. atomic "q" .<=>. (atomic "r" .&. atomic "s") .|. (atomic "t" .<=>. ((.~.) ((.~.) (atomic "u"))) .&. atomic "v") :: PFormula Prop
input = (prettyShow fm, show fm)
expected = (-- Pretty printed
"p⇒q⇔(r∧s)∨(t⇔u∧v)",
-- Haskell expression
"atomic \"p\" .=>. atomic \"q\" .<=>. (atomic \"r\" .&. atomic \"s\") .|. (atomic \"t\" .<=>. atomic \"u\" .&. atomic \"v\")"
) in
TestCase $ assertEqual "Build Formula 1" expected input
test02 :: Test
test02 = TestCase $ assertEqual "Build Formula 2" expected input
where input = (Atom "fm" .&. Atom "fm") :: PFormula Prop
expected = (And (Atom "fm") (Atom "fm"))
test03 :: Test
test03 = TestCase $ assertEqual "Build Formula 3"
(Atom "fm" .|. Atom "fm" .&. Atom "fm" :: PFormula Prop)
(Or (Atom "fm") (And (Atom "fm") (Atom "fm")))
-- Example of use.
test04 :: Test
test04 = TestCase $ assertEqual "fixity tests" expected input
where (input, expected) = unzip (List.map (\ (fm, flag) -> (eval fm v0, flag)) pairs)
v0 x = error $ "v0: " ++ show x
pairs :: [(PFormula Prop, Bool)]
pairs =
[ ( true .&. false .=>. false .&. true, True)
, ( true .&. true .=>. true .&. false, False)
, ( false ∧ true ∨ true, True) -- "∧ binds more tightly than ∨"
, ( (false ∧ true) ∨ true, True)
, ( false ∧ (true ∨ true), False)
, ( (¬) true ∨ true, True) -- "¬ binds more tightly than ∨"
, ( (¬) (true ∨ true), False)
]
-- Example.
test06 :: Test
test06 = TestCase $ assertEqual "atoms test" (atoms $ p .&. q .|. s .=>. ((.~.) p) .|. (r .<=>. s)) (Set.fromList [P "p",P "q",P "r",P "s"])
where (p, q, r, s) = (Atom (P "p"), Atom (P "q"), Atom (P "r"), Atom (P "s"))
-- Example.
test07 :: Test
test07 = TestCase $ assertEqual "truth table 1 (p. 36)" expected input
where input = (truthTable $ p .&. q .=>. q .&. r)
expected =
(TruthTable
[P "p", P "q", P "r"]
[([False,False,False],True),
([False,False,True],True),
([False,True,False],True),
([False,True,True],True),
([True,False,False],True),
([True,False,True],True),
([True,True,False],False),
([True,True,True],True)])
(p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))
-- Additional examples illustrating formula classes.
test08 :: Test
test08 = TestCase $
assertEqual "truth table 2 (p. 39)"
(truthTable $ ((p .=>. q) .=>. p) .=>. p)
(TruthTable
[P "p", P "q"]
[([False,False],True),
([False,True],True),
([True,False],True),
([True,True],True)])
where (p, q) = (Atom (P "p"), Atom (P "q"))
test09 :: Test
test09 = TestCase $
assertEqual "truth table 3 (p. 40)" expected input
where input = (truthTable $ p .&. ((.~.) p))
expected = (TruthTable
[P "p"]
[([False],False),
([True],False)])
p = Atom (P "p")
-- Examples.
test10 :: Test
test10 = TestCase $ assertEqual "tautology 1 (p. 41)" True (tautology $ p .|. ((.~.) p)) where p = Atom (P "p")
test11 :: Test
test11 = TestCase $ assertEqual "tautology 2 (p. 41)" False (tautology $ p .|. q .=>. p) where (p, q) = (Atom (P "p"), Atom (P "q"))
test12 :: Test
test12 = TestCase $ assertEqual "tautology 3 (p. 41)" False (tautology $ p .|. q .=>. q .|. (p .<=>. q)) where (p, q) = (Atom (P "p"), Atom (P "q"))
test13 :: Test
test13 = TestCase $ assertEqual "tautology 4 (p. 41)" True (tautology $ (p .|. q) .&. ((.~.)(p .&. q)) .=>. ((.~.)p .<=>. q)) where (p, q) = (Atom (P "p"), Atom (P "q"))
-- | Substitution operation.
psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula
psubst subfn fm =
foldPropositional co ne tf at fm
where
co p op q = binop (psubst subfn p) op (psubst subfn q)
ne p = (.~.) (psubst subfn p)
tf = fromBool
at p = fromMaybe (atomic p) (fpf subfn p)
-- Example
test14 :: Test
test14 =
TestCase $ assertEqual "pSubst (p. 41)" expected input
where expected = (p .&. q) .&. q .&. (p .&. q) .&. q
input = psubst ((P "p") |=> (p .&. q)) (p .&. q .&. p .&. q)
(p, q) = (Atom (P "p"), Atom (P "q"))
-- Surprising tautologies including Dijkstra's "Golden rule".
test15 :: Test
test15 = TestCase $ assertEqual "tautology 5 (p. 43)" expected input
where input = tautology $ (p .=>. q) .|. (q .=>. p)
expected = True
(p, q) = (Atom (P "p"), Atom (P "q"))
test16 :: Test
test16 = TestCase $ assertEqual "tautology 6 (p. 45)" expected input
where input = tautology $ p .|. (q .<=>. r) .<=>. (p .|. q .<=>. p .|. r)
expected = True
(p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))
test17 :: Test
test17 = TestCase $ assertEqual "Dijkstra's Golden Rule (p. 45)" expected input
where input = tautology $ p .&. q .<=>. ((p .<=>. q) .<=>. p .|. q)
expected = True
(p, q) = (Atom (P "p"), Atom (P "q"))
test18 :: Test
test18 = TestCase $ assertEqual "Contraposition 1 (p. 46)" expected input
where input = tautology $ (p .=>. q) .<=>. (((.~.)q) .=>. ((.~.)p))
expected = True
(p, q) = (Atom (P "p"), Atom (P "q"))
test19 :: Test
test19 = TestCase $ assertEqual "Contraposition 2 (p. 46)" expected input
where input = tautology $ (p .=>. ((.~.)q)) .<=>. (q .=>. ((.~.)p))
expected = True
(p, q) = (Atom (P "p"), Atom (P "q"))
test20 :: Test
test20 = TestCase $ assertEqual "Contraposition 3 (p. 46)" expected input
where input = tautology $ (p .=>. q) .<=>. (q .=>. p)
expected = False
(p, q) = (Atom (P "p"), Atom (P "q"))
-- Some logical equivalences allowing elimination of connectives.
test21 :: Test
test21 = TestCase $ assertEqual "Equivalences (p. 47)" expected input
where input =
List.map tautology
[ true .<=>. false .=>. false
, ((.~.)p) .<=>. p .=>. false
, p .&. q .<=>. (p .=>. q .=>. false) .=>. false
, p .|. q .<=>. (p .=>. false) .=>. q
, (p .<=>. q) .<=>. ((p .=>. q) .=>. (q .=>. p) .=>. false) .=>. false ]
expected = [True, True, True, True, True]
(p, q) = (Atom (P "p"), Atom (P "q"))
-- | Dualization.
dual :: JustPropositional pf => pf -> pf
dual fm =
foldPropositional co ne tf (\_ -> fm) fm
where
tf True = false
tf False = true
ne p = (.~.) (dual p)
co p (:&:) q = dual p .|. dual q
co p (:|:) q = dual p .&. dual q
co _ _ _ = error "Formula involves connectives .=>. or .<=>."
-- Example.
test22 :: Test
test22 = TestCase $ assertEqual "Dual (p. 49)" expected input
where input = dual (Atom (P "p") .|. ((.~.) (Atom (P "p"))))
expected = And (Atom (P {pname = "p"})) (Not (Atom (P {pname = "p"})))
-- | Routine simplification.
psimplify :: IsPropositional formula => formula -> formula
psimplify fm =
foldPropositional' ho co ne tf at fm
where
ho _ = fm
ne p = psimplify1 ((.~.) (psimplify p))
co p (:&:) q = psimplify1 ((psimplify p) .&. (psimplify q))
co p (:|:) q = psimplify1 ((psimplify p) .|. (psimplify q))
co p (:=>:) q = psimplify1 ((psimplify p) .=>. (psimplify q))
co p (:<=>:) q = psimplify1 ((psimplify p) .<=>. (psimplify q))
tf _ = fm
at _ = fm
psimplify1 :: IsPropositional formula => formula -> formula
psimplify1 fm =
foldPropositional' (\_ -> fm) simplifyCombine simplifyNegate (\_ -> fm) (\_ -> fm) fm
where
simplifyNegate p = foldPropositional' (\_ -> fm) simplifyNotCombine simplifyNotNegate (fromBool . not) simplifyNotAtom p
simplifyCombine l op r =
case (asBool l, op , asBool r) of
(Just True, (:&:), _) -> r
(Just False, (:&:), _) -> fromBool False
(_, (:&:), Just True) -> l
(_, (:&:), Just False) -> fromBool False
(Just True, (:|:), _) -> fromBool True
(Just False, (:|:), _) -> r
(_, (:|:), Just True) -> fromBool True
(_, (:|:), Just False) -> l
(Just True, (:=>:), _) -> r
(Just False, (:=>:), _) -> fromBool True
(_, (:=>:), Just True) -> fromBool True
(_, (:=>:), Just False) -> (.~.) l
(Just False, (:<=>:), Just False) -> fromBool True
(Just True, (:<=>:), _) -> r
(Just False, (:<=>:), _) -> (.~.) r
(_, (:<=>:), Just True) -> l
(_, (:<=>:), Just False) -> (.~.) l
_ -> fm
simplifyNotNegate f = f
simplifyNotCombine _ _ _ = fm
simplifyNotAtom x = (.~.) (atomic x)
-- Example.
test23 :: Test
test23 = TestCase $ assertEqual "psimplify 1 (p. 50)" expected input
where input = psimplify $ (true .=>. (x .<=>. false)) .=>. ((.~.) (y .|. false .&. z))
expected = ((.~.) x) .=>. ((.~.) y)
x = Atom (P "x")
y = Atom (P "y")
z = Atom (P "z")
test24 :: Test
test24 = TestCase $ assertEqual "psimplify 2 (p. 51)" expected input
where input = psimplify $ ((x .=>. y) .=>. true) .|. (.~.) false
expected = true
x = Atom (P "x")
y = Atom (P "y")
-- | Negation normal form.
nnf :: JustPropositional pf => pf -> pf
nnf = nnf1 . psimplify
nnf1 :: JustPropositional pf => pf -> pf
nnf1 fm = foldPropositional nnfCombine nnfNegate fromBool (\_ -> fm) fm
where
-- nnfCombine :: (IsPropositional formula atom) => formula -> Combination formula -> formula
nnfNegate p = foldPropositional nnfNotCombine nnfNotNegate (fromBool . not) (\_ -> fm) p
nnfCombine p (:=>:) q = nnf1 ((.~.) p) .|. (nnf1 q)
nnfCombine p (:<=>:) q = (nnf1 p .&. nnf1 q) .|. (nnf1 ((.~.) p) .&. nnf1 ((.~.) q))
nnfCombine p (:&:) q = nnf1 p .&. nnf1 q
nnfCombine p (:|:) q = nnf1 p .|. nnf1 q
-- nnfNotCombine :: (IsPropositional formula atom) => Combination formula -> formula
nnfNotNegate p = nnf1 p
nnfNotCombine p (:&:) q = nnf1 ((.~.) p) .|. nnf1 ((.~.) q)
nnfNotCombine p (:|:) q = nnf1 ((.~.) p) .&. nnf1 ((.~.) q)
nnfNotCombine p (:=>:) q = nnf1 p .&. nnf1 ((.~.) q)
nnfNotCombine p (:<=>:) q = (nnf1 p .&. nnf1 ((.~.) q)) .|. nnf1 ((.~.) p) .&. nnf1 q
-- Example of NNF function in action.
test25 :: Test
test25 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input
where input = nnf $ (p .<=>. q) .<=>. ((.~.)(r .=>. s))
expected = Or (And (Or (And p q) (And (Not p) (Not q)))
(And r (Not s)))
(And (Or (And p (Not q)) (And (Not p) q))
(Or (Not r) s))
p = Atom (P "p")
q = Atom (P "q")
r = Atom (P "r")
s = Atom (P "s")
test26 :: Test
test26 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input
where input = tautology (Iff fm fm')
expected = True
fm' = nnf fm
fm = (p .<=>. q) .<=>. ((.~.)(r .=>. s))
p = Atom (P "p")
q = Atom (P "q")
r = Atom (P "r")
s = Atom (P "s")
nenf :: IsPropositional formula => formula -> formula
nenf = nenf' . psimplify
-- | Simple negation-pushing when we don't care to distinguish occurrences.
nenf' :: IsPropositional formula => formula -> formula
nenf' fm =
foldPropositional' (\_ -> fm) co ne (\_ -> fm) (\_ -> fm) fm
where
ne p = foldPropositional' (\_ -> fm) co' ne' (\_ -> fm) (\_ -> fm) p
co p (:&:) q = nenf' p .&. nenf' q
co p (:|:) q = nenf' p .|. nenf' q
co p (:=>:) q = nenf' ((.~.) p) .|. nenf' q
co p (:<=>:) q = nenf' p .<=>. nenf' q
ne' p = p
co' p (:&:) q = nenf' ((.~.) p) .|. nenf' ((.~.) q)
co' p (:|:) q = nenf' ((.~.) p) .&. nenf' ((.~.) q)
co' p (:=>:) q = nenf' p .&. nenf' ((.~.) q)
co' p (:<=>:) q = nenf' p .<=>. nenf' ((.~.) q) -- really? how is this asymmetrical?
-- Some tautologies remarked on.
test27 :: Test
test27 = TestCase $ assertEqual "tautology 1 (p. 53)" expected input
where input = tautology $ (p .=>. p') .&. (q .=>. q') .=>. (p .&. q .=>. p' .&. q')
expected = True
p = Atom (P "p")
q = Atom (P "q")
p' = Atom (P "p'")
q' = Atom (P "q'")
test28 :: Test
test28 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input
where input = tautology $ (p .=>. p') .&. (q .=>. q') .=>. (p .|. q .=>. p' .|. q')
expected = True
p = Atom (P "p")
q = Atom (P "q")
p' = Atom (P "p'")
q' = Atom (P "q'")
dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf
dnfSet fm =
list_disj (List.map (mk_lits (Set.map atomic pvs)) satvals)
where
satvals = allsatvaluations (eval fm) (\_s -> False) pvs
pvs = atoms fm
mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf
mk_lits pvs v = list_conj (Set.map (\ p -> if eval p v then p else (.~.) p) pvs)
allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool]
allsatvaluations subfn v pvs =
case Set.minView pvs of
Nothing -> if subfn v then [v] else []
Just (p, ps) -> (allsatvaluations subfn (\a -> if a == p then False else v a) ps) ++
(allsatvaluations subfn (\a -> if a == p then True else v a) ps)
-- | Disjunctive normal form (DNF) via truth tables.
list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
list_conj l | null l = true
list_conj l = foldl1 (.&.) l
list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
list_disj l | null l = false
list_disj l = foldl1 (.|.) l
-- This is only used in the test below, its easier to match lists than sets.
dnfList :: JustPropositional pf => pf -> pf
dnfList fm =
list_disj (List.map (mk_lits' (List.map atomic (Set.toAscList pvs))) satvals)
where
satvals = allsatvaluations (eval fm) (\_s -> False) pvs
pvs = atoms fm
mk_lits' :: JustPropositional pf => [pf] -> (AtomOf pf -> Bool) -> pf
mk_lits' pvs' v = list_conj (List.map (\ p -> if eval p v then p else (.~.) p) pvs')
-- Examples.
test29 :: Test
test29 = TestCase $ assertEqual "dnf 1 (p. 56)" expected input
where input = (dnfList fm, truthTable fm)
expected = ((((((.~.) p) .&. q) .&. r) .|. ((p .&. ((.~.) q)) .&. ((.~.) r))) .|. ((p .&. q) .&. ((.~.) r)),
TruthTable
[P "p", P "q", P "r"]
[([False,False,False],False),
([False,False,True],False),
([False,True,False],False),
([False,True,True],True),
([True,False,False],True),
([True,False,True],False),
([True,True,False],True),
([True,True,True],False)])
fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
(p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))
test30 :: Test
test30 = TestCase $ assertEqual "dnf 2 (p. 56)" expected input
where input = dnfList (p .&. q .&. r .&. s .&. t .&. u .|. u .&. v :: PFormula Prop)
expected = (((((((((((((((((((((((((((((((((((((((.~.) p) .&. ((.~.) q)) .&. ((.~.) r)) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. ((.~.) r)) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. ((.~.) r)) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. ((.~.) r)) .&. s) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. r) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. r) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. r) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. ((.~.) q)) .&. r) .&. s) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. ((.~.) r)) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. ((.~.) r)) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. ((.~.) r)) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. ((.~.) r)) .&. s) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. r) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. r) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. r) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((((.~.) p) .&. q) .&. r) .&. s) .&. t) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. ((.~.) r)) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. ((.~.) r)) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. ((.~.) r)) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. ((.~.) r)) .&. s) .&. t) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. r) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. r) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. r) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. ((.~.) q)) .&. r) .&. s) .&. t) .&. u) .&. v)) .|.
((((((p .&. q) .&. ((.~.) r)) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. q) .&. ((.~.) r)) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((p .&. q) .&. ((.~.) r)) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. q) .&. ((.~.) r)) .&. s) .&. t) .&. u) .&. v)) .|.
((((((p .&. q) .&. r) .&. ((.~.) s)) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. q) .&. r) .&. ((.~.) s)) .&. t) .&. u) .&. v)) .|.
((((((p .&. q) .&. r) .&. s) .&. ((.~.) t)) .&. u) .&. v)) .|.
((((((p .&. q) .&. r) .&. s) .&. t) .&. u) .&. ((.~.) v))) .|.
((((((p .&. q) .&. r) .&. s) .&. t) .&. u) .&. v)
[p, q, r, s, t, u, v] = List.map (Atom . P) ["p", "q", "r", "s", "t", "u", "v"]
-- | DNF via distribution.
distrib1 :: IsPropositional formula => formula -> formula
distrib1 fm =
foldCombination (\_ -> fm) (\_ _ -> fm) lhs (\_ _ -> fm) (\_ _ -> fm) fm
where
-- p & (q | r) -> (p & q) | (p & r)
lhs p qr = foldCombination (\_ -> rhs p qr)
(\q r -> distrib1 (p .&. q) .|. distrib1 (p .&. r))
(\_ _ -> rhs p qr)
(\_ _ -> rhs p qr)
(\_ _ -> rhs p qr)
qr
-- (p | q) & r -> (p & r) | (q & r)
rhs pq r = foldCombination (\_ -> fm)
(\p q -> distrib1 (p .&. r) .|. distrib1 (q .&. r))
(\_ _ -> fm)
(\_ _ -> fm)
(\_ _ -> fm)
pq
{-
distrib1 :: Formula atom -> Formula atom
distrib1 fm =
case fm of
And p (Or q r) -> Or (distrib1 (And p q)) (distrib1 (And p r))
And (Or p q) r -> Or (distrib1 (And p r)) (distrib1 (And q r))
_ -> fm
-}
rawdnf :: IsPropositional formula => formula -> formula
rawdnf fm =
foldPropositional' (\_ -> fm) co (\_ -> fm) (\_ -> fm) (\_ -> fm) fm
where
co p (:&:) q = distrib1 (rawdnf p .&. rawdnf q)
co p (:|:) q = (rawdnf p .|. rawdnf q)
co _ _ _ = fm
{-
rawdnf :: Ord atom => Formula atom -> Formula atom
rawdnf fm =
case fm of
And p q -> distrib1 (And (rawdnf p) (rawdnf q))
Or p q -> Or (rawdnf p) (rawdnf q)
_ -> fm
-}
-- Example.
test31 :: Test
test31 = TestCase $ assertEqual "rawdnf (p. 58)" (prettyShow expected) (prettyShow input)
where input :: PFormula Prop
input = rawdnf $ (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
expected :: PFormula Prop
expected = ((atomic (P "p")) .&. ((.~.)(atomic (P "p"))) .|.
((atomic (P "q")) .&. (atomic (P "r"))) .&. ((.~.)(atomic (P "p")))) .|.
((atomic (P "p")) .&. ((.~.)(atomic (P "r"))) .|.
((atomic (P "q")) .&. (atomic (P "r"))) .&. ((.~.)(atomic (P "r"))))
(p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))
purednf :: (JustPropositional pf,
IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purednf ca fm =
foldPropositional co (\_ -> l2f fm) (\_ -> l2f fm) (\_ -> l2f fm) fm
where
l2f f = singleton . singleton . convertToLiteral (error $ "purednf failure: " ++ prettyShow f) ca $ f
co p (:&:) q = distrib (purednf ca p) (purednf ca q)
co p (:|:) q = union (purednf ca p) (purednf ca q)
co _ _ _ = l2f fm
-- Example.
test32 :: Test
test32 = TestCase $ assertEqual "purednf (p. 58)" expected (purednf id fm)
where fm :: PFormula Prop
fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
expected :: Set (Set (LFormula Prop))
expected = Set.map (Set.map (convertToLiteral (error "test32") id)) $
Set.fromList [Set.fromList [p, (.~.) p],
Set.fromList [p, (.~.) r],
Set.fromList [q, r, (.~.) p],
Set.fromList [q, r, (.~.) r]]
p = atomic (P "p")
q = atomic (P "q")
r = atomic (P "r")
-- | Filtering out trivial disjuncts (in this guise, contradictory).
trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial lits =
let (pos, neg) = Set.partition positive lits in
(not . null . Set.intersection neg . Set.map (.~.)) pos
-- Example.
test33 :: Test
test33 = TestCase $ assertEqual "trivial" expected (Set.filter (not . trivial) (purednf id fm))
where expected :: Set (Set (LFormula Prop))
expected = Set.map (Set.map (convertToLiteral (error "test32") id)) $
Set.fromList [Set.fromList [p,(.~.) r],
Set.fromList [q,r,(.~.) p]]
fm :: PFormula Prop
fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
p = atomic (P "p") :: PFormula Prop
q = atomic (P "q") :: PFormula Prop
r = atomic (P "r") :: PFormula Prop
-- | With subsumption checking, done very naively (quadratic).
simpdnf :: (JustPropositional pf,
IsLiteral lit, JustLiteral lit, Ord lit
) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf ca fm =
foldPropositional (\_ _ _ -> go) (\_ -> go) tf (\_ -> go) fm
where
tf False = Set.empty
tf True = singleton Set.empty
go = let djs = Set.filter (not . trivial) (purednf ca (nnf fm)) in
Set.filter (\d -> not (setAny (\d' -> Set.isProperSubsetOf d' d) djs)) djs
-- | Mapping back to a formula.
dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
dnf fm = (list_disj . Set.toAscList . Set.map list_conj .
Set.map (Set.map (convertLiteral id :: LFormula (AtomOf pf) -> pf)) . simpdnf id) fm
-- Example. (p. 56)
test34 :: Test
test34 = TestCase $ assertEqual "dnf (p. 56)" expected input
where input = (prettyShow (dnf fm), tautology (Iff fm (dnf fm)))
expected = ("(p∧¬r)∨(q∧r∧¬p)",True)
fm = let (p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r")) in
(p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
-- | Conjunctive normal form (CNF) by essentially the same code. (p. 60)
purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
purecnf ca fm = Set.map (Set.map negate) (purednf ca (nnf ((.~.) fm)))
simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf ca fm =
foldPropositional (\_ _ _ -> go) (\_ -> go) tf (\_ -> go) fm
where
tf False = Set.empty
tf True = singleton Set.empty
go = let cjs = Set.filter (not . trivial) (purecnf ca fm) in
Set.filter (\c -> not (setAny (\c' -> Set.isProperSubsetOf c' c) cjs)) cjs
cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf
cnf_ ca = list_conj . Set.map (list_disj . Set.map (convertLiteral ca))
cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf' fm = (list_conj . Set.map list_disj . Set.map (Set.map (convertLiteral id :: LFormula (AtomOf pf) -> pf)) . simpcnf id) fm
-- Example. (p. 61)
test35 :: Test
test35 = TestCase $ assertEqual "cnf (p. 61)" expected input
where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))
expected = ("(p∨q)∧(p∨r)∧(¬p∨¬r)", True)
fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
[p, q, r] = [Atom (P "p"), Atom (P "q"), Atom (P "r")]
testProp :: Test
testProp = TestLabel "Prop" $
TestList [test00, test01, test02, test03, test04, {-test05,-}
test06, test07, test08, test09, test10,
test11, test12, test13, test14, test15,
test16, test17, test18, test19, test20,
test21, test22, test23, test24, test25,
test26, test27, test28, test29, test30,
test31, test32, test33, test34, test35]