Portability | unportable |
---|---|

Stability | unstable |

Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |

Safe Haskell | Safe-Infered |

This module reexports direct constructors for *processor instances*
of TcT. For description of the corresponding processor, please see module
Tct.Processors.
In addition, this module also exports a wealth of combinators.

Instances are separated into instances of *standard processors*
and instances of *transformations* for historical reasons.
Whereas standard processors either suceed or fail, transformations
construct from a given input problem several subproblems that
reflect the complexity of the input problem.

- success :: ProcessorInstance Success
- fail :: ProcessorInstance Fail
- open :: ProcessorInstance Open
- empty :: ProcessorInstance EmptyRules
- arctic :: ProcessorInstance ArcticMI
- matrix :: ProcessorInstance NaturalMI
- poly :: ProcessorInstance NaturalPI
- simplePolynomial :: ProcessorInstance NaturalPI
- linearPolynomial :: ProcessorInstance NaturalPI
- stronglyLinearPolynomial :: ProcessorInstance NaturalPI
- simpleMixedPolynomial :: ProcessorInstance NaturalPI
- quadraticPolynomial :: ProcessorInstance NaturalPI
- customPolynomial :: ([Variable] -> [SimpleMonomial]) -> ProcessorInstance NaturalPI
- data SimpleMonomial
- (^^^) :: a -> Int -> Power a
- mono :: [Power Variable] -> SimpleMonomial
- boolCoefficient :: SimpleMonomial -> SimpleMonomial
- constant :: SimpleMonomial
- class HasDimension a where
- withDimension :: a -> Int -> a

- class HasCertBy a where
- withCertBy :: a -> NaturalMIKind -> a

- data NaturalMIKind
- = Algebraic
- | Automaton
- | Triangular
- | Unrestricted

- class HasDegree a where
- withDegree :: a -> Maybe Int -> a

- class HasBits a where
- class HasCBits a where
- class HasUsableArgs a where
- withUsableArgs :: a -> Bool -> a

- class HasUsableRules a where
- withUsableRules :: a -> Bool -> a

- class HasKind a k | a -> k where
- ofKind :: a -> k -> a

- data PolyShape
- = SimpleShape SimplePolyShape
- | CustomShape ([Variable] -> [SimpleMonomial])

