# Module Rewriting.CriticalPairs

Library for representation and computation of critical pairs.

Author: Jan-Hendrik Matthes

Version: February 2020

## Summary of exported operations:

 ```showCPair :: (a -> String) -> (Term a,Term a) -> String``` Transforms a critical pair into a string representation. ```showCPairs :: (a -> String) -> [(Term a,Term a)] -> String``` Transforms a list of critical pairs into a string representation. ```cPairs :: Eq a => [(Term a,Term a)] -> [(Term a,Term a)]``` Returns the critical pairs of a term rewriting system. ```isOrthogonal :: Eq a => [(Term a,Term a)] -> Bool``` Checks whether a term rewriting system is orthogonal. ```isWeakOrthogonal :: Eq a => [(Term a,Term a)] -> Bool``` Checks whether a term rewriting system is weak-orthogonal.

## Exported datatypes:

CPair

A critical pair represented as a pair of terms and parameterized over the kind of function symbols, e.g., strings.

Type synonym: `CPair a = (Term a,Term a)`

## Exported operations:

 ```showCPair :: (a -> String) -> (Term a,Term a) -> String``` Transforms a critical pair into a string representation.
 ```showCPairs :: (a -> String) -> [(Term a,Term a)] -> String``` Transforms a list of critical pairs into a string representation.
 ```cPairs :: Eq a => [(Term a,Term a)] -> [(Term a,Term a)]``` Returns the critical pairs of a term rewriting system.
 ```isOrthogonal :: Eq a => [(Term a,Term a)] -> Bool``` Checks whether a term rewriting system is orthogonal.
 ```isWeakOrthogonal :: Eq a => [(Term a,Term a)] -> Bool``` Checks whether a term rewriting system is weak-orthogonal.