TPDB.DP.Usable

Documentation

restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)

DANGER: this ignores the CE condition

usable :: (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c))

computes the least closed set of usable rules, cf. Def 4.5 http:cl-informatik.uibk.ac.atusersgriffpublicationsSternagel-Thiemann-RTA10.pdf

fixpoint :: Eq a => (a -> a) -> a -> a

required :: (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))

needed :: (Ord v, Ord c) => TRS v c -> Term v c -> [Rule (Term v c)]