Data.Rewriting.CriticalPair

Documentation

data CP f v v'

A critical pair. Critical pairs (should) have the following properties:

top   == Context.ofTerm top pos (Term.map Left id (Rule.lhs leftRule))
left  == Context.ofTerm top pos (Term.map Left id (Rule.rhs leftRule))
top   == Substitution.apply subst (Term.map Right id (Rule.lhs rightRule))
right == Substitution.apply subst (Term.map Right id (Rule.rhs rightRule))

Furthermore, pos is a non-variable position of (lhs rightRule) and subst is a most general substitution with these properties.

Important operations

cps' :: (Ord v, Eq f) => [Rule f v] -> [CP f v v]

Determine all critical pairs of a single TRS with itself.

Unlike cps, cps' takes symmetries into account. See cpsIn' and cpsOut' for details.

cps :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v'] -> [CP f v v']

Determine all critical pairs for a pair of TRSs.

Reexported modules

module Data.Rewriting.CriticalPair.Type

module Data.Rewriting.CriticalPair.Ops