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

Contents

Description

This module defines the POP* and LMPO processors.

Synopsis

Proof Object

data PopStarOrder

Constructors

PopOrder 

Fields

popSafeMapping :: SafeMapping

The safe mapping.

popPrecedence :: Precedence

The precedence.

popRecursives :: RecursiveSymbols

Recursive symbols.

popArgumentFiltering :: Maybe ArgumentFiltering

Employed argument filtering.

popInputProblem :: Problem

The input problem.

popInstance :: TheProcessor PopStar

The specific instance employed.

popUsableSymbols :: [Symbol]

Defined symbols of usable rules.

popStrictlyOriented :: Trs

The rules that were effectively strictly oriented.

Instances

Instance Constructors

popstar :: ProcessorInstance PopStar

This processor implements polynomial path orders.

popstarPS :: ProcessorInstance PopStar

This processor implements polynomial path orders with parameter substitution.

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.

lmpo :: ProcessorInstance PopStar

This processor implements lightweight multiset path orders.

withDegree :: ProcessorInstance PopStar -> Maybe Int -> ProcessorInstance PopStar

Processors

data PopStar

Instances

The processor object.

popstarProcessor :: StdProcessor PopStar

Popstar processor.

ppopstarProcessor :: StdProcessor PopStar

Popstar processor with product extension. Set argument wsc to get small polynomial path orders

lmpoProcessor :: StdProcessor PopStar

Lightweight multiset path order processor.