term-rewriting-0.4.0.1: Term Rewriting Library

Data.Rewriting.CriticalPair.Ops

Synopsis

# pairs of rewrite systems

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.

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

Determine all inner critical pairs for a pair of TRSs.

A critical pair is inner if the left rewrite step is not a root step.

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

Determine outer critical pairs for a pair of TRSs.

A critical pair is outer if the left rewrite step is a root step.

# single rewrite systems

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.

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

Determine all inner critical pairs of a single TRS with itself.

The result of cpsIn' trs differs from cpsIn trs trs in that overlaps of a rule with itself are returned once, not twice.

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

Determine all outer critical pairs of a single TRS with itself.

The result of cpsOut' trs differs from cpsOut trs trs in two aspects:

• The trivial overlaps of rules with themselves are omitted.
• Symmetry is taken into account: Overlaps between distinct rules are returned once instead of twice.