module Data.Logic.Harrison.Skolem
( simplify
, lsimplify
, nnf
, pnf
, functions
, SkolemT
, Skolem
, runSkolem
, runSkolemT
, specialize
, skolemize
, askolemize
, skolemNormalForm
, skolem
) where
import Control.Monad.Identity (Identity(runIdentity))
import Control.Monad.State (StateT(runStateT))
import Data.Logic.Classes.Atom (Atom)
import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..), binop)
import Data.Logic.Classes.Constants (Constants(fromBool, asBool), true, false)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(exists, for_all, foldFirstOrder), Quant(..), quant, toPropositional)
import Data.Logic.Classes.Formula (Formula(..))
import Data.Logic.Classes.Literal (Literal(foldLiteral))
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Propositional (PropositionalFormula(..))
import qualified Data.Logic.Classes.Skolem as C
import Data.Logic.Classes.Term (Term(..))
import Data.Logic.Classes.Variable (Variable(variant))
import Data.Logic.Harrison.FOL (fv, subst)
import Data.Logic.Harrison.Lib ((|=>))
import qualified Data.Map as Map
import qualified Data.Set as Set
simplify1 :: (FirstOrderFormula fof atom v,
Atom atom term v,
Term term v f) => fof -> fof
simplify1 fm =
foldFirstOrder qu co tf at fm
where
qu _ x p = if Set.member x (fv p) then fm else p
co ((:~:) p) = foldFirstOrder (\ _ _ _ -> fm) nco (fromBool . not) (\ _ -> fm) p
co (BinOp l op r) = simplifyBinop l op r
nco ((:~:) p) = p
nco _ = fm
tf = fromBool
at _ = fm
simplifyBinop :: forall p. (Constants p, Combinable p) => p -> BinOp -> p -> p
simplifyBinop 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 False, (:<=>:), Just False) -> true
(Just True, (:<=>:), _ ) -> r
(Just False, (:<=>:), _ ) -> (.~.) r
(_, (:<=>:), Just True ) -> l
(_, (:<=>:), Just False) -> (.~.) l
_ -> binop l op r
simplify :: (FirstOrderFormula fof atom v,
Atom atom term v,
Term term v f) => fof -> fof
simplify fm =
foldFirstOrder qu co tf at fm
where
qu op x fm' = simplify1 (quant op x (simplify fm'))
co ((:~:) fm') = simplify1 ((.~.) (simplify fm'))
co (BinOp fm1 op fm2) = simplify1 (binop (simplify fm1) op (simplify fm2))
tf = fromBool
at _ = fm
lsimplify :: Literal lit atom => lit -> lit
lsimplify fm = foldLiteral (lsimplify1 . (.~.) . lsimplify) fromBool (const fm) fm
lsimplify1 :: Literal lit atom => lit -> lit
lsimplify1 fm = foldLiteral (foldLiteral id (fromBool . not) (const fm)) fromBool (const fm) fm
nnf :: FirstOrderFormula formula atom v => formula -> formula
nnf fm =
foldFirstOrder nnfQuant nnfCombine (\ _ -> fm) (\ _ -> fm) fm
where
nnfQuant op v p = quant op v (nnf p)
nnfCombine ((:~:) p) = foldFirstOrder nnfNotQuant 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
nnfNotQuant Forall v p = exists v (nnf ((.~.) p))
nnfNotQuant Exists v p = for_all v (nnf ((.~.) p))
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
pullQuants :: forall formula atom v term f. (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) =>
formula -> formula
pullQuants fm =
foldFirstOrder (\ _ _ _ -> fm) pullQuantsCombine (\ _ -> fm) (\ _ -> fm) fm
where
getQuant = foldFirstOrder (\ op v f -> Just (op, v, f)) (\ _ -> Nothing) (\ _ -> Nothing) (\ _ -> Nothing)
pullQuantsCombine ((:~:) _) = fm
pullQuantsCombine (BinOp l op r) =
case (getQuant l, op, getQuant r) of
(Just (Forall, vl, l'), (:&:), Just (Forall, vr, r')) -> pullq True True fm for_all (.&.) vl vr l' r'
(Just (Exists, vl, l'), (:|:), Just (Exists, vr, r')) -> pullq True True fm exists (.|.) vl vr l' r'
(Just (Forall, vl, l'), (:&:), _) -> pullq True False fm for_all (.&.) vl vl l' r
(_, (:&:), Just (Forall, vr, r')) -> pullq False True fm for_all (.&.) vr vr l r'
(Just (Forall, vl, l'), (:|:), _) -> pullq True False fm for_all (.|.) vl vl l' r
(_, (:|:), Just (Forall, vr, r')) -> pullq False True fm for_all (.|.) vr vr l r'
(Just (Exists, vl, l'), (:&:), _) -> pullq True False fm exists (.&.) vl vl l' r
(_, (:&:), Just (Exists, vr, r')) -> pullq False True fm exists (.&.) vr vr l r'
(Just (Exists, vl, l'), (:|:), _) -> pullq True False fm exists (.|.) vl vl l' r
(_, (:|:), Just (Exists, vr, r')) -> pullq False True fm exists (.|.) vr vr l r'
_ -> fm
pullq :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) =>
Bool -> Bool
-> formula
-> (v -> formula -> formula)
-> (formula -> formula -> formula)
-> v -> v
-> formula -> formula
-> formula
pullq l r fm mkq op x y p q =
let z = variant x (fv fm)
p' = if l then subst (x |=> vt z) p else p
q' = if r then subst (y |=> vt z) q else q
fm' = pullQuants (op p' q') in
mkq z fm'
prenex :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) =>
formula -> formula
prenex fm =
foldFirstOrder qu co (\ _ -> fm) (\ _ -> fm) fm
where
qu op x p = quant op x (prenex p)
co (BinOp l (:&:) r) = pullQuants (prenex l .&. prenex r)
co (BinOp l (:|:) r) = pullQuants (prenex l .|. prenex r)
co _ = fm
pnf :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) => formula -> formula
pnf = prenex . nnf . simplify
functions :: forall formula atom f. (Formula formula atom, Ord f) => (atom -> Set.Set (f, Int)) -> formula -> Set.Set (f, Int)
functions fa fm = foldAtoms (\ s a -> Set.union s (fa a)) Set.empty fm
data SkolemState v term
= SkolemState
{ skolemCount :: Int
, univQuant :: [v]
}
newSkolemState :: SkolemState v term
newSkolemState
= SkolemState
{ skolemCount = 1
, univQuant = []
}
type SkolemT v term m = StateT (SkolemState v term) m
runSkolem :: SkolemT v term Identity a -> a
runSkolem = runIdentity . runSkolemT
type Skolem v term = StateT (SkolemState v term) Identity
runSkolemT :: Monad m => SkolemT v term m a -> m a
runSkolemT action = (runStateT action) newSkolemState >>= return . fst
skolem :: (Monad m,
FirstOrderFormula fof atom v,
Atom atom term v,
Term term v f) =>
fof -> SkolemT v term m fof
skolem fm =
foldFirstOrder qu co (return . fromBool) (return . atomic) fm
where
qu Exists y p =
do let xs = fv fm
let fx = fApp (C.toSkolem y) (map vt (Set.toAscList xs))
skolem (subst (Map.singleton y fx) p)
qu Forall x p = skolem p >>= return . for_all x
co (BinOp l (:&:) r) = skolem2 (.&.) l r
co (BinOp l (:|:) r) = skolem2 (.|.) l r
co _ = return fm
skolem2 :: (Monad m,
FirstOrderFormula fof atom v,
Atom atom term v,
Term term v f) =>
(fof -> fof -> fof) -> fof -> fof -> SkolemT v term m fof
skolem2 cons p q =
skolem p >>= \ p' ->
skolem q >>= \ q' ->
return (cons p' q')
askolemize :: forall m fof atom term v f.
(Monad m,
FirstOrderFormula fof atom v,
Atom atom term v,
Term term v f) =>
fof -> SkolemT v term m fof
askolemize = skolem . nnf . simplify
specialize :: forall fof atom v. FirstOrderFormula fof atom v => fof -> fof
specialize f =
foldFirstOrder q (\ _ -> f) (\ _ -> f) (\ _ -> f) f
where
q Forall _ f' = specialize f'
q _ _ _ = f
skolemize :: forall m fof atom term v f pf atom2. (Monad m,
FirstOrderFormula fof atom v,
PropositionalFormula pf atom2,
Atom atom term v,
Term term v f,
Eq pf) =>
(atom -> atom2) -> fof -> SkolemT v term m pf
skolemize ca fm = askolemize fm >>= return . (toPropositional ca :: fof -> pf) . specialize . pnf
skolemNormalForm :: (FirstOrderFormula fof atom v,
PropositionalFormula pf atom2,
Atom atom term v,
Term term v f,
Monad m, Ord fof, Eq pf) =>
(atom -> atom2) -> fof -> SkolemT v term m pf
skolemNormalForm = skolemize