- popstar :: ProcessorInstance PopStar
- popstarPS :: ProcessorInstance PopStar
- lmpo :: ProcessorInstance PopStar
- spopstar :: ProcessorInstance PopStar
- spopstarPS :: ProcessorInstance PopStar
- mpo :: InstanceOf (StdProcessor Mpo)
- bounds :: InitialAutomaton -> Enrichment -> ProcessorInstance Bounds
- data Enrichment
- data InitialAutomaton
- ite :: (Processor g, Processor t, Processor e) => InstanceOf g -> InstanceOf t -> InstanceOf e -> ProcessorInstance (Ite g t e)
- iteProgress :: (Transformer g, Processor t, Processor e) => TheTransformer g -> InstanceOf t -> InstanceOf e -> ProcessorInstance (IteProgress g t e)
- step :: (Transformer t1, Processor a) => [t] -> (t -> TheTransformer t1) -> (t -> InstanceOf a) -> InstanceOf SomeProcessor
- upto :: (Enum n, Ord n, ComplexityProof (ProofOf p), Processor p) => (n -> InstanceOf p) -> (Bool :+: (n :+: n)) -> ProcessorInstance (OneOf p)
- named :: Processor proc => String -> InstanceOf proc -> InstanceOf SomeProcessor
- bsearch :: Processor proc => String -> (Maybe Int -> InstanceOf proc) -> InstanceOf (Custom Unit (ProofOf proc))
- before :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)
- orBetter :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)
- orFaster :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)
- sequentially :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)
- best :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)
- fastest :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)
- isCollapsing :: WhichTrs -> ProcessorInstance Predicate
- isConstructor :: WhichTrs -> ProcessorInstance Predicate
- isDuplicating :: WhichTrs -> ProcessorInstance Predicate
- isLeftLinear :: WhichTrs -> ProcessorInstance Predicate
- isRightLinear :: WhichTrs -> ProcessorInstance Predicate
- isWellFormed :: WhichTrs -> ProcessorInstance Predicate
- isFull :: ProcessorInstance Predicate
- isInnermost :: ProcessorInstance Predicate
- isOutermost :: ProcessorInstance Predicate
- isRCProblem :: ProcessorInstance Predicate
- isDCProblem :: ProcessorInstance Predicate
- isContextSensitive :: ProcessorInstance Predicate
- trsPredicate :: String -> (Trs -> Bool) -> WhichTrs -> ProcessorInstance Predicate
- problemPredicate :: String -> (Problem -> Bool) -> ProcessorInstance Predicate
- data WhichTrs
- (>>|) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub
- (>>!) :: (Processor b, Transformer t) => TheTransformer t -> InstanceOf b -> InstanceOf SomeProcessor
- (>>||) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub
- (>>!!) :: (Processor b, Transformer t) => TheTransformer t -> InstanceOf b -> InstanceOf SomeProcessor
- irr :: TheTransformer InnermostRuleRemoval
- toInnermost :: TheTransformer ToInnermost
- uncurry :: TheTransformer Uncurry
- weightgap :: TheTransformer WeightGap
- data WgOn
- wgOn :: TheTransformer WeightGap -> WgOn -> TheTransformer WeightGap
- decompose :: Processor p1 => ExpressionSelector -> DecomposeBound -> InstanceOf p1 -> TheTransformer (Decompose p1)
- decomposeBy :: ExpressionSelector -> TheTransformer (Decompose AnyProcessor)
- decomposeAnyWith :: Processor p1 => InstanceOf p1 -> TheTransformer (Decompose p1)
- combineBy :: Processor p1 => TheTransformer (Decompose p1) -> DecomposeBound -> TheTransformer (Decompose p1)
- greedy :: Processor p1 => TheTransformer (Decompose p1) -> TheTransformer (Decompose p1)
- decomposeIndependent :: TheTransformer SomeTransformation
- decomposeIndependentSG :: TheTransformer SomeTransformation
- data DecomposeBound
- dependencyPairs :: TheTransformer DPs
- dependencyTuples :: TheTransformer DPs
- data Approximation
- pathAnalysis :: TheTransformer PathAnalysis
- linearPathAnalysis :: TheTransformer PathAnalysis
- usableRules :: TheTransformer UR
- simpPE :: TheTransformer (SimpPE AnyProcessor)
- simpPEOn :: ExpressionSelector -> TheTransformer (SimpPE AnyProcessor)
- withPEOn :: Processor p => InstanceOf p -> ExpressionSelector -> TheTransformer (SimpPE p)
- decomposeDG :: TheTransformer (DecomposeDG AnyProcessor AnyProcessor)
- decomposeDGselect :: ExpressionSelector
- solveUpperWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p1 p)
- solveLowerWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p p2)
- selectLowerBy :: (Processor p1, Processor p2) => TheTransformer (DecomposeDG p1 p2) -> RuleSelector SelectorExpression -> TheTransformer (DecomposeDG p1 p2)
- removeWeakSuffix :: TheTransformer RemoveWeakSuffix
- removeHeads :: TheTransformer RemoveHead
- trivial :: TheTransformer Trivial
- removeInapplicable :: TheTransformer RemoveInapplicable
- simpDPRHS :: TheTransformer SimpRHS
- try :: Transformer t => TheTransformer t -> TheTransformer (Try t)
- force :: Transformer t => TheTransformer t -> TheTransformer (Try t)
- (>>>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation
- (<>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation
- (<||>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation
- exhaustively :: Transformer t => TheTransformer t -> TheTransformer SomeTransformation
- te :: Transformer t => TheTransformer t -> TheTransformer (Try SomeTransformation)
- successive :: Transformer t => [TheTransformer t] -> TheTransformer SomeTransformation
- when :: EQuantified inp (TheTransformer SomeTransformation) => Bool -> inp -> TheTransformer SomeTransformation
- idtrans :: TheTransformer Id
- toDP :: TheTransformer SomeTransformation
- dpsimps :: TheTransformer SomeTransformation
- removeLeaf :: Processor p => InstanceOf p -> TheTransformer SomeTransformation
- cleanSuffix :: TheTransformer SomeTransformation
- class TimesOut inp outp | inp -> outp where
- class Timed inp outp | inp -> outp where
- timed :: inp -> outp

- class WithProblem inp outp | inp -> outp where
- withProblem :: (Problem -> inp) -> outp

- withWDG :: WithProblem inp outp => (DG -> inp) -> outp
- withCWDG :: WithProblem inp outp => (CDG -> inp) -> outp
- withStrategy :: WithProblem inp outp => (Strategy -> inp) -> outp
- rc2011 :: InstanceOf SomeProcessor
- dc2011 :: InstanceOf SomeProcessor
- rc2012 :: InstanceOf SomeProcessor
- dc2012 :: InstanceOf SomeProcessor
- certify2012 :: InstanceOf SomeProcessor
- module Tct.Method.RuleSelector
- type ProcessorInstance a = InstanceOf (StdProcessor a)
- data TheTransformer t
- class EQuantified inp outp | inp -> outp where
- equantify :: inp -> outp

- some :: EQuantified inp outp => inp -> outp

# Standard Processors

This section collects combinators concerning standard processors, toghether with combinators on standard processors.

## Trivial Processors

success :: ProcessorInstance Success

This processor always returns the answer `Yes(?,?)`

.

fail :: ProcessorInstance Fail

This processor always returns the answer `No`

.

open :: ProcessorInstance Open

This processor always returns the answer `Maybe`

.

empty :: ProcessorInstance EmptyRules

This processor returns the answer `Yes(O(1),(1))`

if the strict component is empty.

## Processors Based on Interpretations

### Matrix Interpretations

TcT implements both *matrix interpretations over natural numbers* and *arctic matrix interpretations*.

arctic :: ProcessorInstance ArcticMI

This processor implements arctic interpretations.

matrix :: ProcessorInstance NaturalMI

This processor implements matrix interpretations.

Further customisation of these processors is possible as described in Tct.Instances

### Polynomial Interpretations

TcT implements *polynomial interpretations over natural numbers*.
Again these can be customised as described Tct.Instances

simplePolynomial :: ProcessorInstance NaturalPI

Options for `simple`

polynomial interpretations.

linearPolynomial :: ProcessorInstance NaturalPI

Options for `linear`

polynomial interpretations.

stronglyLinearPolynomial :: ProcessorInstance NaturalPI

Options for `strongly linear`

polynomial interpretations.

simpleMixedPolynomial :: ProcessorInstance NaturalPI

Options for `simple mixed`

polynomial interpretations.

quadraticPolynomial :: ProcessorInstance NaturalPI

Options for `quadratic mixed`

polynomial interpretations.

#### Custom Polynomial Shapes

customPolynomial :: ([Variable] -> [SimpleMonomial]) -> ProcessorInstance NaturalPI

Option for polynomials of custom shape, as defined by the first argument.
This function receives a list of variables
denoting the `n`

arguments of the interpretation function. The return value of type [`SimpleMonomial`

]
corresponds to the list of monomials of the constructed interpretation function.
A polynomial is a list of unique `SimpleMonomial`

, where `SimpleMonomial`

are
considered equal if the set variables together with powers match.
`SimpleMonomial`

can be build using `^^^`

, `constant`

and `mono`

.
For instance, linear interpretations are constructed using the function
```
vs -> [constant] ++ [ v^^^1 | v <- vs]
```

.

data SimpleMonomial

A `SimpleMonomial`

denotes a monomial with variables in `Variable`

,
and can be build using `^^^`

, `constant`

and `mono`

.

mono :: [Power Variable] -> SimpleMonomial

```
mono [v1^^^k1,...,vn^^^kn]
```

constructs the `SimpleMonomial`

```
c * v1^k1 * ... * v1^kn
```

where `c`

is unique for the constructed monomial.

boolCoefficient :: SimpleMonomial -> SimpleMonomial

Returns a new monomial whose coefficient is guaranteed to be `0`

or `1`

.

Returns a new monomial without variables.

### Customising Interpretations

The following classes allow the costumisation of interpretation
techniques implemented in TcT,
cf., `arctic`

, `matrix`

and `polys`

that construct various processors
based on sensible defaults.
To exemplify the usage,

matrix `withDimension` 3 `withCertBy` Automaton

defines an matrix interpretation of dimension `3`

, whose complexity certificate
is inferred using automaton techniques.

class HasDimension a where

withDimension :: a -> Int -> a

Modify dimesion of method.

class HasCertBy a where

withCertBy :: a -> NaturalMIKind -> a

Defines under which method a certificate should be obtained

data NaturalMIKind

This parameter defines the shape of the matrix interpretations, and how the induced complexity is computed.

Algebraic | Count number of ones in diagonal to compute induced complexity function. |

Automaton | Use automaton-techniques to compute induced complexity function. |

Triangular | Use triangular matrices only. |

Unrestricted | Put no further restrictions on the interpretation. |

class HasDegree a where

withDegree :: a -> Maybe Int -> a

Specifies an upper bound on the estimated degree, or ounbounded degree if given `Nothing`

.

class HasBits a where

class HasCBits a where

class HasUsableArgs a where

withUsableArgs :: a -> Bool -> a

Specifies that the *usable arguments* criterion should be employed to weaken monotonicity requirements.

class HasUsableRules a where

withUsableRules :: a -> Bool -> a

Specifies that the *usable rules modulo interpretation* criterion should be considered.

data PolyShape

The shape of polynomial interpretations.

## Processors Based on Recursive Path Orderings

popstar :: ProcessorInstance PopStar

This processor implements polynomial path orders.

popstarPS :: ProcessorInstance PopStar

This processor implements polynomial path orders with parameter substitution.

lmpo :: ProcessorInstance PopStar

This processor implements lightweight multiset path orders.

spopstar :: ProcessorInstance PopStar

This processor implements small polynomial path orders (polynomial path orders with product extension and weak safe composition) which allow to determine the degree of the obtained polynomial certificate.

spopstarPS :: ProcessorInstance PopStar

This processor is like `popstarSmall`

but incorporates parameter substitution addidionally.

mpo :: InstanceOf (StdProcessor Mpo)

This processor implements multiset path orders.

## Bounds Processor

bounds :: InitialAutomaton -> Enrichment -> ProcessorInstance Bounds

This processor implements the bounds technique.

data Enrichment

This datatype represents the *enrichment* employed.

data InitialAutomaton

This datatype represents the initial automaton employed.

## Control Structures

ite :: (Processor g, Processor t, Processor e) => InstanceOf g -> InstanceOf t -> InstanceOf e -> ProcessorInstance (Ite g t e)

`ite g t e`

applies processor `t`

if processor `g`

succeeds, otherwise processor `e`

is applied.

iteProgress :: (Transformer g, Processor t, Processor e) => TheTransformer g -> InstanceOf t -> InstanceOf e -> ProcessorInstance (IteProgress g t e)

step :: (Transformer t1, Processor a) => [t] -> (t -> TheTransformer t1) -> (t -> InstanceOf a) -> InstanceOf SomeProcessor

```
step [l..u] trans proc
```

successively applies the transformations
```
[trans l..trans u]
```

, additionally checking after each application of `trans i`

whether `proc i`

can solve the problem. More precise
```
step [l..] trans proc == proc l `
```

.
The resulting processor can be infinite.
`before`

` (trans l `>>|`

(proc l ``before`

` (trans l `>>|`

...)))

upto :: (Enum n, Ord n, ComplexityProof (ProofOf p), Processor p) => (n -> InstanceOf p) -> (Bool :+: (n :+: n)) -> ProcessorInstance (OneOf p)

```
upto mkproc (b :+: l :+: u) == f [ mkproc i | i <- [l..u]]
```

where
`f == fastest`

if `b == True`

and `f == sequentially`

otherwise.

named :: Processor proc => String -> InstanceOf proc -> InstanceOf SomeProcessor

'named name proc' acts like `proc`

, but displays itself under the name `name`

in proof outputs

bsearch :: Processor proc => String -> (Maybe Int -> InstanceOf proc) -> InstanceOf (Custom Unit (ProofOf proc))

## Combinators Guiding the Proof Search

before :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)

The processor `p1 `

first applies processor `before`

p2`p1`

, and if that fails processor `p2`

.

orBetter :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)

The processor `p1 `

applies processor `orBetter`

p2`p1`

and `p2`

in parallel. Returns the
proof that gives the better certificate.

orFaster :: (Processor a, Processor b) => InstanceOf a -> InstanceOf b -> ProcessorInstance (OneOf SomeProcessor)

The processor `p1 `

applies processor `orFaster`

p2`p1`

and `p2`

in parallel. Returns the
proof of that processor that finishes fastest.

The following three processors provide list versions of `before`

, `orBetter`

and `orFaster`

respectively.
Note that the type of all given processors need to agree. To mix processors
of different type, use `some`

on the individual arguments.

sequentially :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)

