On this page we compare small polynomial path orders to various similar techniques.
The employed testbed collects a subset of 597 examples from the
termination problem database, version 8.0.
This subset was obtained by restricting the
runtime complexity problem set
to constructor TRSs that are known to be terminating
.
Techniques
The tests rendered below cover following techniques:|
LMPO
|
Lightweight multiset path orders over quasi precedences |
|
MPO
|
multiset path orders over quasi precedences |
|
POP*
|
Polynomial Path Orders over quasi precedences |
|
POP* (PS)
|
polynomial path orders with parameter substitution, over quasi precedences |
|
sPOP*
|
Small polynomial path orders over quasi precedences |
|
sPOP* (PS)
|
Small polynomial path orders with parameter substitution, over quasi precedences |
Overview
LMPO | MPO | POP* | POP* (PS) | sPOP* | sPOP* (PS) | |
|---|---|---|---|---|---|---|
O(1) | - | - | - | - | 9 | 9 |
O(n^1) | - | - | - | - | 23 | 37 |
O(n^2) | - | - | - | - | 6 | 7 |
O(n^3) | - | - | - | - | 1 | 1 |
POLY | - | - | 43 | 56 | - | - |
ELEMENTARY | 57 | - | - | - | - | - |
PRIMREC | - | 76 | - | - | - | - |
Total YES | 57 | 76 | 43 | 56 | 39 | 54 |
Total MAYBE | 540 | 520 | 554 | 541 | 558 | 543 |
Strict Wins | 14 | 19 | - | - | - | 15 |
Average Execution Time (in seconds)
LMPO | MPO | POP* | POP* (PS) | sPOP* | sPOP* (PS) | |
|---|---|---|---|---|---|---|
O(1) | - | - | - | - | 0.057 | 0.056 |
O(n^1) | - | - | - | - | 0.071 | 0.085 |
O(n^2) | - | - | - | - | 0.089 | 0.095 |
O(n^3) | - | - | - | - | 0.197 | 0.216 |
POLY | - | - | 0.048 | 0.050 | - | - |
ELEMENTARY | 0.053 | - | - | - | - | - |
PRIMREC | - | 0.085 | - | - | - | - |
Total YES | 0.053 | 0.085 | 0.048 | 0.050 | 0.074 | 0.084 |
Total MAYBE | 0.101 | 0.156 | 0.095 | 0.095 | 0.092 | 0.099 |