module Folly.Formula(
Term, Formula,
fvt, subTerm, isVar, isConst, isFunc,
funcName, funcArgs, varName,
appendVarName, collectVars,
var, func, constant,
te, fa, pr, con, dis, neg, imp, bic, t, f,
vars, freeVars, isAtom, stripNegations,
generalize, subFormula,
applyToTerms,
literalArgs,
toPNF, toSkolemForm, skf,
toClausalForm,
matchingLiterals) where
import Control.Monad
import Data.Set as S
import Data.List as L
import Data.Map as M
data Term =
Constant String |
Var String |
Func String [Term]
deriving (Eq, Ord)
instance Show Term where
show = showTerm
showTerm :: Term -> String
showTerm (Constant name) = name
showTerm (Var name) = name
showTerm (Func name args) = name ++ "(" ++ (concat $ intersperse ", " $ L.map showTerm args) ++ ")"
isVar (Var _) = True
isVar _ = False
isFunc (Func _ _) = True
isFunc _ = False
isConst (Constant _) = True
isConst _ = False
funcName (Func n _) = n
funcArgs (Func _ a) = a
var n = Var n
func n args = case (L.take 3 n) == "skl" of
True -> error $ "Function names beginning with skl are reserved for skolemization"
False -> Func n args
constant n = Constant n
varName (Var n) = n
appendVarName :: String -> Term -> Term
appendVarName suffix (Var n) = Var (n ++ suffix)
appendVarName suffix (Func name args) = Func name $ L.map (appendVarName suffix) args
appendVarName _ t = t
fvt :: Term -> Set Term
fvt (Constant _) = S.empty
fvt (Var n) = S.fromList [(Var n)]
fvt (Func name args) = S.foldl S.union S.empty (S.fromList (L.map fvt args))
subTerm :: Map Term Term -> Term -> Term
subTerm _ (Constant name) = Constant name
subTerm sub (Func name args) = (Func name (L.map (subTerm sub) args))
subTerm sub (Var x) = case M.lookup (Var x) sub of
Just s -> s
Nothing -> (Var x)
data Formula =
T |
F |
P String [Term] |
B String Formula Formula |
N Formula |
Q String Term Formula
deriving (Eq, Ord)
instance Show Formula where
show = showFormula
showFormula :: Formula -> String
showFormula T = "True"
showFormula F = "False"
showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args) ++ "]"
showFormula (N f) = "~(" ++ show f ++ ")"
showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " " ++ show f2 ++ ")"
showFormula (Q q t f) = "(" ++ q ++ " " ++ show t ++ " . " ++ show f ++ ")"
applyToTerms :: Formula -> (Term -> Term) -> Formula
applyToTerms (P n args) f = P n $ L.map f args
applyToTerms (B n l r) f = B n (applyToTerms l f) (applyToTerms r f)
applyToTerms (Q n v l) f = Q n (f v) (applyToTerms l f)
applyToTerms (N l) f = N (applyToTerms l f)
collectVars :: Formula -> [Term]
collectVars (P _ args) = L.concatMap (\t -> if isVar t then [t] else []) args
collectVars (N f) = collectVars f
collectVars (B _ a b) = collectVars a ++ collectVars b
collectVars (Q _ v f) = v:(collectVars f)
collectVars _ = []
te :: Term -> Formula -> Formula
te v@(Var _) f = Q "E" v f
te t _ = error $ "Cannot quantify over non-variable term " ++ show t
fa :: Term -> Formula -> Formula
fa v@(Var _) f = Q "V" v f
fa t _ = error $ "Cannot quantify over non-variable term " ++ show t
pr name args = P name args
con f1 f2 = B "&" f1 f2
dis f1 f2 = B "|" f1 f2
imp f1 f2 = B "->" f1 f2
bic f1 f2 = B "<->" f1 f2
neg f = N f
t = T
f = F
vars :: Formula -> Set Term
vars T = S.empty
vars F = S.empty
vars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)
vars (B _ f1 f2) = S.union (vars f1) (vars f2)
vars (N f) = vars f
vars (Q _ v f) = S.insert v (vars f)
freeVars :: Formula -> Set Term
freeVars T = S.empty
freeVars F = S.empty
freeVars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)
freeVars (B _ f1 f2) = S.union (freeVars f1) (freeVars f2)
freeVars (N f) = freeVars f
freeVars (Q _ v f) = S.delete v (freeVars f)
isAtom :: Formula -> Bool
isAtom (P _ _) = True
isAtom _ = False
stripNegations :: Formula -> Formula
stripNegations (N t) = t
stripNegations f = f
literalArgs :: Formula -> [Term]
literalArgs (P _ a) = a
literalArgs (N (P _ a)) = a
literalArgs l = error $ show l ++ " is not a literal"
matchingLiterals :: Formula -> Formula -> Bool
matchingLiterals (P n1 _) (N (P n2 _)) = n1 == n2
matchingLiterals (N (P n1 _)) (P n2 _) = n1 == n2
matchingLiterals (P _ _) (P _ _) = False
matchingLiterals (N (P _ _)) (N (P _ _)) = False
matchingLiterals l1 l2 = error $ show l1 ++ " or " ++ show l2 ++ " is not a literal"
generalize :: Formula -> Formula
generalize f = applyList genFreeVar f
where
genFreeVar = L.map fa (S.toList (freeVars f))
applyList :: [a -> a] -> a -> a
applyList [] a = a
applyList (f:fs) a = applyList fs (f a)
variant :: Set Term -> Term -> Term
variant vars x@(Var n) = case S.member x vars of
True -> variant vars (Var (n ++ "'"))
False -> x
subFormula :: Map Term Term -> Formula -> Formula
subFormula subst (P name args) = P name $ L.map (subTerm subst) args
subFormula subst (B op f1 f2) = B op (subFormula subst f1) (subFormula subst f2)
subFormula subst (N f) = N (subFormula subst f)
subFormula subst q@(Q _ _ _) = subQuant subst q
subFormula subst f = f
subQuant :: Map Term Term -> Formula -> Formula
subQuant subst (Q n v f) = case (M.filter (== v) subst) == M.empty of
True -> Q n v (subFormula subst f)
False -> Q n vNew $ subFormula (M.insert v vNew subst) f
where
vNew = variant (freeVars (subFormula (M.delete v subst) f)) v
toPNF :: Formula -> Formula
toPNF = (transformFormula pullQuantifiers) .
(transformFormula simplifyFormula) .
(transformFormula pushNegation) .
(transformFormula elimVacuousQuantifiers) .
(transformFormula replaceImp) .
(transformFormula replaceBic)
pullQuantifiers f@(B "&" (Q "V" x p) (Q "V" y q)) = pullQ True True f fa con x y p q
pullQuantifiers f@(B "|" (Q "E" x p) (Q "E" y q)) = pullQ True True f te dis x y p q
pullQuantifiers f@(B "|" (Q "V" x p) q) = pullQ True False f fa dis x x p q
pullQuantifiers f@(B "|" p (Q "V" y q)) = pullQ False True f fa dis y y p q
pullQuantifiers f@(B "|" (Q "E" x p) q) = pullQ True False f te dis x x p q
pullQuantifiers f@(B "|" p (Q "E" y q)) = pullQ False True f te dis y y p q
pullQuantifiers f@(B "&" (Q "V" x p) q) = pullQ True False f fa con x x p q
pullQuantifiers f@(B "&" p (Q "V" y q)) = pullQ False True f fa con y y p q
pullQuantifiers f@(B "&" (Q "E" x p) q) = pullQ True False f te con x x p q
pullQuantifiers f@(B "&" p (Q "E" y q)) = pullQ False True f te con y y p q
pullQuantifiers f = f
pullQ :: Bool ->
Bool ->
Formula ->
(Term -> Formula -> Formula) ->
(Formula -> Formula -> Formula) ->
Term ->
Term ->
Formula ->
Formula ->
Formula
pullQ l r f quant op x y p q =
let z = variant (freeVars f) x in
let ps = if l then subFormula (M.singleton x z) p else p in
let qs = if r then subFormula (M.singleton y z) q else q in
quant z (pullQuantifiers $ op ps qs)
simplifyFormula (N (N f)) = f
simplifyFormula (N T) = F
simplifyFormula (N F) = T
simplifyFormula (B "|" T f) = T
simplifyFormula (B "|" f T) = T
simplifyFormula (B "|" F F) = F
simplifyFormula (B "&" F f) = F
simplifyFormula (B "&" f F) = F
simplifyFormula (B "&" T T) = T
simplifyFormula f = f
pushNegation (N (B "|" f1 f2)) = B "&" (pushNegation (N f1)) (pushNegation (N f2))
pushNegation (N (B "&" f1 f2)) = B "|" (pushNegation (N f1)) (pushNegation (N f2))
pushNegation (N (Q "V" x f)) = Q "E" x (pushNegation (N f))
pushNegation (N (Q "E" x f)) = Q "V" x (pushNegation (N f))
pushNegation f = f
elimVacuousQuantifiers (Q n x f) = case S.member x (freeVars f) of
True -> Q n x f
False -> f
elimVacuousQuantifiers f = f
replaceImp (B "->" f1 f2) = dis (neg f1) f2
replaceImp f = f
replaceBic (B "<->" f1 f2) = con (imp f1 f2) (imp f2 f1)
replaceBic f = f
transformFormula :: (Formula -> Formula) -> Formula -> Formula
transformFormula tran (B op f1 f2) = tran (B op (transformFormula tran f1) (transformFormula tran f2))
transformFormula tran (Q q x f) = tran (Q q x (transformFormula tran f))
transformFormula tran (N f) = tran (N (transformFormula tran f))
transformFormula tran f = tran f
toSkolemForm :: Formula -> Formula
toSkolemForm = skolemize . toPNF
skolemize :: Formula -> Formula
skolemize f = (transformFormula removeExistential) $ replaceVarsWithSkolemFuncs f
removeExistential :: Formula -> Formula
removeExistential (Q "E" v f) = f
removeExistential f = f
replaceVarsWithSkolemFuncs :: Formula -> Formula
replaceVarsWithSkolemFuncs f = subFormula varsToSkolemFuncs f
where
varsToSkolemFuncs = collectSkolemFuncs f 0 []
collectSkolemFuncs :: Formula -> Int -> [Term] -> Map Term Term
collectSkolemFuncs (Q "E" v f) n vars = M.insert v (skf n vars) (collectSkolemFuncs f (n+1) vars)
collectSkolemFuncs (Q "V" v f) n vars = collectSkolemFuncs f n (v:vars)
collectSkolemFuncs _ _ _ = M.empty
skf :: Int -> [Term] -> Term
skf n vars = Func ("skl" ++ show n) vars
toClausalForm :: Formula -> [[Formula]]
toClausalForm = splitClauses . removeUniversals . distributeDisjunction . toSkolemForm
distributeDisjunction :: (Formula) -> (Formula)
distributeDisjunction f = transformFormula distrDis f
distrDis :: (Formula) -> (Formula)
distrDis (B "|" (B "&" l r) f) = (B "&" (B "|" l f) (B "|" r f))
distrDis (B "|" f (B "&" l r)) = (B "&" (B "|" f l) (B "|" f r))
distrDis f = f
removeUniversals :: Formula -> Formula
removeUniversals (Q "V" v f) = removeUniversals f
removeUniversals f = f
splitClauses :: Formula -> [[Formula]]
splitClauses (B "&" l r) = (splitClauses l) ++ (splitClauses r)
splitClauses f = [splitDis f]
splitDis :: Formula -> [Formula]
splitDis (B "|" l r) = (splitDis l) ++ (splitDis r)
splitDis f = [f]