List version of `before`

.

best :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)

List version of `orBetter`

.
Note that the type of all given processors need to agree. To mix processors
of different type, use `some`

on the individual arguments.

fastest :: Processor p => [InstanceOf p] -> ProcessorInstance (OneOf p)

List version of `orFaster`

.
Note that the type of all given processors need to agree. To mix processors
of different type, use `some`

on the individual arguments.

## Predicates

The following predicates return either the answer `Yes(?,?)`

or `No`

.

trsPredicate :: String -> (Trs -> Bool) -> WhichTrs -> ProcessorInstance Predicate

problemPredicate :: String -> (Problem -> Bool) -> ProcessorInstance Predicate

data WhichTrs

Determines which components of a problem should be checked.

# Transformations

This section list all instances of `Transformation`

. A transformation `t`

is lifted to a `Processor`

using the combinator `>>|`

or `>>||`

.

## Lifting Transformations to Processors

(>>|) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub

(>>!) :: (Processor b, Transformer t) => TheTransformer t -> InstanceOf b -> InstanceOf SomeProcessor

Similar to `>>|`

but checks if strict rules are empty

(>>||) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub

Like `>>|`

but resulting subproblems are solved in parallel by the given processor.

(>>!!) :: (Processor b, Transformer t) => TheTransformer t -> InstanceOf b -> InstanceOf SomeProcessor

