Module Rewriting.Rules

showRule :: (a -> String) -> (Term a,Term a) -> String   

Transforms a rule into a string representation.

showTRS :: (a -> String) -> [(Term a,Term a)] -> String   

Transforms a term rewriting system into a string representation.

rRoot :: (Term a,Term a) -> Either Int a   

Returns the root symbol (variable or constructor) of a rule.

Further infos:

• solution complete, i.e., able to compute all solutions

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

Returns a list without duplicates of all constructors in a rule.

rVars :: (Term a,Term a) -> [Int]   

Returns a list without duplicates of all variables in a rule.

maxVarInRule :: (Term a,Term a) -> Maybe Int   

Returns the maximum variable in a rule or Nothing if no variable exists.

minVarInRule :: (Term a,Term a) -> Maybe Int   

Returns the minimum variable in a rule or Nothing if no variable exists.

maxVarInTRS :: [(Term a,Term a)] -> Maybe Int   

Returns the maximum variable in a term rewriting system or Nothing if no variable exists.

minVarInTRS :: [(Term a,Term a)] -> Maybe Int   

Returns the minimum variable in a term rewriting system or Nothing if no variable exists.

renameRuleVars :: Int -> (Term a,Term a) -> (Term a,Term a)   

Renames the variables in a rule by the given number.

renameTRSVars :: Int -> [(Term a,Term a)] -> [(Term a,Term a)]   

Renames the variables in every rule of a term rewriting system by the given number.

normalizeRule :: (Term a,Term a) -> (Term a,Term a)   

Normalizes a rule by renaming all variables with an increasing order, starting from the minimum possible variable.

normalizeTRS :: [(Term a,Term a)] -> [(Term a,Term a)]   

Normalizes all rules in a term rewriting system by renaming all variables with an increasing order, starting from the minimum possible variable.

isVariantOf :: Eq a => (Term a,Term a) -> (Term a,Term a) -> Bool   

Checks whether the first rule is a variant of the second rule.

isLeftLinear :: [(Term a,Term a)] -> Bool   

Checks whether a term rewriting system is left-linear.

isLeftNormal :: [(Term a,Term a)] -> Bool   

Checks whether a term rewriting system is left-normal.

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

Checks whether a term is reducible with some rule of the given term rewriting system.

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

Checks whether a term is a pattern, i.e., an root-reducible term where the argaccording to the given term rewriting system.

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

Checks whether a term rewriting system is constructor-based.

isDemandedAt :: Int -> (Term a,Term a) -> Bool   

Checks whether the given argument position of a rule is demanded. Returns True if the corresponding argument term is a constructor term.