tct-2.0.1: A Complexity Analyser for Term Rewrite Systems

Portabilityunportable
Stabilityunstable
MaintainerMartin Avanzini <martin.avanzini@uibk.ac.at>
Safe HaskellSafe-Infered

Tct.Method.ComposeRC

Contents

Description

This module provides the compose-RC transformation.

Synopsis

Documentation

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.

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.

Proof Object

Processor

data DecomposeDG p1 p2

Instances