On this page we demonstrate the effect of integrating small polynomial path orders in our complexity analyser TcT. As testbed we use straight forward translations of Resource aware ML programs to TRSs. The input program are also available here.
Techniques
|
tct
|
This column refers to TcT in a standard configuration that uses dependency pairs for complexity analysis, polynomial and matrix interpretations and a few simplifications. |
|
tct-popstar
|
This column refers to the above configuration of TcT but additionally employs small polynomial path orders. Noteworthy, the TRS representation of the longest common subsequence program can only be handled with this version. |
Overview
tct | tct-popstar | |
|---|---|---|
O(n^1) | 3 | 3 |
O(n^2) | 11 | 12 |
O(n^3) | 1 | 1 |
Total YES | 15 | 16 |
Total MAYBE | 5 | 3 |
Total TIMEOUT | 1 | 2 |
Strict Wins | - | 1 |
Average Execution Time (in seconds)
tct | tct-popstar | |
|---|---|---|
O(n^1) | 2.846 | 3.653 |
O(n^2) | 13.779 | 14.696 |
O(n^3) | 38.798 | 39.677 |
Total YES | 13.260 | 14.187 |
Total MAYBE | 36.411 | 41.948 |