Data.Rewriting.CriticalPair.Type

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.

Constructors

CP

Fields

• left :: Term f (Either v v')

  left reduct

• top :: Term f (Either v v')

  source

• right :: Term f (Either v v')

  right reduct

• leftRule :: Rule f v

  rule applied on left side

• leftPos :: Pos

  position of left rule application

• rightRule :: Rule f v'

  rule applied on right side

• subst :: Subst f (Either v v')

  common substitution of the rewrite steps