Similar to `>>||`

but checks if strict rules are empty

## Instances

### Innermost Rule Removal

irr :: TheTransformer InnermostRuleRemoval

On innermost problems, this processor removes inapplicable rules by looking at non-root overlaps.

### To Innermost Transformation

### Uncurrying

uncurry :: TheTransformer Uncurry

Uncurrying for full and innermost rewriting. Note that this processor fails on dependency pair problems.

### Weightgap Principle

weightgap :: TheTransformer WeightGap

This processor implements the weightgap principle.

data WgOn

wgOn :: TheTransformer WeightGap -> WgOn -> TheTransformer WeightGap

### Decompose

decompose :: Processor p1 => ExpressionSelector -> DecomposeBound -> InstanceOf p1 -> TheTransformer (Decompose p1)

This transformation implements techniques for splitting the complexity problem
into two complexity problems (R) and (S) so that the complexity of the input problem
can be estimated by the complexity of the transformed problem.
The processor closely follows the ideas presented in
*Complexity Bounds From Relative Termination Proofs*
(http://www.imn.htwk-leipzig.de/~waldmann/talk/06/rpt/rel/main.pdf).

decomposeBy :: ExpressionSelector -> TheTransformer (Decompose AnyProcessor)

same as decompose with `DecomposeBound`

`Add`

, but the transformation results in two sub-problems,
instead of applying a given processor on the selected sub-problem

decomposeAnyWith :: Processor p1 => InstanceOf p1 -> TheTransformer (Decompose p1)

`decomposeAnyWith == decompose (selAnyOf selStricts) Add`

.

combineBy :: Processor p1 => TheTransformer (Decompose p1) -> DecomposeBound -> TheTransformer (Decompose p1)

greedy :: Processor p1 => TheTransformer (Decompose p1) -> TheTransformer (Decompose p1)

decomposeIndependent :: TheTransformer SomeTransformation

Using the decomposition processor (c.f. `decomposeBy`

) this transformation
decomposes dependency pairs into two independent sets, in the sense that these DPs
constitute unconnected sub-graphs of the dependency graph. Applies `cleanSuffix`

on the resulting sub-problems,
if applicable.

decomposeIndependentSG :: TheTransformer SomeTransformation

Similar to `decomposeIndependent`

, but in the computation of the independent sets,
dependency pairs above cycles in the dependency graph are not taken into account.

data DecomposeBound

### Weak Dependency Pairs and Dependency Tuples

dependencyPairs :: TheTransformer DPs

Implements dependency pair transformation. Only applicable on runtime-complexity problems.

dependencyTuples :: TheTransformer DPs

Implements dependency tuples transformation. Only applicable on innermost runtime-complexity problems.

data Approximation

### Path analysis

pathAnalysis :: TheTransformer PathAnalysis

Path Analysis

linearPathAnalysis :: TheTransformer PathAnalysis

Variation of `pathAnalysis`

that generates only a linear number
of sub-problems, in the size of the dependency graph

### Usable Rules

### Predecessor Estimation

simpPE :: TheTransformer (SimpPE AnyProcessor)

Moves a strict dependency into the weak component if all predecessors in the dependency graph are strict and there is no edge from the rule to itself.

withPEOn :: Processor p => InstanceOf p -> ExpressionSelector -> TheTransformer (SimpPE p)

### Dependency Graph Decomposition

decomposeDG :: TheTransformer (DecomposeDG AnyProcessor AnyProcessor)

This processor implements processor 'dependency graph decomposition'. It tries to estimate the complexity of the input problem based on the complexity of dependency pairs of upper congruence classes (with respect to the congruence graph) relative to the dependency pairs in the remaining lower congruence classes. The overall upper bound for the complexity of the input problem is estimated by multiplication of upper bounds of the sub problems. Note that the processor allows the optional specification of processors that are applied on the two individual subproblems. The transformation results into the systems which could not be oriented by those processors.

decomposeDGselect :: ExpressionSelector

This is the default `RuleSelector`

used with `decomposeDG`

.

solveUpperWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p1 p)

