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.