tpdb-1.3.3: Data Type for Rewriting Systems

Safe HaskellSafe
LanguageHaskell98

TPDB.DP.Unify

Synopsis

Documentation

mgu :: (Ord v, Eq c) => Term v c -> Term v c -> Maybe (Map v (Term v c)) Source #

naive implementation (worst case exponential)

match :: (Ord v, Ord w, Eq c) => Term v c -> Term w c -> Maybe (Map v (Term w c)) Source #

will only bind variables in the left side

unifies :: (Ord v, Eq c) => Term v c -> Term v c -> Bool Source #

apply :: Ord k => Term k s -> Map k (Term k s) -> Term k s Source #

times :: Ord v => Substitution v c -> Substitution v c -> Substitution v c Source #