Safe Haskell | None |
---|---|

Language | Haskell98 |

## 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.