term-rewriting-0.2: Term Rewriting Library

Safe HaskellNone
LanguageHaskell98

Data.Rewriting.CriticalPair

Contents

Synopsis

Documentation

data CP f v v' Source

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

Important operations

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

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'] Source

Determine all critical pairs for a pair of TRSs.

Reexported modules