This web site contains additional information on our paper “A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting”. More precisely, we provide a longer version of our paper including all appendices and proofs, 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 b4d5af is the newest release that is able to analyze termination, almost-sure termination (AST), and positive almost-sure termination (PAST) of PTRSs w.r.t. different rewrite strategies. For termination analysis of probabilistic term rewriting systems, 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.
In the following, we first describe the input syntax of a PTRS file. Then, we explain more details about our implementation. In the end, we describe how to execute the implementation via the web interface and via the JAR file on GitHub.
Our implementation uses the input syntax of PTRSs that was first described in the paper ADY20. The syntax extends the WST format for term rewrite systems by adding a new syntax for probabilistic rules. A probabilistic rewrite rule has the form:
lhs -> w1 : rhs1 || ... || wk : rhsk
Here, lhs, rhs1, …, rhsk are terms and w1,…,wk are natural numbers > 0. This corresponds to the rule:
lhs -> {w1/w : rhs1, ..., wk/w : rhsk}
where w is the sum of all w1,…,wk.
We also allow the following syntax for probabilistic rules that might be easier to read:
lhs -> a1/b1 : rhs1 || ... || ak/bk : rhsk
Here, lhs, rhs1,…,rhsk are again terms and a1,…,ak and b1,…,bk are natural numbers > 0 that describe the actual probabilities. This corresponds to the rule:
lhs -> {a1/b1 : rhs1, ..., ak/bk : rhsk}
However, one has to ensure that the value ai/bi is actually between 0 and 1, and that the sum of all probabilities in a rule is 1. Otherwise, AProVE rejects the input file with an exception. The PTRS may contain rules in both notations.
One can use AProVE to prove termination, AST, or PAST of PTRSs w.r.t. either full or innermost rewriting. The proof goal can be indicated via the keywords ‘STRATEGY’ and ‘GOAL’. The input file has to contain either ‘(GOAL TERMINATION)’, ‘(GOAL AST)’, or ‘(GOAL PAST)’. If the input file contains ‘(STRATEGY INNERMOST)’, then AProVE tries to prove the provided goal w.r.t. innermost evaluation and if the file does not contain the ‘STRATEGY’ keyword, then AProVE tries to prove the provided goal w.r.t. full rewriting.
As described in the input syntax section, we only allow for rational probabilities. Internally, we store probabilities as (arbitrarily precise) fractions, by storing the numerator and denominator as integers. However, once we need to check satisfiability of polynomial (in)equations (e.g., in the direct application of polynomial interpretations) we multiply the (in)equations with appropriate integers so that the resulting SMT-problem only deals with natural polynomials.
We use the same general strategy to prove (P)AST that was described here under ‘implementation’. However, we improve this approach into a complete criterion for iAST by presenting a new, more elegant definition of DPs, called Annotated Dependency Pairs (ADPs). Based on this, we integrate our newly developed transformational processors for proving innermost AST into the ADP framework. Our strategy for the use of the different processors follows the corresponding strategy in the non-probabilistic setting. Whenever possible, we try to use the dependency graph-, the usable terms-, the usable rules-, and the probability removal processor, and we call them the default processors. These are the processors that, if applicable, can only ease the termination proof, while being very fast to compute. If there is no default processor applicable, we first search for a very simple polynomial for the reduction pair processor. If this succeeds, we go back to the default processors and start our strategy from the start. Otherwise, we use our new transformational processors before proceeding.
Since these new transformational processors can sometimes be used infinitely often, even on an initial PTRS that is iAST, we have to integrate heuristics when to use which new processor. The added heuristics are similar to the heuristics used in the non-probabilistic setting, as described here. As in these previous heuristics, we call certain applications of a transformational processor safe such that we will always terminate if we only use safe transformations. An example of a condition that makes a transformation safe would be that the number of variables in the left-hand sides of the resulting DTs is strictly smaller than the number in the original DT.
For the strategy used in AProVE, we first try to use only safe transformations and if one of them is applied successfully, we go back to the start of our strategy. Only if all default processors, the reduction pair processor, and all safe transformations are not applicable, then we use the transformational processors arbitrarily for a fixed amount of time, until another processor becomes applicable again, or we give up. Regarding the order of the transformational processors, we first try to use the rewriting processor, followed by the rule overlap processor, the instantiation processor, and finally the forward instantiation processor.
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 .ptrs).Submit calls AProVE in order to prove almost-sure termination of the given PTRS.Return to program input takes you back to the web page with the input program.After downloading AProVE and 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 randData01.ptrs
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.
java -ea -jar aprove.jar -m wst randData01.ptrs -p plain
java -ea -jar aprove.jar -m wst randData01.ptrs -p html
One can also set a fixed time limit, which should be used, since our transformational processors might run infinitely long.
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 randData01.ptrs -p html -t 30
To evaluate the power of our new processors, we added 33 new benchmarks to the existing set of 67 benchmarks from here. The set of all benchmarks can be found here. The new benchmarks are partitioned into 4 categories:
We tested AProVE using StarExec, which provides an Intel Xeon E5-2609 CPU with 2.4 GHz and 264 GB of RAM.
Here, the result YES indicates a successful iAST proof,
the result MAYBE indicates that the tool crashed or terminated the verification process within the given time without a result,
and the result NO indicates a successful iAST disproof.
As in TermComp, a timeout of 300 seconds was used for each example.
The following table shows the overall results for AProVE with different transformational processors on all of the 33 new benchmarks. Here, we compare the version of the probabilistic DT framework without transformational processors (DT) to the new version that also includes our novel transformational processors (ADP-Trans). Here, we also evaluate settings where we disable the rewriting processor, the rule overlap instantiation processor, the instantiation and the forward instantiation processor, and a setting where we disable all transformational processors except rewriting. Finally, the setting AProVE below extends ADP-Trans by the direct application of polynomial interpretations to show AST.
| Number YES | Number YES AProVE | Number YES DT | Number YES ADP-Trans | Number YES Only Rewriting | Number YES Without Rewriting | Number YES Without Roi | Number YES Without Inst + FInst |
|---|---|---|---|---|---|---|---|
| 29 | 25 | 3 | 24 | 5 | 9 | 9 | 23 |
The next table shows the time needed for each of the different strategies (in seconds):
| Time AProVE | Time DT | Time ADP-Trans | Time Only Rewriting | Time Without Rewriting | Time Without Roi | Time Without Inst + FInst |
|---|---|---|---|---|---|---|
| 17.1 | 4.1 | 13.5 | 5.1 | 9.4 | 6.1 | 14.2 |
You can find a detailed table with the individual result and time for each benchmark here. We also added the results of our new version of AProVE to the table for the 67 old benchmarks, which can be found here. These tables also contain detailed descriptions of the individual examples.
Some of our examples demonstrate the strengths and the limits of the DT framework.
The leading example R_incpl (Paper02.ptrs) from our paper is AST, but not terminating. Here, the DT framework fails, but the ADP framework with the new transformational processors can prove almost-sure innermost termination automatically.
a -> 1 : f(h(g),g)
g -> 1/2 : b1 || 1/2 : b2
h(b1) -> 1 : a
f(x,b2) -> 1 : a
In our paper, we already presented a version of the classical probabilistic quicksort algorithm where iAST can only be proved if we use the new transformational processors. The following PTRS (randData01.ptrs) is the full implementation of this probabilistic quicksort algorithm.
rotate(nil) -> 1 : nil
rotate(cons(x, xs)) -> 1 : cons(x, xs) || 1 : rotate(app(xs, cons(x, nil)))
empty(nil) -> 1 : true
empty(cons(x, xs)) -> 1 : false
quicksort(xs) -> 1 : if(empty(xs), low(head(xs), tail(xs)), head(xs), high(head(xs), tail(xs)))
if(true, xs, x, ys) -> 1 : nil
if(false, xs, x, ys) -> 1 : app(quicksort(rotate(xs)), cons(x, quicksort(rotate(ys))))
head(cons(x, xs)) -> 1 : x
tail(cons(x, xs)) -> 1 : xs
low(x, nil) -> 1 : nil
low(x, cons(y, ys)) -> 1 : if_low(leq(y, x), x, cons(y, ys))
if_low(true, x, cons(y, ys)) -> 1 : low(x, ys)
if_low(false, x, cons(y, ys)) -> 1 : cons(y, low(x, ys))
high(x, nil) -> 1 : nil
high(x, cons(y, ys)) -> 1 : if_high(leq(y, x), x, cons(y, ys))
if_high(true, x, cons(y, ys)) -> 1 : cons(y, high(x, ys))
if_high(false, x, cons(y, ys)) -> 1 : high(x, ys)
leq(0, x) -> 1 : true
leq(s(x), 0) -> 1 : false
leq(s(x), s(y)) -> 1 : leq(x, y)
app(nil, ys) -> 1 : ys
app(cons(x, xs), ys) -> 1 : cons(x, app(xs, ys))
This quicksort algorithm searches for a random pivot element using the first two rotate rules.
Here, we rotate the list and always move the head element to the end of the list.
With a chance of 1/2 we stop this iteration and use the current head element as the next pivot element.
The rest of the rules represents the classical quicksort algorithm without any probabilities.
Here, app computes list concatenation,
low(x,xs) returns all elements of the list xs that are smaller than x, and high works analogously.
Furthermore, head returns the head element of a list and tail returns the rest of the list without the head.
Finally, empty checks whether the list is empty or not.
Using our new ADP framework with the new transformational processors,
ADP-Trans can automatically prove that this PTRS is iAST.
In particular, we need the transformations, namely the rewriting processor to evaluate the
head, tail, and empty functions, and we need the rule overlap instantiation
processor
to check for all possible terms that these functions can actually be applied on, e.g.,
we need to detect that if we have the term empty(x) for a variable x, then in order to
apply any rewrite step, the variable x needs to be instantiated with either nil or cons(...).
Another interesting probabilistic algorithm that deals with lists is the following: We are given two lists L1 and L2. If one of the two lists is empty, then the algorithm terminates. Otherwise, we either move the head of list L1 to L2 or vice versa, both with a chance of 1/2, and then we repeat this procedure. This algorithm is represented by the following PTRS (randData05.ptrs).
or(false,false) -> 1 : false
or(true,x) -> 1 : true
or(x,true) -> 1 : true
move_elements(xs,ys) -> 1 : if(or(empty(xs),empty(ys)), xs, ys)
if(true, xs, ys) -> 1 : xs
if(false, xs, ys) -> 1 : move_elements(tail(xs),cons(head(xs),ys)) || 1 : move_elements(cons(head(ys),xs), tail(ys))
empty(nil) -> 1 : true
empty(cons(x, xs)) -> 1 : false
head(cons(x, xs)) -> 1 : x
tail(cons(x, xs)) -> 1 : xs
This algorithm is iAST (and even AST) because we can view this as a classical random walk on the number of elements in the first list that is both bounded from below by 0 and from above by the sum of the lengths of both lists.
In order to prove this automatically, we again have to use some kind of instantiation processor, e.g., the rule overlap instantiation processor, to find all possible terms that the functions head, tail, and empty can actually be applied on.
In addition, we also need the rewriting processor again to evaluate these functions afterwards.
Once the move_elements-ADP contains the symbols cons and nil in the left-hand side, we can detect the structure of the random walk using an application of the reduction pair processor that removes all annotations of this ADP.
After that, there is no SCC in the dependency graph left, and we have proven iAST.
Another important task of termination analysis is to be able to handle conditions on numbers.
These occur in nearly every program and often impact the termination behavior.
The same is true for probabilistic programs.
For a successful proof of iAST without transformations, we need that the rules of the PTRS
have these conditions integrated in their left-hand sides of the rules, i.e., if one wants
to check whether a number is zero or not, then one needs two different rules
f(0) -> ... and f(s(x)) -> ... to perform this case analysis.
However, in programs, conditions are mostly implemented by an if-construct, where one
could use, e.g., an
additional function gt to check whether a number is greater than another.
The same is true for conditions on other data structures than numbers, as we have seen above.
If one wants to check whether the list is empty or not, then without transformations, one needs two rules
(for nil and cons), whereas with transformations, one can use conditions and auxiliary
functions like empty.
The following PTRS (randNum03.ptrs) depicts the classical random walk, but we check the condition x > 0
not directly in the left-hand side of the rule but with an additional function gt(x,y)
which checks whether x > y.
Additionally, in order to decrease the value of a number by one, we use the predecessor function p(x) = x-1.
gt(0,0) -> 1 : false
gt(s(x),0) -> 1 : true
gt(0,s(y)) -> 1 : false
gt(s(x),s(y)) -> 1 : gt(x,y)
p(0) -> 1 : 0
p(s(x)) -> 1 : x
loop(x) -> 1 : if(gt(x, 0), x)
if(false, x) -> 1 : stop
if(true, x) -> 1 : loop(p(x)) || 1 : loop(s(x))
In this case, we need the rewriting processor to evaluate the
functions gt and p
and once again we need the rule overlap instantiation processor
to check for all possible terms that these functions can actually be applied on.
Whenever we have an ADP where the left-hand side of the rule is also contained in the support of the right-hand side,
then instantiations become useless, because we will always have at least the same ADP again after applying the processor.
For example, we need to apply one of the instantiation processors in order to prove
termination for the TRS with the rules f(x,y,z) -> g(x,y,z) and g(a,b,z) -> f(z,z,z).
If we make the rules probabilistic by adding the possibility to do nothing in a rewrite step with the probability 1/2,
then we result in the following PTRS.
f(x,y,z) -> 1 : g(x,y,z) || 1 : f(x,y,z)
g(a,b,z) -> 1 : f(z,z,z) || 1 : g(a,b,z)
This PTRS is iAST (since the original TRS was innermost terminating) but we are unable to show this
using the instantiation processor, because if one tries to instantiate any of the rules, this will result in at least
the same rule after the processor.
In contrast, if we consider nearly the same PTRS but the first rule remains the non-probabilistic rule f(x,y,z) -> 1 : g(x,y,z), then we are able to apply the instantiation processor and prove iAST using the ADP
Framework. (However, while instantiation does not help in our example above, we can prove
iAST using the rule overlap instantiation processor.)
Transformational processors are useful to perform a case analysis, but they do not suffice
for PTRSs where one needs inductive reasoning for the termination analysis.
For example, we cannot show iAST of the following PTRS (randNum09.prts) even though the
if-structure seems similar to the one of the
probabilistic quicksort example. This example was proposed to us by Johannes Niederhauser at the 0-th probabilistic termination competition in August 2023.
even(0) -> 1 : true
even(s(0)) -> 1 : false
even(s(s(x))) -> 1 : even(x)
loop(x) -> 1 : if(even(x), x)
if(false, x) -> 1 : stop
if(true, x) -> 1 : loop(x) || 1 : loop(s(x))
The idea here is that the recursion of loop stops if its argument is an even number.
If it is not even, then we either increase the value by 1 or use the same value again.
Here, a simple case analysis does not suffice, but we actually have to show (inductively),
that if a number x is odd, then x+1 is even.
This is not possible with the new transformational processors but needs other types of
processors for inductive reasoning.