Tyrolean Complexity Tool
Small Polynomial Path Orders

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)
33
O(n^2)
1112
O(n^3)
11
Total YES
1516
Total MAYBE
53
Total TIMEOUT
12
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

Details