RSolve
NOTE: NO LONGER for general logic programming, this package is now dedicated for the simple propositional logic.
The README is going to get updated.
Propositional Logic
RSolve uses disjunctive normal form to solve logic problems.
This disjunctive normal form works naturally with the logic problems where the atom formulas can be generalized to an arbitrary equation in the problem domain by introducing a problem domain specific solver. A vivid
example can be found at RSolve.HM, where
I implemented an extended algo-W for HM unification.
To take advantage of RSolve, we should implement 2 classes:
-
AtomF, which stands for the atom formula. -
CtxSolver, which stands for the way to solve a bunch of atom formulas.
However we might not need to a solver sometimes:
data Value = A | B | C | D
deriving (Show, Eq, Ord, Enum)
data At = At {at_l :: String, at_r :: Value}
deriving (Show, Eq, Ord)
instance AtomF At where
notA At {at_l = lhs, at_r = rhs} =
let wholeSet = enumFrom (toEnum 0) :: [Value]
contrasts = delete rhs wholeSet
in [At {at_l = lhs, at_r = rhs'} | rhs' <- contrasts]
infix 6 <==>
s <==> v = Atom $ At s v
equations = do
assert $ "a" <==> A :||: "a" <==> B
assert $ Not ("a" <==> A)
main =
let equationGroups = unionEquations equations
in forM equationGroups printproduces
[At {at_l = "a", at_r = A},At {at_l = "a", at_r = B}]
[At {at_l = "a", at_r = A},At {at_l = "a", at_r = C}]
[At {at_l = "a", at_r = A},At {at_l = "a", at_r = D}]
[At {at_l = "a", at_r = B}]
[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C}]
[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C},At {at_l = "a", at_r = D}]
[At {at_l = "a", at_r = B},At {at_l = "a", at_r = D}]According to the property of the problem domain, we can figure out that
only the 4-th(1-based indexing) equation group
[At {at_l = "a", at_r = B}]
will produce a feasible solution because symbol a can
only hold one value.
When do we need a solver? For instance, type checking&inference.
In this case, we need type checking environments to represent the checking states:
data TCEnv = TCEnv {
_noms :: M.Map Int T -- nominal type ids
, _tvars :: M.Map Int T -- type variables
, _neqs :: S.Set (T, T) -- negation constraints
}
deriving (Show)
emptyTCEnv = TCEnv M.empty M.empty S.emptyFor sure we also need to represent the type:
data T
= TVar Int
| TFresh String
| T :-> T
| T :* T -- tuple
| TForall (S.Set String) T
| TApp T T -- type application
| TNom Int -- nominal type index
deriving (Eq, Ord)Then the atom formula of HM unification is:
data Unif
= Unif {
lhs :: T
, rhs :: T
, neq :: Bool -- lhs /= rhs or lhs == rhs?
}
deriving (Eq, Ord)We then need to implement this:
-- class AtomF a => CtxSolver s a where
-- solve :: a -> MS s ()
prune :: T -> MS TCEnv T -- MS: MultiState
instance CtxSolver TCEnv Unif where
solver = ...Finally we got this:
infixl 6 <=>
a <=> b = Atom $ Unif {lhs=a, rhs=b, neq=False}
solu = do
a <- newTVar
b <- newTVar
c <- newTVar
d <- newTVar
let [eqs] = unionEquations $
do
assert $ TVar a <=> TForall (S.fromList ["s"]) ((TFresh "s") :-> (TFresh "s" :* TFresh "s"))
assert $ TVar a <=> (TVar b :-> (TVar c :* TVar d))
assert $ TVar d <=> TNom 1
-- return eqs
forM_ eqs solve
return eqs
a <- prune $ TVar a
b <- prune $ TVar b
c <- prune $ TVar c
return (a, b, c)
test :: Eq a => String -> a -> a -> IO ()
test msg a b
| a == b = return ()
| otherwise = print msg
main = do
forM (unionEquations equations) print
let (a, b, c):_ = map fst $ runMS solu emptyTCEnv
test "1 failed" (show a) "@t1 -> @t1 * @t1"
test "2 failed" (show b) "@t1"
test "3 failed" (show c) "@t1"