| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Certificate
Description
This module defines the Certificate and Complexity datatype,
together with accessors.
- data Complexity
- constant :: Complexity
- poly :: Maybe Int -> Complexity
- expo :: Maybe Int -> Complexity
- supexp :: Complexity
- primrec :: Complexity
- unknown :: Complexity
- add :: Complexity -> Complexity -> Complexity
- mult :: Complexity -> Complexity -> Complexity
- compose :: Complexity -> Complexity -> Complexity
- iter :: Complexity -> Complexity -> Complexity
- data Certificate
- lowerBound :: Certificate -> Complexity
- upperBound :: Certificate -> Complexity
- certified :: (Complexity, Complexity) -> Certificate
- uncertified :: Certificate
Complexity
data Complexity
Constructors
| Poly (Maybe Int) | Polynomial. If argument is |
| Exp (Maybe Int) | Exponential. If argument is |
| Supexp | Super exponential. |
| Primrec | Primitive recursive. |
| Multrec | Multiple recursive. |
| Rec | Recursive. |
| Unknown | Unknown. |
Instances
The datatype Complexity is TcTs representation
of a bounding function, in big-O notation
Constructors
Constructor for constant bounding function.
poly :: Maybe Int -> Complexity
Constructor for polynomial bounding function, with optional degree.
expo :: Maybe Int -> Complexity
Constructor for elementary (k-exponential) bounding function.
supexp :: Complexity
Constructor for super exponential bounding function.
Constructor for primitive recursive bounding function.
Combinations
add :: Complexity -> Complexity -> Complexity
Addition of bounds modulo big-O notation, i.e., f ` so
constructs an element of add` gComplexity that majorises O(f(n)) + O(g(n)).
mult :: Complexity -> Complexity -> Complexity
Multiplication of bounds modulo big-O notation, i.e., f ` so
constructs an element of mult` gComplexity that majorises O(f(n)) + O(g(n)).
compose :: Complexity -> Complexity -> Complexity
Composition of bounds modulo big-O notation, i.e., f ` so
constructs an element of compose` gComplexity that majorises O(f(g(n))).
iter :: Complexity -> Complexity -> Complexity
Iteration of bounds modulo big-O notation, i.e., f ` so
constructs an element of iter` gComplexity that majorises O(f(..f(n)..))
with O(m) occurences of f.
Complexity Certificate
data Certificate
A certificate consists of a lower and an upper bound.
lowerBound :: Certificate -> Complexity
Extract the lower bound from a Certificate.
upperBound :: Certificate -> Complexity
Extract the upper bound from a Certificate.
certified :: (Complexity, Complexity) -> Certificate
The call certificate (l,u) constructs a Certificate
with lower bound l and upper bound u.
Constructs a Certificate where both lower and upper bounds are unknown.