This website contains additional information on our paper “A Dependency Pair Framework for Relative Termination of Term Rewriting”. More precisely, we provide information on our implementation in the tool AProVE and we describe our experiments.
The easiest way to run AProVE is via its web interface.
Moreover, recent releases of AProVE are available for download on GitHub. Release 8f672b5 is the newest release that is able to analyze relative termination of TRSs via annotated dependency pairs (ADPs). For termination analysis of (relative) term rewriting, the following dependencies have to be installed (see here for more installation instructions):
Extending the path environment is necessary so that AProVE can find these programs.
AProVE can parse the standard XML input format from the annual termination competition (TermComp), as well as the original .trs format (see also here) for relative TRSs. One distinguishes the main from the base TRS by using ‘->’ for rules of the main TRS, and ‘->=’ for relative rules (i.e., of the base TRS).
We use the same general strategy to prove relative termination via ADPs as for proving ordinary termination via DPs. We generate the canonical ADPs, and start by using the dependency graph processor. Afterwards, we try to apply the reduction pair processor to remove some annotations and to move rules from the main ADPs to the relative part. In the end, we try to use the rule removal processor to remove ADPs. Then we loop back to the dependency graph processor and repeat the whole process.
Whenever the relative ADPs contain no annotation anymore, we switch to ordinary DPs via the first derelatifying processor. We noticed that the argument filtering processor is important to handle DP problems that result from relative termination problems. Usually, this processor is only applied rarely in AProVE, because it entails a switch from “minimal” DP problems (where it suffices to prove the absence of minimal infinite chains) to general DP problems (where one has to prove the absence of all infinite chains). However, in our setting the DP problems that result from the derelatifying processor are not “minimal” anyway. Hence, we search for a possible argument filtering that helps in proving termination of the DP problem, and then use the standard DP framework with its corresponding strategy.
Finally, if no other processor is applicable, then we use the second derelatifying processor. If this fails as well, we use the previously existing techniques in AProVE to analyze the relative TRSs directly, e.g., by searching for a loop that shows non-termination. While the chain criterion and processors like the dependency graph and reduction pair processor are not only sound but also complete, there is not yet any processor that can disprove relative termination within the ADP framework.
Our implementation can be tested via a web interface.
Enter Program Code shows the program that is currently analyzed. The user can modify the program or replace it by a new one.Upload a File of a program to analyze (where the file should have the extension .trs).Submit calls AProVE in order to prove (relative) termination of the given TRS.Return to program input takes you back to the web page with the input program.As mentioned above, instead of using the web interface, you can also download AProVE. After installing all dependencies, make sure that the path variables are set as described above. Then AProVE can be run by executing
java -ea -jar aprove.jar -m wst mset2.trs
or if you want to see the full proof you can use the option -p plain for a plain text version or -p html for an html format as in the web interface.
java -ea -jar aprove.jar -m wst mset2.trs -p plain
java -ea -jar aprove.jar -m wst mset2.trs -p html
One can also set a fixed time limit.
Use the option -t limit to set the maximum time to search for a termination proof in seconds, e.g.,
java -ea -jar aprove.jar -m wst mset2.trs -p html -t 30
To evaluate the power of our new processors, we added 32 new benchmarks to the existing set of 98 benchmarks for relative termination of TRSs from the TPDB, the benchmark collection used at TermComp. Most of these examples adapt well-known classical TRSs from the TPDB to the relative setting. The set of all new benchmarks can be found here. Each benchmark also contains a comment to explain what the example illustrates and from which classical TRS it was obtained.
We tested AProVE using StarExec, which provides an Intel Xeon E5-2609 CPU with 2.4 GHz and 264 GB of RAM.
The following table shows the overall results for the new version of AProVE via ADPs compared to the old version of AProVE
and the three current competitors in TermComp: NaTT, TTT2, and MultumNonMulta (MnM).
For all tools except NaTT, we used the version from TermComp 2023. For NaTT, we used the version from TermComp 2022 due to a bug in its version from TermComp 2023.
Here, the result YES indicates a successful proof of relative termination,
NO indicates a successful disproof of relative termination, and
MAYBE indicates that the tool did not obtain a result within the timeout.
As in TermComp, a timeout of 300 seconds was used for each example. The numbers in
brackets are the respective results when only considering our new 32 examples.
AVG(s) gives the average runtime of the tool
on solved examples in seconds.
| New AProVE | NaTT | Old AProVE | TTT2 | MnM | |
|---|---|---|---|---|---|
| YES | 91 (32) | 68 (10) | 48 (5) | 39 (3) | 0 (0) |
| NO | 13 (0) | 5 (0) | 13 (0) | 7 (0) | 13 (0) |
| MAYBE | 26 (0) | 57 (22) | 69 (27) | 84 (29) | 117 (32) |
| AVG(s) | 5.11 | 0.41 | 4.02 | 1.67 | 1.60 |
A detailed table with the individual result for each benchmark can be found here.
The table clearly shows that while Old AProVE was already the second most powerful
tool for relative termination, the integration of the ADP framework in New AProVE
yields a substantial advance in power (i.e., it only fails on 26 of the examples, compared
to 57 and 69 failures of NaTT and Old AProVE, respectively).
In particular, previous tools (including Old AProVE)
often have problems with relative TRSs where the main TRS does
not dominate the base TRS and where it does not suffice to directly use (monotonic) reduction orders. In contrast, the ADP framework can handle such examples (and it also improves AProVE’s results on the previous 98 examples of the collection). The runtime of AProVE increases due to the integration of the novel ADP framework, but still successful proofs do not take longer than 6 seconds on average.
Furthermore, we tested our new ADP framework also for other applications of relative rewriting, namely relative string rewriting and equational rewriting. We used the 403 benchmarks from the TPDB and compared the ADP framework to the current competitors from the corresponding categories of TermComp. In the category of relative string rewriting, these competitors are Matchbox in addition to NaTT, TTT2, MultumNonMulta (MnM), and AProVE. Also for Matchbox, we used the version from TermComp 2023.
| MnM | Matchbox | AProVE | TTT2 | ADP Framework | NaTT | |
|---|---|---|---|---|---|---|
| YES | 261 | 259 | 207 | 96 | 69 | 61 |
| NO | 13 | 10 | 2 | 2 | 2 | 0 |
| MAYBE | 129 | 134 | 194 | 305 | 332 | 342 |
Due to the base ADPs with two annotated symbols on the right-hand side, here the ADP framework is less powerful than dedicated techniques for string rewriting. To be precise, it is very challenging to successfully use the reduction pair processor if two annotations are above each other in the right-hand side of a rule, e.g., if we have g(g(x)) ->= g(g(x)) as a relative rule. Then we would have the ADP g(g(x)) ->= G(G(x)) and for the reduction pair processor with polynomial interpretations we have to satisfy Pol(G(g(x))) >= Pol(c2(G(g(x)),G(x))) = Pol(G(g(x))) + Pol(G(x)), if Pol interprets the symbol c2 as addition. The problem is that we need to consider the inner g twice when computing the polynomial value of the right-hand side.
Finally, for equational rewriting we compared with MU-TERM, NaTT and AProVE on the 76 benchmarks for AC- and C-rewriting from the TPDB. Again, for MU-TERM, we used the version from TermComp 2023.
| AProVE | MU-TERM | NaTT | ADP Framework | |
|---|---|---|---|---|
| YES | 64 | 64 | 47 | 32 |
| NO | 2 | 0 | 1 | 4 |
| MAYBE | 10 | 12 | 28 | 40 |
Again, on these examples, our new framework is weaker than
dedicated tools for AC-rewriting.
However, note that all these examples only use AC- or C-equations where
unification is decidable and finitary.
Our new ADP framework also works for other theories.
Furthermore, we are able to find two NOs that no previous tool was able to find on the examples Mixed_C/PEANO-NAT_nosorts-noand.trs and Mixed_C/PEANO-NAT_nosorts.trs by moving to DPs via the first derelatifying processor and then using a processor that searches for infinite chains to disprove termination.
Some of our examples demonstrate the strengths and the limits of the ADP framework.
Our leading example R_mset2 (Ex. 14 from our paper) is relatively terminating. Here, we need DPs to prove relative termination (due to the div-rules that cannot be handled by standard simplification orders) but the previous technique for the application of ordinary DPs for relative termination fails because the main TRS does not dominate the base TRS.
minus(x, o) -> x
minus(s(x), s(y)) -> minus(x, y)
div(x, s(o)) -> x
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
divL(x, nil) -> x
divL(x, cons(y, xs)) -> divL(div(x, y), xs)
divL(z, cons(x, cons(y, zs))) ->= divL(z, cons(y, cons(x, zs)))
As mentioned above, with our new ADP framework we can now use dependency pairs for equational theories E where E-unification is not finitary or undecidable. Associativity is an example for a theory where unification is infinitary. However, associativity is also hard to deal with for our new ADP framework due to the two defined symbols in the right-hand side. As we mentioned above, it is very challenging to successfully use the reduction pair processor if two annotations are above each other in the right-hand side of a rule.
app(nil, ys) -> ys
app(cons(x,xs), ys) -> cons(x,app(xs,ys))
app(xs, app(ys, zs)) ->= app(app(xs, ys), zs)
app(app(xs, ys), zs) ->= app(xs, app(ys, zs))
In this example we have an append-algorithm and additionally two relative rules which express that append is associative. The corresponding ADPs for the relative rules are app(xs, app(ys, zs)) ->= APP(APP(xs, ys), zs) and app(app(xs, ys), zs) ->= APP(xs, APP(ys, zs)). Here, the reduction pair processor has difficulties to orient the rules since the inner app needs to be considered twice in the calculation. Actually, the only polynomial interpretation that can orient the ADP app(xs, app(ys, zs)) ->= APP(APP(xs, ys), zs) equal is the interpretation that maps APP to 0. On the other hand, relative termination of the example can be proved easily without (A)DPs by simply applying (monotonic) reduction orders (or by using the rule removal processor).
The following is a variant of the Toyama example where one uses relative rules to permute the arguments of f. With the ADP framework, we can now prove relative termination by only using the relative dependency graph processor, without searching for a reduction pair.
f(a,b,x) -> f(x,x,x)
f(x,y,z) ->= f(y,x,z)
f(x,y,z) ->= f(x,z,y)
f(x,y,z) ->= f(z,y,x)
The following example illustrates lassos in the dependency graph.
minus(x,0) -> x
minus(x,s(y)) -> pred(minus(x,y))
quot(0,s(y)) -> 0
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
pred(s(x)) ->= x
pred(s(x)) ->= s(pred(x))
s(pred(x)) ->= pred(s(x))
log(s(0)) ->= 0
log(s(s(x))) ->= s(log(s(quot(x,s(s(0))))))
This algorithm computes the logarithm w.r.t. base 2 of a natural number. However, we allow switching between different representations of integer numbers using the successor and the predecessor function. This and the rules for the logarithm itself are relative. Note that the last log-rule is an SCC on its own that has a path to the quot-rules. These result in two different minimal lassos in the dependency graph that we need to analyze on their own.