We prove that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be examined by considering finitely many start terms. We implemented our semi-decision procedure in the tool AProVE to show its efficiency and its success for systems where state-of-the-art complexity analysis tools fail.
We integrated our new technique in the termination and complexity analyzer AProVE, which is one of the most powerful termination and complexity tools for TRSs. The implementation of our new semi-decision procedure for constant bounds can be accessed via a custom web interface.
This web interface only runs the procedure for the inference of constant bounds, i.e., it does not use the other complexity analysis techniques implemented in AProVE. Please note that the server running the web interface is considerably slower than the computer used for the experiments described below.
In our experiments, we consider various configurations of AProVE, namely:
We used a timeout of 60 seconds per example on an Intel Xeon with 4 cores at 2.33 GHz each and 16 GB of RAM.
We evaluated the configurations described above on all 959 examples of the category "Runtime Complexity - Full Rewriting" and all 1022 examples of the category "Runtime Complexity - Innermost Rewriting" of the Termination and Complexity Competition 2016. Note that for these categories, the collection of examples from the Termination and Complexity Competition 2017 is a subset of the examples from the Termination and Complexity Competition 2016, as all non-left-linear and all non-constructor systems were removed from the category "Runtime Complexity - Innermost Rewriting" prior to the Termination and Complexity Competition 2017.
For full rewriting, our technique proves a constant upper bound in 57 cases. In 6 of these cases, neither AProVE '17 nor TcT is able to prove rcR(n) ∈ O(1). In contrast, whenever AProVE '17 or TcT proves a constant upper bound, AProVE Constant succeeds as well. The average runtime of AProVE Constant on successfully analyzed examples was 1.8 s. For all but 5 TRSs where AProVE Constant fails, AProVE '17 can disprove constant complexity (by inferring a non-constant lower bound for rcR(m)). The following (manual) analysis reveals that the remaining 5 TRSs have non-constant complexity, too:
SK90/2.61 consists of the following rules:
It has the following non-terminating constructor-based narrowing sequence (here, "⊳" stands for the proper superterm relation and "→" stands for the rewrite relation):
Note that the only function symbols which are introduced by the narrowing substitutions in the ⇝-steps are the constructors j, h1, and s (e.g., the substitution in the first ⇝-step instantiates x with j(x'', h1(s(x'), y'))), i.e., the narrowing sequence is indeed constructor based. According to the main theorem from our paper, this proves rcR(m) ∉ O(1).
Strategy_removed_mixed_05/ex6 consists of the following rules:
It has the following loop:
Thus, this TRS is non-terminating. As the start term f(x,x) of the non-terminating sequence is basic, this proves rcR(m) ∉ O(1).
Transformed_CSR_04/ExIntrod_GM99_Z consists of the following rules:
It has the following loop:
Even though sieve(from(s(s(x)))) is not basic, its instance sieve(from(s(s(0)))) is reachable from the basic term primes due to the rule primes → sieve(from(s(s(0)))), which proves rcR(m) ∉ O(1).
Transformed_CSR_04/LISTUTILITIES_complete_noand_GM has
407 rules. One of them is the decreasing loop [1]
which proves rcR(m) ∉ O(1).
Transformed_CSR_04/LISTUTILITIES_nosorts-noand_Z
consists of the following rules:
It has the following decreasing loop:
Thus, we have rcR(m) ∉ O(1).
Click here for more detailed results of all benchmarks for full rewriting. In this table, clicking on the name of an example opens the web interface in order to let the semi-decision procedure run on the respective example.
For innermost rewriting, AProVE Constant proves a constant upper bound in 58
cases. In 3 of these cases, neither AProVE '17 nor TcT is able to prove
ircR(m) ∈ O(1) (where ircR denotes
the innermost runtime complexity function). Again, whenever AProVE '17 or
TcT infers a constant upper bound, AProVE Constant succeeds as well. Its
average runtime per successfully analyzed example was again 1.4 s. In all but 6
cases where AProVE Constant fails, AProVE '17 can disprove constant
complexity (by inferring a non-constant lower bound for
ircR(m)). A manual analysis reveals that 5 of these 6 examples
have non-constant
complexity as well: Frederiksen_Glenstrup/ordered_better, SK90/2.61, Strategy_removed_mixed_05/ex6, Transformed_CSR_04/LISTUTILITIES_complete_noand_GM,
and Transformed_CSR_04/LISTUTILITIES_nosorts-noand_Z.
The only TRS with constant complexity where AProVE Constant fails is
Frederiksen_Glenstrup/nolexicord. This is a TRS with
relative
rules.
Such rules can be applied "for free", i.e., their application does not contribute to the derivation height.
While our procedure is clearly sound in the presence of relative rules, it is no longer a semi-decision procedure.
For example, consider the TRS consisting of a single relative rule f → f.
Its runtime complexity is obviously constant, but the constructor-based narrowing
sequence f ⇝ f ⇝ ... does not terminate.
AProVE Constant can also prove ircR(m) ∈ O(1)
for Transformed_CSR_04/ExIntrod_GM99_Z, whose innermost
runtime complexity is constant, whereas its full runtime complexity is
unbounded. To see this, note that the second rewrite step of the loop
shown above is not innermost, as cons is a defined symbol and the subterm
cons(...,...) is not in normal form.
Click here for more detailed results of all benchmarks for innermost rewriting.