logic-classes-1.1: Data/Logic/Harrison/Prop.hs
{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}
{-# OPTIONS_GHC -Wall -Wwarn #-}
module Data.Logic.Harrison.Prop
( eval
, atoms
, onAllValuations
, truthTable
, tautology
, unsatisfiable
, satisfiable
, rawdnf
, purednf
, dnf
, trivial
, psimplify
, nnf
-- , simpdnf
, simpcnf
, positive
, negative
, negate
, distrib
, list_disj
, list_conj
-- previously unexported
, pSubst
, dual
, nenf
, mkLits
, allSatValuations
, dnf0
, cnf
) where
import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..), binop)
import Data.Logic.Classes.Constants (Constants(fromBool, true, false), asBool, ifElse)
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Propositional
import Data.Logic.Harrison.Formulas.Propositional (atom_union, on_atoms)
import Data.Logic.Harrison.Lib (fpf, allpairs, setAny)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Prelude hiding (negate)
-- -------------------------------------------------------------------------
-- Parsing of propositional formulas.
-- -------------------------------------------------------------------------
{-
let parse_propvar vs inp =
match inp with
p::oinp when p /= "(" -> Atom(P(p)),oinp
| _ -> failwith "parse_propvar";;
let parse_prop_formula = make_parser
(parse_formula ((fun _ _ -> failwith ""),parse_propvar) []);;
-}
-- -------------------------------------------------------------------------
-- Set this up as default for quotations.
-- -------------------------------------------------------------------------
{-
let default_parser = parse_prop_formula;;
-}
-- -------------------------------------------------------------------------
-- Printer.
-- -------------------------------------------------------------------------
{-
let print_propvar prec p = print_string(pname p);;
let print_prop_formula = print_qformula print_propvar;;
#install_printer print_prop_formula;;
-}
-- -------------------------------------------------------------------------
-- Interpretation of formulas.
-- -------------------------------------------------------------------------
eval :: PropositionalFormula formula atomic => formula -> (atomic -> Bool) -> Bool
eval fm v =
foldPropositional co id at fm
where
co ((:~:) p) = not (eval p v)
co (BinOp p (:&:) q) = eval p v && eval q v
co (BinOp p (:|:) q) = eval p v || eval q v
co (BinOp p (:=>:) q) = not (eval p v) || eval q v
co (BinOp p (:<=>:) q) = eval p v == eval q v
at x = v x
{-
START_INTERACTIVE;;
eval <<p /\ q ==> q /\ r>>
(function P"p" -> true | P"q" -> false | P"r" -> true);;
eval <<p /\ q ==> q /\ r>>
(function P"p" -> true | P"q" -> true | P"r" -> false);;
END_INTERACTIVE;;
-}
-- -------------------------------------------------------------------------
-- Return the set of propositional variables in a formula.
-- -------------------------------------------------------------------------
atoms :: Ord atomic => PropositionalFormula formula atomic => formula -> Set.Set atomic
atoms = atom_union Set.singleton
-- -------------------------------------------------------------------------
-- Code to print out truth tables.
-- -------------------------------------------------------------------------
onAllValuations :: (Eq a) =>
(r -> r -> r) -- ^ Combine function for result type
-> ((a -> Bool) -> r) -- ^ The substitution function
-> (a -> Bool) -- ^ The default valuation function for atoms not in ps
-> Set.Set a -- ^ The variables to vary
-> r
onAllValuations _ subfn v ps | Set.null ps = subfn v
onAllValuations append subfn v ps =
case Set.deleteFindMin ps of
(p, ps') -> append -- Do the valuations of the remaining variables with set to false
(onAllValuations append subfn (\ q -> if q == p then False else v q) ps')
-- Do the valuations of the remaining variables with set to true
(onAllValuations append subfn (\ q -> if q == p then True else v q) ps')
type TruthTableRow a = ([(a, Bool)], Bool)
truthTable :: forall formula atomic. (PropositionalFormula formula atomic, Eq atomic, Ord atomic) =>
formula -> [TruthTableRow atomic]
truthTable fm =
onAllValuations (++) mkRow (const False) ats
where
mkRow :: (atomic -> Bool) -- The current variable assignment
-> [TruthTableRow atomic] -- The variable assignments and the formula value
mkRow v = [(map (\ a -> (a, v a)) (Set.toList ats), eval fm v)]
ats = atoms fm
-- -------------------------------------------------------------------------
-- Recognizing tautologies.
-- -------------------------------------------------------------------------
tautology :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
tautology fm = onAllValuations (&&) (eval fm) (const False) (atoms fm)
-- -------------------------------------------------------------------------
-- Related concepts.
-- -------------------------------------------------------------------------
unsatisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
unsatisfiable fm = tautology ((.~.) fm)
satisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool
satisfiable = not . unsatisfiable
-- -------------------------------------------------------------------------
-- Substitution operation.
-- -------------------------------------------------------------------------
-- pSubst :: Ord a => Map.Map a (Formula a) -> Formula a -> Formula a
pSubst :: (PropositionalFormula formula atomic, Ord atomic) => Map.Map atomic formula -> formula -> formula
pSubst subfn fm = on_atoms (\ p -> maybe (atomic p) id (fpf subfn p)) fm
-- -------------------------------------------------------------------------
-- Dualization.
-- -------------------------------------------------------------------------
dual :: forall formula atomic. (PropositionalFormula formula atomic) => formula -> formula
dual fm =
foldPropositional co (fromBool . not) at fm
where
co ((:~:) _) = fm
co (BinOp p (:&:) q) = dual p .|. dual q
co (BinOp p (:|:) q) = dual p .&. dual q
co _ = error "dual: Formula involves connectives ==> or <=>";;
at = atomic
-- -------------------------------------------------------------------------
-- Routine simplification.
-- -------------------------------------------------------------------------
psimplify1 :: (PropositionalFormula r a, Eq r) => r -> r
psimplify1 fm =
foldPropositional simplifyCombine (\ _ -> fm) (\ _ -> fm) fm
where
simplifyCombine ((:~:) fm') = foldPropositional simplifyNotCombine (fromBool . not) (\ _ -> fm) fm'
simplifyCombine (BinOp l op r) =
case (asBool l, op, asBool r) of
(Just True, (:&:), _ ) -> r
(Just False, (:&:), _ ) -> false
(_, (:&:), Just True ) -> l
(_, (:&:), Just False) -> false
(Just True, (:|:), _ ) -> true
(Just False, (:|:), _ ) -> r
(_, (:|:), Just True ) -> true
(_, (:|:), Just False) -> l
(Just True, (:=>:), _ ) -> r
(Just False, (:=>:), _ ) -> true
(_, (:=>:), Just True ) -> true
(_, (:=>:), Just False) -> (.~.) l
(Just True, (:<=>:), _ ) -> r
(Just False, (:<=>:), _ ) -> (.~.) r
(_, (:<=>:), Just True ) -> l
(_, (:<=>:), Just False) -> (.~.) l
_ -> fm
simplifyNotCombine ((:~:) p) = p
simplifyNotCombine _ = fm
psimplify :: forall formula atomic. (PropositionalFormula formula atomic, Eq formula) => formula -> formula
psimplify fm =
foldPropositional c (\ _ -> fm) (\ _ -> fm) fm
where
c :: Combination formula -> formula
c ((:~:) p) = psimplify1 ((.~.) (psimplify p))
c (BinOp p op q) = psimplify1 (binop (psimplify p) op (psimplify q))
-- -------------------------------------------------------------------------
-- Some operations on literals.
-- -------------------------------------------------------------------------
negative :: PropositionalFormula formula atomic => formula -> Bool
negative lit =
foldPropositional c tf a lit
where
c ((:~:) _) = True
c _ = False
tf = not
a _ = False
positive :: PropositionalFormula formula atomic => formula -> Bool
positive = not . negative
negate :: PropositionalFormula formula atomic => formula -> formula
negate lit =
foldPropositional c (fromBool . not) a lit
where
c ((:~:) p) = p
c _ = (.~.) lit
a _ = (.~.) lit
-- -------------------------------------------------------------------------
-- Negation normal form.
-- -------------------------------------------------------------------------
nnf' :: PropositionalFormula formula atomic => formula -> formula
nnf' fm =
foldPropositional nnfCombine (\ _ -> fm) (\ _ -> fm) fm
where
nnfCombine ((:~:) p) = foldPropositional nnfNotCombine (fromBool . not) (\ _ -> fm) p
nnfCombine (BinOp p (:=>:) q) = nnf' ((.~.) p) .|. (nnf' q)
nnfCombine (BinOp p (:<=>:) q) = (nnf' p .&. nnf' q) .|. (nnf' ((.~.) p) .&. nnf' ((.~.) q))
nnfCombine (BinOp p (:&:) q) = nnf' p .&. nnf' q
nnfCombine (BinOp p (:|:) q) = nnf' p .|. nnf' q
nnfNotCombine ((:~:) p) = nnf' p
nnfNotCombine (BinOp p (:&:) q) = nnf' ((.~.) p) .|. nnf' ((.~.) q)
nnfNotCombine (BinOp p (:|:) q) = nnf' ((.~.) p) .&. nnf' ((.~.) q)
nnfNotCombine (BinOp p (:=>:) q) = nnf' p .&. nnf' ((.~.) q)
nnfNotCombine (BinOp p (:<=>:) q) = (nnf' p .&. nnf' ((.~.) q)) .|. nnf' ((.~.) p) .&. nnf' q
-- -------------------------------------------------------------------------
-- Roll in simplification.
-- -------------------------------------------------------------------------
nnf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula
nnf = nnf' . psimplify
-- -------------------------------------------------------------------------
-- Simple negation-pushing when we don't care to distinguish occurrences.
-- -------------------------------------------------------------------------
nenf' :: PropositionalFormula formula atomic => formula -> formula
nenf' fm =
foldPropositional nenfCombine (\ _ -> fm) (\ _ -> fm) fm
where
nenfCombine ((:~:) p) = foldPropositional nenfNotCombine (\ _ -> fm) (\ _ -> fm) p
nenfCombine (BinOp p (:&:) q) = nenf' p .|. nenf' q
nenfCombine (BinOp p (:|:) q) = nenf' p .|. nenf' q
nenfCombine (BinOp p (:=>:) q) = nenf' ((.~.) p) .|. nenf' q
nenfCombine (BinOp p (:<=>:) q) = nenf' p .<=>. nenf' q
nenfNotCombine ((:~:) p) = p
nenfNotCombine (BinOp p (:&:) q) = nenf' ((.~.) p) .|. nenf' ((.~.) q)
nenfNotCombine (BinOp p (:|:) q) = nenf' ((.~.) p) .&. nenf' ((.~.) q)
nenfNotCombine (BinOp p (:=>:) q) = nenf' p .&. nenf' ((.~.) q)
nenfNotCombine (BinOp p (:<=>:) q) = nenf' p .<=>. nenf' ((.~.) q) -- really? how is this asymmetrical?
nenf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula
nenf = nenf' . psimplify
-- -------------------------------------------------------------------------
-- Disjunctive normal form (DNF) via truth tables.
-- -------------------------------------------------------------------------
list_conj :: (PropositionalFormula formula atomic, Ord formula) => Set.Set formula -> formula
list_conj l = maybe true (\ (x, xs) -> Set.fold (.&.) x xs) (Set.minView l)
list_disj :: PropositionalFormula formula atomic => Set.Set formula -> formula
list_disj l = maybe false (\ (x, xs) -> Set.fold (.|.) x xs) (Set.minView l)
mkLits :: (PropositionalFormula formula atomic, Ord formula) =>
Set.Set formula -> (atomic -> Bool) -> formula
mkLits pvs v = list_conj (Set.map (\ p -> if eval p v then p else (.~.) p) pvs)
allSatValuations :: Eq a => ((a -> Bool) -> Bool) -> (a -> Bool) -> Set.Set a -> [a -> Bool]
allSatValuations subfn v pvs =
case Set.minView pvs of
Nothing -> if subfn v then [v] else []
Just (p, ps) -> (allSatValuations subfn (\ q -> if q == p then False else v p) ps) ++
(allSatValuations subfn (\ q -> if q == p then True else v p) ps)
dnf0 :: forall formula atomic. (PropositionalFormula formula atomic, Ord atomic, Ord formula) => formula -> formula
dnf0 fm =
list_disj (Set.fromList (map (mkLits (Set.map atomic pvs)) satvals))
where
satvals = allSatValuations (eval fm) (const False) pvs
pvs = atoms fm
-- -------------------------------------------------------------------------
-- DNF via distribution.
-- -------------------------------------------------------------------------
distrib :: PropositionalFormula formula atomic => formula -> formula
distrib fm =
foldPropositional c tf a fm
where
c (BinOp p (:&:) s) =
foldPropositional c' tf a s
where c' (BinOp q (:|:) r) = distrib (p .&. q) .|. distrib (p .&. r)
c' _ =
foldPropositional c'' tf a p
where c'' (BinOp q (:|:) r) = distrib (q .&. s) .|. distrib (r .&. s)
c'' _ = fm
c _ = fm
tf _ = fm
a _ = fm
rawdnf :: PropositionalFormula formula atomic => formula -> formula
rawdnf fm =
foldPropositional c tf a fm
where
c (BinOp p (:&:) q) = distrib (rawdnf p .&. rawdnf q)
c (BinOp p (:|:) q) = rawdnf p .|. rawdnf q
c _ = fm
tf _ = fm
a _ = fm
-- -------------------------------------------------------------------------
-- A version using a list representation.
-- -------------------------------------------------------------------------
distrib' :: (Eq formula, Ord formula) => Set.Set (Set.Set formula) -> Set.Set (Set.Set formula) -> Set.Set (Set.Set formula)
distrib' s1 s2 = allpairs (Set.union) s1 s2
purednf :: (PropositionalFormula formula atomic, Ord formula) => formula -> Set.Set (Set.Set formula)
purednf fm =
foldPropositional c tf a fm
where
c (BinOp p (:&:) q) = distrib' (purednf p) (purednf q)
c (BinOp p (:|:) q) = Set.union (purednf p) (purednf q)
c _ = Set.singleton (Set.singleton fm)
tf _ = Set.singleton (Set.singleton fm)
a _ = Set.singleton (Set.singleton fm)
-- -------------------------------------------------------------------------
-- Filtering out trivial disjuncts (in this guise, contradictory).
-- -------------------------------------------------------------------------
trivial :: (PropositionalFormula formula atomic, Ord formula) => Set.Set formula -> Bool
trivial lits =
not . Set.null $ Set.intersection neg (Set.map (.~.) pos)
where (pos, neg) = Set.partition positive lits
-- -------------------------------------------------------------------------
-- With subsumption checking, done very naively (quadratic).
-- -------------------------------------------------------------------------
simpdnf :: forall formula atomic. (PropositionalFormula formula atomic, Eq formula, Ord formula) => formula -> Set.Set (Set.Set formula)
simpdnf fm =
foldPropositional c tf a fm
where
c :: Combination formula -> Set.Set (Set.Set formula)
c _ = Set.filter (\ d -> not (setAny (\ d' -> Set.isProperSubsetOf d' d) djs)) djs
where djs = Set.filter (not . trivial) (purednf (nnf fm))
tf = ifElse (Set.singleton Set.empty) Set.empty
a :: atomic -> Set.Set (Set.Set formula)
a _ = Set.singleton (Set.singleton fm)
-- -------------------------------------------------------------------------
-- Mapping back to a formula.
-- -------------------------------------------------------------------------
dnf :: (PropositionalFormula formula atomic, Ord formula) => formula -> formula
dnf fm = list_disj (Set.map list_conj (simpdnf fm))
-- -------------------------------------------------------------------------
-- Conjunctive normal form (CNF) by essentially the same code.
-- -------------------------------------------------------------------------
purecnf :: (PropositionalFormula formula atomic, Ord formula) => formula -> Set.Set (Set.Set formula)
purecnf fm = Set.map (Set.map (psimplify . (.~.))) (purednf (nnf ((.~.) fm)))
simpcnf :: (PropositionalFormula formula atomic, Ord formula) =>
formula -> Set.Set (Set.Set formula)
simpcnf fm =
foldPropositional c tf a fm
where
tf = ifElse Set.empty (Set.singleton Set.empty)
-- Discard any clause that is the proper subset of another clause
c _ = Set.filter keep cjs
keep x = not (setAny (`Set.isProperSubsetOf` x) cjs)
cjs = Set.filter (not . trivial) (purecnf fm)
a _ = Set.singleton (Set.singleton fm)
cnf :: (PropositionalFormula formula atomic, Ord formula) => formula -> formula
cnf fm = list_conj (Set.map list_disj (simpcnf fm))