TPDB.DP.Unify

Documentation

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

naive implementation (worst case exponential)

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

will only bind variables in the left side

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

apply :: Ord v => Term v s -> Map v (Term v s) -> Term v s

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