On this web page, we provide the experimental data supporting our claims.
Runtime_Complexity_Innermost_Rewriting.
Out of the above 663 TRSs, 294 TRSs have potential for parallelism, indicated by a Maximal Structural Dependency Chain Set
of size at least two for the right-hand side of at least one rewrite rule.
This corresponds to function calls at parallel positions.
If this is not given, the parallel-innermost rewrite relation and the (sequential) innermost rewrite relation from the considered start terms (i.e., basic terms) are identical.
Details of the corresponding analysis are available here.
Therefore, we now focus on this subset of 294 parallelisable TRSs,
with the data taken from the same experiments as above.
Our benchmark files are available here:(GOAL COMPLEXITY)(STARTTERM CONSTRUCTOR-BASED)
The line
(STRATEGY INNERMOST)
denotes that only (sequential) innermost rewrite strategies are considered.
To indicate that runtime complexity of parallel-innermost
rewrite strategies is supposed to be analysed, replace this line by:
(STRATEGY PARALLELINNERMOST)
For our experiments on confluence, in addition to the above benchmarks,
we used the 577 unsorted unconditional TRSs of
COPS (version of 29 May 2023),
the benchmark collection used in the
Confluence Competition.
The file format is the same as above, except that the above annotations
are absent. The TRSs in these files are normally analysed for confluence
of full rewriting. In contrast, we analyse them for confluence of
parallel-innermost rewriting.
Our benchmark files from COPS are available here:
benchmarks_cops.zip
We used the all.q computer queue
and a timeout of 300 seconds per example.
As far as we are aware, prior to our work there have not been any automated tools able to analyse runtime complexity of parallel-innermost rewriting. However, an upper bound on runtime complexity of innermost rewriting is always also an upper bound on runtime complexity of parallel-innermost rewriting: pircR(n) ≤ ircR(n) holds for all TRSs R.
Thus, as the state of the art for upper bounds of runtime complexity of parallel-innermost rewriting with which to compare our contributions, we used the complexity analysis tools AProVE and TcT (Starexec URL for TcT) from the Termination and Complexity Competitions in 2021 and 2022 to analyse runtime complexity for innermost rewriting. We used the "tct_rci" configuration of TcT from StarExec. The corresponding tool configurations are labelled "AProVE irc" and "TcT irc" in our tables.
We have assessed the following configurations of AProVE and TcT as the state of the art in searching for upper bounds of parallel-innermost complexity. You can find the resulting data from these experiments downloaded from StarExec here:
We implemented our contributions in the complexity analysis tool AProVE. The configuration "AProVE pircR Section 3" includes the techniques from Section 3, and the configuration "AProVE pircR Sections 3 & 4" (in two variants for different confluence criteria, to assess the impact of the criteria for complexity analysis) includes the techniques from both Section 3 and Section 4. We used these configurations to obtain upper and lower bounds on the runtime complexity of parallel-innermost rewriting for the TRSs from our benchmark suite. You can find the data from these experiments here:
Thus, we used the above configurations of AProVE and TcT from the Termination Competitions 2021 and 2022 for ircR also to analyse PDT(R)/R. You can find the data from these experiments here:
| Tool | O(1) | ≤ O(n) | ≤ O(n2) | ≤ O(n3) | ≤ O(n≥4) |
|---|---|---|---|---|---|
| TcT irc | 4 | 32 | 51 | 62 | 67 |
| AProVE irc | 5 | 50 | 111 | 123 | 127 |
| AProVE pirc Section 3 | 5 | 70 | 125 | 139 | 141 |
| AProVE pirc Sections 3 and 4 | 5 | 70 | 125 | 140 | 142 |
| TCT pirc Section 4 | 4 | 46 | 66 | 79 | 80 |
| AProVE pirc Section 4 | 5 | 64 | 99 | 108 | 108 |
Here we use upper bounds on
ircR as a correct but imprecise over-approximation
for pircR.
We observe that upper complexity bounds improve in a
noticeable number of cases, e.g., linear bounds on pirc can now be inferred
for 70 TRSs rather than for 50 TRSs, an improvement by 40%.
Improvements from irc to pirc can be drastic:
for example, for the TRS TCT_12/recursion_10, the
bounds found by AProVE change from an upper bound of sequential
complexity of O(n10) to a (tight) upper bound for
parallel complexity of O(n).
(This TRS models a specific recursion structure, with rules
{ f0(x) → a } ∪
{ fi(x) → gi(x,x), gi(s(x), y) → b(fi-1(y), gi(x,y)) | 1 ≤ i ≤ 10 }, and is highly amenable to parallelisation.)
We observe that adding the
techniques from Section 4 to the techniques from
Section 3 leads to only few examples for which better
upper bounds can be found.
| Tool | Confluent | ≥ Ω(n) | ≥ Ω(n2) | ≥ Ω(n3) | ≥ Ω(n≥4) |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4, confluence by Corollary 5.10 | 165 | 116 | 22 | 5 | 1 |
| AProVE pirc Sections 3 and 4, confluence by Theorem 5.18 | 190 | 133 | 22 | 5 | 1 |
| TcT pirc Section 4, confluence by Corollary 5.10 | 165 | 112 | 0 | 0 | 0 |
| TcT pirc Section 4, confluence by Theorem 5.18 | 190 | 131 | 0 | 0 | 0 |
| AProVE pirc Section 4, confluence by Corollary 5.10 | 165 | 140 | 21 | 5 | 1 |
| AProVE pirc Section 4, confluence by Theorem 5.18 | 190 | 159 | 21 | 5 | 1 |
We observe that non-trivial lower bounds can be inferred for 140 out of the 165 examples proved confluent via Corollary 5.10, and for 159 out of the 190 examples proved confluent via Theorem 5.18. This shows that our transformation from Section 4 has practical value since it produces relative TRSs that are generally amenable to analysis by existing program analysis tools. (A standard concern with transformations for program analysis is that, although correct, their output might be hard to analyse for existing tools. Our experimental results alleviate this concern for the contributions of this paper, both for upper and for lower bounds on pirc.) It also shows that the more powerful confluence analysis by Theorem 5.18 improves also the inference of lower complexity bounds.
| Tool | Θ(1) | Θ(n) | Θ(n2) | Θ(n3) | Total |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4, confluence by Corollary 5.10 | 5 | 27 | 0 | 3 | 35 |
| AProVE pirc Sections 3 and 4, confluence by Theorem 5.18 | 5 | 33 | 0 | 3 | 41 |
| TcT pirc Section 4, confluence by Corollary 5.10 | 4 | 19 | 0 | 0 | 23 |
| TcT pirc Section 4, confluence by Theorem 5.18 | 4 | 22 | 0 | 0 | 26 |
| AProVE pirc Section 4, confluence by Corollary 5.10 | 5 | 33 | 0 | 3 | 41 |
| AProVE pirc Section 4, confluence by Theorem 5.18 | 5 | 41 | 0 | 3 | 49 |
Finally, the third table shows that for overall 49 of the 294 TRSs, the bounds that were found are asymptotically precise.
However, the nature of the benchmark set also plays a significant role
for assessing the applicability of criteria for proving confluence.
In our second experiment using the 577 TRSs obtained from COPS,
only 60 out of the 577 TRSs (about 10.4%) were proved confluent by
Corollary 5.10. In contrast, using Theorem 5.18, confluence proofs
for 274 TRSs (about 47.5%) were found, a much higher number.
Details of our experiments on the TRSs from COPS are
available here:
confluence_analysis_cops.txt
The significantly lower success rate for this benchmark
set is not surprising: COPS collects TRSs that provide a challenge
to confluence analysis tools, whereas the analysed subset of the
TPDB contains TRSs which are interesting specifically for
runtime complexity analysis.
Towards a possible explanation for the substantially higher success rate
of Theorem 5.18 over Corollary 5.10, consider that the benchmark set
is specifically about confluence of the full rewrite relation,
whereas we assess the parallel-innermost rewrite relation.
Both Corollary 5.10 and Theorem 5.18 take
the more restricted choice of (innermost!) redexes for rewrite steps
into account, but Theorem 5.18 does so to a much higher degree.