PAKCS
Exported names: Imported modules:

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.