PAKCS
Exported names: Imported modules:

Module Rewriting.Rules

Library for representation of rules and term rewriting systems.

Author: Jan-Hendrik Matthes

Version: February 2020

Summary of exported operations:

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 :: 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., a root-reducible term according 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.

Exported datatypes:

Rule

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)

TRS

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]

Exported operations:

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 :: 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., a root-reducible term according 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.