On this page we compare polynomial path orders to its predecessors.
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
|
Interpretations
|
Polynomial (degree 2 and 3) and Matrix Interpretations (dimension 1 and 3) run in parallel. The implementation uses the usable arguments criterion to weaken monotonicity constraints. |
|
LMPO
|
Lightweight multiset path orders |
|
MPO
|
Multiset Path Orders |
|
POP*
|
Polynomial Path Orders |
|
POP* (PS)
|
Polynomial Path Orders with Parameter Substitution |
Overview
Interpretations | LMPO | MPO | POP* | POP* (PS) | |
|---|---|---|---|---|---|
O(n^1) | 85 | - | - | - | - |
O(n^2) | 18 | - | - | - | - |
O(n^3) | 36 | - | - | - | - |
POLY | - | - | - | 43 | 56 |
ELEMENTARY | - | 57 | - | - | - |
PRIMREC | - | - | 76 | - | - |
Total YES | 139 | 57 | 76 | 43 | 56 |
Total MAYBE | 272 | 540 | 518 | 554 | 541 |
Total TIMEOUT | 186 | - | 3 | - | - |
Strict Wins | 139 | 4 | 14 | - | 2 |
Average Execution Time (in seconds)
Interpretations | LMPO | MPO | POP* | POP* (PS) | |
|---|---|---|---|---|---|
O(n^1) | 0.403 | - | - | - | - |
O(n^2) | 2.284 | - | - | - | - |
O(n^3) | 8.584 | - | - | - | - |
POLY | - | - | - | 0.176 | 0.187 |
ELEMENTARY | - | 0.201 | - | - | - |
PRIMREC | - | - | 0.332 | - | - |
Total YES | 2.765 | 0.201 | 0.332 | 0.176 | 0.187 |
Total MAYBE | 6.470 | 0.410 | 0.519 | 0.361 | 0.370 |