Module Rewriting.CriticalPairs

Library for representation and computation of critical pairs.

Author: Jan-Hendrik Matthes

Version: August 2016

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.