# RSolve

[ library, logic, mit, program, unification ] [ Propose Tags ]

A general solver for equations

Versions [faq] 0.1.0.0, 0.1.0.1, 2.0.0.0 ChangeLog.md base (>=4.7 && <5), containers, lens, mtl, RSolve [details] MIT 2018, 2019 thautwarm thautwarm twshere@outlook.com Logic, Unification https://github.com/thautwarm/RSolve#readme https://github.com/thautwarm/RSolve/issues head: git clone https://github.com/thautwarm/RSolve by ice1000 at 2019-08-05T03:13:04Z NixOS:2.0.0.0 RSolve-exe 1026 total (47 in the last 30 days) 2.0 (votes: 1) [estimated by Bayesian average] λ λ λ Docs available Last success reported on 2019-08-05

## Modules

[Index] [Quick Jump]

• RSolve

#### Maintainer's Corner

For package maintainers and hackage trustees

[back to package description]

# 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 print  produces [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.empty  For 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"