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

Stability | unstable |

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

Safe Haskell | Safe-Infered |

This module provides the *compose-RC* transformation.

- decomposeDG :: TheTransformer (DecomposeDG AnyProcessor AnyProcessor)
- 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)
- decomposeDGselect :: ExpressionSelector
- data DecomposeDGProof p1 p2
- = DecomposeDGProof {
- cpRuleSelector :: ExpressionSelector
- cpUnselected :: Trs
- cpSelected :: Trs
- cpExtensionRules :: Trs
- cpProofD :: Maybe (Proof p1)
- cpProofU :: Maybe (Proof p2)
- cpProbD :: Problem
- cpProbU :: Problem
- cpWdg :: DG

- | DecomposeDGInapplicable String

- = DecomposeDGProof {
- decomposeDGProcessor :: Transformation (DecomposeDG AnyProcessor AnyProcessor) AnyProcessor
- data DecomposeDG p1 p2

# 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.

decomposeDGselect :: ExpressionSelector

This is the default `RuleSelector`

used with `decomposeDG`

.

# Proof Object

data DecomposeDGProof p1 p2

DecomposeDGProof | |

- cpRuleSelector :: ExpressionSelector
- cpUnselected :: Trs
- cpSelected :: Trs
- cpExtensionRules :: Trs
- cpProofD :: Maybe (Proof p1)
- cpProofU :: Maybe (Proof p2)
- cpProbD :: Problem
- cpProbU :: Problem
- cpWdg :: DG
| |

DecomposeDGInapplicable String |

# Processor

data DecomposeDG p1 p2

(Processor p1, Processor p2) => Transformer (DecomposeDG p1 p2) | |

(Processor p1, Processor p2) => TransformationProof (DecomposeDG p1 p2) |