Module Rewriting.Term

Library for representation of first-order terms.

This library is the basis of other libraries for the manipulation of first-order terms, e.g., unification of terms. Therefore, this library also defines other structures, like term equations.

Author: Jan-Hendrik Matthes

Version: October 2020

Summary of exported operations:

showVarIdx :: Int -> String  Deterministic 
Transforms a variable into a string representation.
showTerm :: (a -> String) -> Term a -> String  Deterministic 
Transforms a term into a string representation.
showTermEq :: (a -> String) -> (Term a,Term a) -> String  Deterministic 
Transforms a term equation into a string representation.
showTermEqs :: (a -> String) -> [(Term a,Term a)] -> String  Deterministic 
Transforms a list of term equations into a string representation.
tConst :: a -> Term a  Deterministic 
Returns a term with the given constructor and no argument terms.
tOp :: Term a -> a -> Term a -> Term a  Deterministic 
Returns an infix operator term with the given constructor and the given left and right argument term.
tRoot :: Term a -> Either Int a  Deterministic 
Returns the root symbol (variable or constructor) of a term.
tCons :: Eq a => Term a -> [a]  Deterministic 
Returns a list without duplicates of all constructors in a term.
tConsAll :: Term a -> [a]  Deterministic 
Returns a list of all constructors in a term.
tVars :: Term a -> [Int]  Deterministic 
Returns a list without duplicates of all variables in a term.
tVarsAll :: Term a -> [Int]  Deterministic 
Returns a list of all variables in a term.
isConsTerm :: Term a -> Bool  Deterministic 
Checks whether a term is a constructor term.
isVarTerm :: Term a -> Bool  Deterministic 
Checks whether a term is a variable term.
isGround :: Term a -> Bool  Deterministic 
Checks whether a term is a ground term (contains no variables).
isLinear :: Term a -> Bool  Deterministic 
Checks whether a term is linear (contains no variable more than once).
isNormal :: Term a -> Bool  Deterministic 
Checks whether a term is normal (behind a variable is not a constructor).
maxVarInTerm :: Term a -> Maybe Int  Deterministic 
Returns the maximum variable in a term or Nothing if no variable exists.
minVarInTerm :: Term a -> Maybe Int  Deterministic 
Returns the minimum variable in a term or Nothing if no variable exists.
normalizeTerm :: Term a -> Term a  Deterministic 
Normalizes a term by renaming all variables with an increasing order, starting from the minimum possible variable.
renameTermVars :: Int -> Term a -> Term a  Deterministic 
Renames the variables in a term by the given number.
mapTerm :: (a -> b) -> Term a -> Term b  Deterministic 
Transforms a term by applying a transformation on all constructors.
eqConsPattern :: Eq a => Term a -> Term a -> Bool  Deterministic 
Checks whether the constructor pattern of the first term is equal to the constructor pattern of the second term.

Exported datatypes:

VarIdx

A variable represented as an integer greater than or equal to zero.

Type synonym: VarIdx = Int

Term

Representation of a first-order term, parameterized over the kind of function symbols, e.g., strings.

Constructors:

  • TermVar :: VarIdx -> Term a : The variable term with variable v.
  • TermCons :: a -> [Term a] -> Term a : The constructor term with constructor c and argument terms ts.
TermEq

A term equation represented as a pair of terms and parameterized over the kind of function symbols, e.g., strings.

Type synonym: TermEq a = (Term a,Term a)

TermEqs

Multiple term equations represented as a list of term equations and parameterized over the kind of function symbols, e.g., strings.

Type synonym: TermEqs a = [TermEq a]

Exported operations:

showVarIdx :: Int -> String  Deterministic 

Transforms a variable into a string representation.

showTerm :: (a -> String) -> Term a -> String  Deterministic 

Transforms a term into a string representation.

showTermEq :: (a -> String) -> (Term a,Term a) -> String  Deterministic 

Transforms a term equation into a string representation.

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

Transforms a list of term equations into a string representation.

tConst :: a -> Term a  Deterministic 

Returns a term with the given constructor and no argument terms.

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

tOp :: Term a -> a -> Term a -> Term a  Deterministic 

Returns an infix operator term with the given constructor and the given left and right argument term.

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

tRoot :: Term a -> Either Int a  Deterministic 

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

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

tCons :: Eq a => Term a -> [a]  Deterministic 

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

tConsAll :: Term a -> [a]  Deterministic 

Returns a list of all constructors in a term. The resulting list may contain duplicates.

tVars :: Term a -> [Int]  Deterministic 

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

tVarsAll :: Term a -> [Int]  Deterministic 

Returns a list of all variables in a term. The resulting list may contain duplicates.

isConsTerm :: Term a -> Bool  Deterministic 

Checks whether a term is a constructor term.

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

isVarTerm :: Term a -> Bool  Deterministic 

Checks whether a term is a variable term.

isGround :: Term a -> Bool  Deterministic 

Checks whether a term is a ground term (contains no variables).

isLinear :: Term a -> Bool  Deterministic 

Checks whether a term is linear (contains no variable more than once).

isNormal :: Term a -> Bool  Deterministic 

Checks whether a term is normal (behind a variable is not a constructor).

maxVarInTerm :: Term a -> Maybe Int  Deterministic 

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

minVarInTerm :: Term a -> Maybe Int  Deterministic 

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

normalizeTerm :: Term a -> Term a  Deterministic 

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

renameTermVars :: Int -> Term a -> Term a  Deterministic 

Renames the variables in a term by the given number.

mapTerm :: (a -> b) -> Term a -> Term b  Deterministic 

Transforms a term by applying a transformation on all constructors.

eqConsPattern :: Eq a => Term a -> Term a -> Bool  Deterministic 

Checks whether the constructor pattern of the first term is equal to the constructor pattern of the second term. Returns True if both terms have the same constructor and the same arity.