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"