Specify a processor to solve the upper component immediately. The Transformation aborts if the problem cannot be handled.

solveLowerWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p p2)

Specify a processor to solve the lower immediately. The Transformation aborts if the problem cannot be handled.

selectLowerBy :: (Processor p1, Processor p2) => TheTransformer (DecomposeDG p1 p2) -> RuleSelector SelectorExpression -> TheTransformer (DecomposeDG p1 p2)

Specify how the lower component should be selected.

### DP Simplifications

removeWeakSuffix :: TheTransformer RemoveWeakSuffix

Removes trailing weak paths. A dependency pair is on a trailing weak path if it is from the weak components and all sucessors in the dependency graph are on trailing weak paths.

Only applicable on DP-problems as obtained by `dependencyPairs`

or `dependencyTuples`

. Also
not applicable when `strictTrs prob = Trs.empty`

.

removeHeads :: TheTransformer RemoveHead

Removes unnecessary roots from the dependency graph.

trivial :: TheTransformer Trivial

Checks whether the DP problem is trivial, i.e., does not contain any cycles.

Only applicable on DP-problems as obtained by `dependencyPairs`

or `dependencyTuples`

. Also
not applicable when `strictTrs prob = Trs.empty`

.

removeInapplicable :: TheTransformer RemoveInapplicable

