On this page we compare small polynomial path orders to various similar techniques.
The employed testbed collects a subset of 290 examples from the
termination problem database, version 8.0.
This subset was obtained by restricting the
runtime complexity problem set
to orthogonal constructor TRSs that are known to be terminating
.
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) | - | - | - | - | 5 | 5 |
O(n^1) | - | - | - | - | 14 | 19 |
O(n^2) | - | - | - | - | 4 | 4 |
POLY | - | - | 24 | 29 | - | - |
ELEMENTARY | 29 | - | - | - | - | - |
PRIMREC | - | 40 | - | - | - | - |
Total YES | 29 | 40 | 24 | 29 | 23 | 28 |
Total MAYBE | 261 | 250 | 266 | 261 | 267 | 262 |
Strict Wins | 5 | 11 | - | - | - | 5 |
Average Execution Time (in seconds)
LMPO | MPO | POP* | POP* (PS) | sPOP* | sPOP* (PS) | |
|---|---|---|---|---|---|---|
O(1) | - | - | - | - | 0.061 | 0.056 |
O(n^1) | - | - | - | - | 0.066 | 0.075 |
O(n^2) | - | - | - | - | 0.090 | 0.097 |
POLY | - | - | 0.043 | 0.049 | - | - |
ELEMENTARY | 0.048 | - | - | - | - | - |
PRIMREC | - | 0.080 | - | - | - | - |
Total YES | 0.048 | 0.080 | 0.043 | 0.049 | 0.069 | 0.075 |
Total MAYBE | 0.061 | 0.076 | 0.063 | 0.063 | 0.062 | 0.062 |