Library for representation of rules and term rewriting systems.
Author: Jan-Hendrik Matthes
Version: November 2016
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. |
rCons
:: (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
:: (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
:: [(Term a,Term a)] -> Term a -> Bool
Checks whether a term is reducible with some rule of the given term rewriting system. |
isPattern
:: [(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
:: [(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. |
A rule represented as a pair of terms and parameterized over the kind of function symbols, e.g., strings.
Type synonym: Rule a = (Term a,Term a)
A term rewriting system represented as a list of rules and parameterized over the kind of function symbols, e.g., strings.
Type synonym: TRS a = [Rule a]
Transforms a rule into a string representation. |
Transforms a term rewriting system into a string representation. |
Returns the root symbol (variable or constructor) of a rule.
|
Returns the maximum variable in a rule or |
Returns the minimum variable in a rule or |
Returns the maximum variable in a term rewriting system or |
Returns the minimum variable in a term rewriting system or |
Renames the variables in a rule by the given number. |
Renames the variables in every rule of a term rewriting system by the given number. |
Normalizes a rule by renaming all variables with an increasing order, starting from the minimum possible variable. |
Normalizes all rules in a term rewriting system by renaming all variables with an increasing order, starting from the minimum possible variable. |
Checks whether the first rule is a variant of the second rule. |
Checks whether a term rewriting system is left-linear. |
Checks whether a term rewriting system is left-normal. |
Checks whether a term is reducible with some rule of the given term rewriting system. |
Checks whether a term is a pattern, i.e., an root-reducible term where the argaccording to the given term rewriting system. |
Checks whether a term rewriting system is constructor-based. |
Checks whether the given argument position of a rule is demanded. Returns
|