Tools:Oops
Oops (Oops)
- developed at RWTH Aachen, Germany
- home page: http://verify.rwth-aachen.de/emmes/Oops/Oops-0.0.1.tar.gz
- developers: Fabian Emmes, Lars Noschinski
- publication:
Oops
Oops is no real complexity analyzer. Its main purpose was to mark unsuitable examples in the runtime complexity categories during the Termination Competition 2010. Many thanks to Georg Moser for the fitting name.
For runtime complexity, one does not analyze the derivation length of arbitrary terms (as one does in derivational complexity), but only of terms with exactly one defined symbol. For some systems this leads to much better intuition about the complexity of the described functions, but for others this definition yields strange results. For example applicative systems only have one defined symbol (the apply symbol), whereas the rest are just constants. Starting only with one apply symbol (as runtime complexity requires), one is most likely not able to build the derivation sequences the author of the example intended.
Furthermore, for such examples where all constructor symbols are constants, there are only finitely many basic terms. This makes asymptotic complexity analysis pointless, as one cannot build arbitrary large start terms.
We identified the following situations, in which we can conclude constant complexity. The strategy of oops is just to identify these situations and return an upper bound of O(1) if successful.
- All constructor symbols of the system are constants. This implies that there are only finitely many basic terms. If all of those terms are terminating, we can conclude constant runtime complexity. The termination of the terms proved by testing doing all possible evaluations of those terms.
- A similar situation occurs if all defined symbols are constants. Again we have only finitely many basic terms which can be tested.
- A third case is if the left-hand sides of all rules contain at least two defined symbols. Since every basic term has exactly one defined symbol, no rule can be applied to any basic term. This way, we can directly conclude O(1), without testing any terms for termination.
