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  Deterministic 
Transforms a critical pair into a string representation.
showCPairs :: (a -> String) -> [(Term a,Term a)] -> String  Deterministic 
Transforms a list of critical pairs into a string representation.
cPairs :: Eq a => [(Term a,Term a)] -> [(Term a,Term a)]  Deterministic 
Returns the critical pairs of a term rewriting system.
isOrthogonal :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 
Checks whether a term rewriting system is orthogonal.
isWeakOrthogonal :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 
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  Deterministic 

Transforms a critical pair into a string representation.

showCPairs :: (a -> String) -> [(Term a,Term a)] -> String  Deterministic 

Transforms a list of critical pairs into a string representation.

cPairs :: Eq a => [(Term a,Term a)] -> [(Term a,Term a)]  Deterministic 

Returns the critical pairs of a term rewriting system.

isOrthogonal :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 

Checks whether a term rewriting system is orthogonal.

isWeakOrthogonal :: Eq a => [(Term a,Term a)] -> Bool  Deterministic 

Checks whether a term rewriting system is weak-orthogonal.