Library for representation and computation of critical pairs.
Author: Jan-Hendrik Matthes
Version: August 2016
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
:: [(Term a,Term a)] -> [(Term a,Term a)]
Returns the critical pairs of a term rewriting system. |
isOrthogonal
:: [(Term a,Term a)] -> Bool
Checks whether a term rewriting system is orthogonal. |
isWeakOrthogonal
:: [(Term a,Term a)] -> Bool
Checks whether a term rewriting system is weak-orthogonal. |
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)
Transforms a critical pair into a string representation. |
Transforms a list of critical pairs into a string representation. |
Returns the critical pairs of a term rewriting system. |
Checks whether a term rewriting system is orthogonal. |
Checks whether a term rewriting system is weak-orthogonal. |