termlib-0.9: Term Rewriting Library

Safe HaskellSafe-Infered

Termlib.Repl

Contents

Synopsis

Documentation

This Module provides enlists most common used functions.

Data Structures containing terms

class WithTerms a where

Methods

vars :: a -> Set Variable

extracts the set of variables

symbols :: a -> Set Symbol

extracts the set of function symbols

subterms :: a -> Set Term

returns the list of subterms

isLinear :: a -> Bool

isGround :: a -> Bool

isFlat :: a -> Bool

isShallow :: a -> Bool

Instances

isSubtermOf :: WithTerms a => Term -> a -> Bool

't `isSubtermOf` a' checks if t occurs in the list of subterms of a

nonVariableSubterms :: WithTerms a => a -> Set Term

filters variables from the list of subterms

Terms

data Term

Constructors

Var Variable

term is a variable

Fun Symbol [Term]

'Fun f ts' denotes term with root symbol f and arguments ts

Instances

Querying

depth :: Term -> Int

returns the depth of a term. Variables and constants admit depth '0'

size :: Term -> Int

returns the size of a term. Variables and constants admit size '1'

fsize :: Term -> Int

returns the number of function symbols

root :: Term -> Either Variable Symbol

returns the root of the term

immediateSubterms :: Term -> [Term]

returns the list of direct subterms or '[]' if argument is a variable

properSubterms :: Term -> [Term]

returns the list of subterms, excluding the argument

isSupertermOf :: Term -> Term -> Bool

converse of isSubtermOf

cardinality :: Either Variable Symbol -> Term -> Int

returns the number of occurences of the first argument

isUnifiable :: Term -> Term -> Bool

returns True iff the arguments are unifiable

isRenamedUnifiable :: Term -> Term -> Bool

returns True iff renamings without common variables are unifiable

matches :: Term -> Term -> Bool

's `matches` t' returns True iff t is an instance of s

subsumes :: Term -> Term -> Bool

inverse of matches

encompasses :: Term -> Term -> Bool

's `encomapsses` t' returns True iff s encompasses t

variant :: Term -> Term -> Bool

two terms are variants if they subsume eatch other

isVariable :: Term -> Bool

returns True if the argument is a variable

type Overlap = (Rule, [Int], Rule)

Term Rewriting Rule

data Rule

Constructors

Rule 

Fields

lhs :: Term

left hand side of rule

rhs :: Term

right hand side of rule

Instances

Predicates

See module Termlib.Rule for further predicates. Predicates can be lifted with all and any from module Foldable to Trss.

isNonErasing :: Rule -> Bool

rule is non-erasing if every occurence of a variable in the left-hand side occurs in the right-hand side

isErasing :: Rule -> Bool

inverse of isNonErasing

isNonDuplicating :: Rule -> Bool

a rule is non-duplicating if no variable appears more often in the right-hand side than in the left-hand side

isDuplicating :: Rule -> Bool

inverse of isNonDuplicating

Modification

invert :: Rule -> Rule

convert a rule 'l -> r' to 'r -> l'

canonise :: Rule -> Rule

renames variables to a canonical form. Two rules r1 and r2 are equal modulo variable renaming, iff 'canonise r1' and 'canonise r2' are syntactically equal.

Term Rewrite System

type Trs = RuleSet Rule

A TRS is a list of Rule.

emptyTrs :: Trs

The empty Trs..

fromRules :: [Rule] -> Trs

translates a list of rewrite rules to a Trs.

toRules :: Trs -> [Rule]

returns the list of rewrite rules in the TRS

Set Operations

union :: Trs -> Trs -> Trs

union operator on the set of rules, removing duplicates

append :: Trs -> Trs -> Trs

like union, but does not remove duplicates

(\\) :: Trs -> Trs -> Trs

difference on the set of rules

intersect :: Trs -> Trs -> Trs

intersection on the set of rules

member :: Trs -> Rule -> Bool

checks if a rule is contained in the TRS, does not perform variable conversion

insert :: Rule -> Trs -> Trs

inserts a rule into a TRS, if the rule is not already contained

Querying

lhss :: Trs -> [Term]

returns the list of left-hand sides

rhss :: Trs -> [Term]

returns the list of left-hand sides

definedSymbols :: Trs -> Set Symbol

returns roots of right-hand sides

constructors :: Trs -> Set Symbol

returns all symbols which are not roots of right-hand sides

overlaps :: Trs -> [Overlap]

returns the Overlap of a term rewrite system ** Predicates | Many predicates are defined in Termlib.Rule. These can be lifted to Trs by all and any

isEmpty :: Trs -> Bool

checks if the list of rules is empty

wellFormed :: Trs -> Bool

checks that no left-hand side is a variable and all variables of a right-hand side are included in the corresponding left-hand side

isOverlapping :: Trs -> Bool

returns True iff it contains two overlapping rules

isOverlay :: Trs -> Bool

returns True iff all overlaps are only root overlaps

isOrthogonal :: Trs -> Bool

returns True iff the given TRS is orthogonal

isNestedRecursive :: Trs -> Bool

returns True iff there exists a rule 'f(..) -> C[f(..C[f(..)]..)]'.

Modification

filterRules :: (Rule -> Bool) -> Trs -> Trs

removes rules from the TRS matching the predicate

mapRules :: (Rule -> Rule) -> Trs -> Trs

map the given function over the rules

Complexity Problem

data Problem

Constructors

Problem 

Fields

startTerms :: StartTerms

considered start-terms

strategy :: Strategy

considered strategy

variables :: Variables

underlying set of variables

signature :: Signature

underlying signature

strictDPs :: Trs

strict dependency pairs

strictTrs :: Trs

strict rules

weakDPs :: Trs

weak dependency pairs

weakTrs :: Trs

weak rules

Instances

data StartTerms

Constructors

BasicTerms 

Fields

defineds :: Set Symbol
 
constrs :: Set Symbol
 
TermAlgebra (Set Symbol) 

Instances

data Ruleset

Constructors

Ruleset 

Fields

sdp :: Trs

strict dependency pairs

wdp :: Trs

weak dependency pairs

strs :: Trs

strict rules

wtrs :: Trs

weak rules

emptyRuleset :: Ruleset

data Strategy

Constructors

Innermost 
Full 
ContextSensitive ReplacementMap 
Outermost 

Instances

Querying

weakComponents :: Problem -> Trs

returns weak dependency pairs and weak rewrite rules

strictComponents :: Problem -> Trs

returns strict dependency pairs and strict rewrite rules

dpComponents :: Problem -> Trs

returns all dependency pairs

trsComponents :: Problem -> Trs

returns all dependency rules which are not dependency pairs

allComponents :: Problem -> Trs

returns all dependency pairs and rules ** Predicates

isRCProblem :: Problem -> Bool

returns True iff the set of start-terms is basic

isDCProblem :: Problem -> Bool

converse of isRCProblem

isDPProblem :: Problem -> Bool

returns True iff the set of start-terms is basic, and all defined symbols are marked in the set of basic terms

Modification

withFreshCompounds :: Problem -> Problem

replaces all compound symbols by fresh compound symbols, and removes unary compound symbols

Parsing Utilities

parseFromString :: TermParser a -> String -> Problem -> (a, Problem)