Removes inapplicable rules in DP deriviations.

Currently we check whether the left-hand side is non-basic, and there exists no incoming edge except from the same rule.

simpDPRHS :: TheTransformer SimpRHS

Simplifies right-hand sides of dependency pairs.
Removes r_i from right-hand side `c_n(r_1,...,r_n)`

if no instance of
r_i can be rewritten.

Only applicable on DP-problems as obtained by `dependencyPairs`

or `dependencyTuples`

. Also
not applicable when `strictTrs prob = Trs.empty`

.

## Combinators

Following Combinators work on transformations.

try :: Transformer t => TheTransformer t -> TheTransformer (Try t)

The transformer `try t`

behaves like `t`

but succeeds even if `t`

fails. When `t`

fails
the input problem is returned.

force :: Transformer t => TheTransformer t -> TheTransformer (Try t)

The transformer `force t`

behaves like `t`

but fails always whenever no
progress is achieved.

(>>>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer `t1 >>> t2`

first transforms using `t1`

, resulting subproblems are
transformed using `t2`

.

(<>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer `t1 <> t2`

transforms the input using `t1`

if successfull, otherwise
`t2`

is applied.

(<||>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer `t1 <||> t2`

applies the transformations `t1`

and
`t2`

in parallel, using the result of whichever transformation succeeds first.

exhaustively :: Transformer t => TheTransformer t -> TheTransformer SomeTransformation

The transformer `exhaustively t`

applies `t`

repeatedly until `t`

fails.
`exhaustively t == t `

.
`>>>`

try (exhaustively t)

te :: Transformer t => TheTransformer t -> TheTransformer (Try SomeTransformation)

Shorthand for 'try . exhaustively'

successive :: Transformer t => [TheTransformer t] -> TheTransformer SomeTransformation

List version of `>>>`

.

successive [t_1..t_n] == t_1 >>> .. >>> t_n

when :: EQuantified inp (TheTransformer SomeTransformation) => Bool -> inp -> TheTransformer SomeTransformation

Transformation 'when b t' applies `t`

only when `b`

holds

idtrans :: TheTransformer Id

Identity transformation.

## Abbreviations

toDP :: TheTransformer SomeTransformation

Tries dependency pairs for RC, and dependency pairs with weightgap, otherwise uses dependency tuples for IRC. Simpifies the resulting DP problem as much as possible.

dpsimps :: TheTransformer SomeTransformation

Fast simplifications based on dependency graph analysis.

removeLeaf :: Processor p => InstanceOf p -> TheTransformer SomeTransformation

tries to remove leafs in the congruence graph,
by (i) orienting using predecessor extimation and the given processor,
and (ii) using `removeWeakSuffix`

and various sensible further simplifications.
Fails only if (i) fails.

cleanSuffix :: TheTransformer SomeTransformation

use `simpPEOn`

and `removeWeakSuffix`

to remove leafs from the dependency graph.
If successful, right-hand sides of dependency pairs are simplified (`simpDPRHS`

)
and usable rules are re-computed (`usableRules`

).

# Inspecting Combinators

class TimesOut inp outp | inp -> outp where

Lifts a processor or transformation to one that times out after given number of seconds

(Processor p, ~ * outp (ProcessorInstance (Timeout p))) => TimesOut (InstanceOf p) outp | |

Transformer t => TimesOut (TheTransformer t) (TheTransformer (Timeout t)) |

class Timed inp outp | inp -> outp where

timed :: inp -> outp

Additionally present timing information

(Processor p, ~ * outp (ProcessorInstance (Timed p))) => Timed (InstanceOf p) outp | |

Transformer t => Timed (TheTransformer t) (TheTransformer (Timed t)) |

class WithProblem inp outp | inp -> outp where

withProblem :: (Problem -> inp) -> outp

(Processor proc, ~ * (ProofOf proc) res) => WithProblem (InstanceOf proc) (InstanceOf (Custom Unit res)) | |

Transformer t => WithProblem (TheTransformer t) (TheTransformer (WithProblem t)) |

withWDG :: WithProblem inp outp => (DG -> inp) -> outp

withCWDG :: WithProblem inp outp => (CDG -> inp) -> outp

withStrategy :: WithProblem inp outp => (Strategy -> inp) -> outp

# Competition Strategies

Runtime complexity strategy employed in the competition 2011.

Derivational complexity strategy employed in the competition 2011.

Runtime complexity strategy employed in the competition 2012.

Derivational complexity strategy employed in the competition 2012.

Strategy for certification employed in the competition 2012.

# RuleSelector

module Tct.Method.RuleSelector

# Type Exports

type ProcessorInstance a = InstanceOf (StdProcessor a)

data TheTransformer t

This datatype defines a specific instance of a transformation.

HasUsableArgs (TheTransformer WeightGap) | |

HasCBits (TheTransformer WeightGap) | |

HasBits (TheTransformer WeightGap) | |

HasDegree (TheTransformer WeightGap) | |

Processor a => Decomposing (TheTransformer (Decompose a)) | |

HasCertBy (TheTransformer WeightGap) | |

HasDimension (TheTransformer WeightGap) | |

(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (TheTransformer t) | |

Transformer t => Apply (TheTransformer t) | |

Transformer trans => AsStrategy (TheTransformer trans) ConstantDeclaration | |

Transformer t => WithProblem (TheTransformer t) (TheTransformer (WithProblem t)) | |

Transformer t => Timed (TheTransformer t) (TheTransformer (Timed t)) | |

Transformer t => TimesOut (TheTransformer t) (TheTransformer (Timeout t)) | |

Transformer t => EQuantified (TheTransformer t) (TheTransformer SomeTransformation) | |

(ParsableArguments args, Transformer trans, ~ * ds (Domains args)) => AsStrategy (ds -> TheTransformer trans) (FunctionDeclaration args) |

class EQuantified inp outp | inp -> outp where

This class establishes a mapping between types and their existential quantified counterparts.

equantify :: inp -> outp

Processor p => EQuantified (InstanceOf p) (InstanceOf SomeProcessor) | |

Transformer t => EQuantified (TheTransformer t) (TheTransformer SomeTransformation) |

some :: EQuantified inp outp => inp -> outp

Wrap an object by existential quantification.