RSolve

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

A general solver for equations


[Skip to Readme]
Versions [faq] 0.1.0.0, 0.1.0.1, 2.0.0.0
Change log ChangeLog.md
Dependencies base (>=4.7 && <5), containers, lens, mtl, RSolve [details]
License MIT
Copyright 2018, 2019 thautwarm
Author thautwarm
Maintainer twshere@outlook.com
Category Logic, Unification
Home page https://github.com/thautwarm/RSolve#readme
Bug tracker https://github.com/thautwarm/RSolve/issues
Source repo head: git clone https://github.com/thautwarm/RSolve
Uploaded by ice1000 at 2019-08-05T03:13:04Z
Distributions NixOS:2.0.0.0
Executables RSolve-exe
Downloads 1028 total (32 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2019-08-05 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for RSolve-2.0.0.0

[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"