"Constant Runtime Complexity of Term Rewriting is Semi-Decidable" - Experiments

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.


Implementation in AProVE

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.


Settings

In our experiments, we consider various configurations of AProVE, namely:

This covers all techniques which are implemented in AProVE and can prove or disprove rcR(m) ∈ O(1). In the following, we refer to the combination of AProVE CDT, AProVE RNTS, AProVE CoFloCo, AProVE Loops, AProVE Induction, and AProVE Extra Vars as AProVE '17. Additionally, we also compare with TcT, since AProVE and TcT were the most powerful complexity tools for TRSs at the Termination and Complexity Competition 2017.

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.


Examples

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.


Experiments & Discussion

Full Rewriting

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:

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.

Innermost Rewriting

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.


References

  1. F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
    Lower Bounds for Runtime Complexity of Term Rewriting
    Journal of Automated Reasoning, 59(1):121-163, 2017. ©Springer-Verlag
    The final publication is available at Springer via the DOI 10.1007/s10817-016-9397-x.
    Preliminary Version
  2. F. Frohn and J. Giesl
    Analyzing Runtime Complexity via Innermost Runtime Complexity
    In Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '17), Maun, Botswana, EPiC Series in Computing 46, pages 249-268, 2017.
    Extended version appeared as Technical Report AIB-2017-02, RWTH Aachen University, Germany.
  3. M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl
    Complexity Analysis for Term Rewriting by Integer Transition Systems
    In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasilia, Brazil, Lecture Notes in Artificial Intelligence 10483, pages 132-150, 2017. ©Springer-Verlag
    Extended version appeared as Technical Report AIB-2017-05, RWTH Aachen University, Germany.
  4. L. Noschinski, F. Emmes, and J. Giesl
    Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs
    Journal of Automated Reasoning, 51(1):27-56, 2013. ©Springer-Verlag.
    The final publication is available at Springer via the DOI 10.1007/s10817-013-9277-6.
    Preliminary Version