| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Rewriting.CriticalPair.Ops
Synopsis
- cps :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v'] -> [CP f v v']
- cpsIn :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v'] -> [CP f v v']
- cpsOut :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v'] -> [CP f v v']
- cps' :: (Ord v, Eq f) => [Rule f v] -> [CP f v v]
- cpsIn' :: (Ord v, Eq f) => [Rule f v] -> [CP f v v]
- cpsOut' :: (Ord v, Eq f) => [Rule f v] -> [CP f v v]
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
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.