Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

This web site contains additional information on our paper “Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs”. More precisely, we provide a longer version of our paper including all appendices, information on our implementation in the tool AProVE, and we describe our experiments.

Implementation in AProVE

The easiest way to run AProVE is via its web interface.

Moreover, recent releases of AProVE are available for download on GitHub. Release 7ba1745 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.

Input Syntax

Our implementation uses the input syntax of PTRSs that was first described in the paper ADY20, since up to now, this was the only tool that can analyze PTRSs. 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.

Since this syntax does not use the actual probabilities but rather computes them after summing all occurring numbers in a rule, this might be a little confusing to read. Hence, we also allow the following syntax for probabilistic rules:

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 for the input file and if the file does not contain the ‘STRATEGY’ keyword, then AProVE tries to prove the provided goal w.r.t. full rewriting.

Implementation

As described in the input syntax section, we only allow for rational probabilities. Internally, we store probabilities as 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.

For AST, we only use the direct application of polynomial interpretations as in Thm.17 of our paper, as the DP framework is not yet able to prove AST. For innermost AST (iAST), we first use the DP framework. If the DP framework is unable to prove iAST, then we use the direct application of polynomial interpretations again. The reason is that there exist examples that can only be proven by the direct application and not by the DP framework as discussed below.

The concrete implementation of the DP framework and the strategy behind the use of the different processors is very similar to the original non-probabilistic DP framework. We first use the processors that do not rely on finding an interpretation (i.e., every processor except the reduction pair processor) until we are unable to decrease the size of the problem any further. Then we use the reduction pair processor to delete some (or all) of the dependency tuples and then we use the other processors again. Furthermore, changing to the non-probabilistic DP framework if there are only trivial probabilities is always preferred over the probabilistic reduction pair processor.

For the dependency graph and the usable terms, AProVE uses the same over-approximations as for the dependency graph in the non-probabilistic setting.

For the reduction pair processor, we currently only search for polynomials with coefficients in the range {0,1,2} and if this fails we increase the range once to {0,…,10}. In the future, we will try to extend this to more advanced orders (like polynomials with real coefficients or matrix orderings as described in ADY20).

Finally, for PAST and innermost PAST (iPAST), we use the polynomial interpretation technique from ADY20 that is also implemented in the tool NaTT 2. However, in contrast to NaTT 2 we only consider natural polynomials and do not allow for rational or even real coefficients in the polynomials.

Web Interface

Our implementation can be tested via a web interface.

JAR File

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 rw1.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 rw1.ptrs -p plain

java -ea -jar aprove.jar -m wst rw1.ptrs -p html

Experiments

To evaluate the power of our approach we collected a set of 67 benchmarks based on different algorithms from the literature. The set of benchmarks can be found here. They consist of the following PTRSs:

For a more detailed explanation of every single benchmark see here.

In the table below, we compare AProVE’s results when applying polynomials directly (via our new Thm. 17) to prove AST (Direct Polo) with the results of our new probabilistic DP framework. The only other existing tool that can analyze PTRSs is NaTT 2. However, currently AProVE is the only tool that can analyze AST for PTRSs. NaTT 2 can only prove PAST and not AST. Since every PTRS that is PAST must also be AST, their approach can also be used on our examples. We also implemented their “PAST criterion” in our tool and added the results for our example data base to the table below. Note that some of our examples are only AST and not PAST, hence their approach cannot be used successfully on those examples.

Furthermore, we also performed experiments where we disabled individual processors of the probabilistic DP framework. More precisely, we disabled either the usable terms processor, both the dependency graph and the usable terms processor, or all processors except the reduction pair processor. You can find the detailed results for all of these different strategies here. The overall result is also given in the table below.

In all of our experiments, we search for polynomials with coefficients in the range {0,1,2} and if this fails we increase the range once to {0,…,10}, as we described in the implementation section.

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 for the DP framework and a successful AST proof for the direct application, the result MAYBE indicates that the tool crashed or terminated the verification process within the given time without a result. The result NO cannot occur, as there does not yet exist any processor to prove non-iAST (or non-AST).

As in TermComp, a timeout of 300 seconds was used. However, in our experiments AProVE never took longer than 15 seconds, since we have not yet adapted the DP transformations from the non-probabilistic to the probabilistic DP framework. Thus, our approach terminates directly if we cannot find an interpretation that can be used to delete at least a single dependency tuple and if the direct application of polynomial interpretations fails as well.


Example Program Terminating AST innermost AST DP Framework DP Framework (Time) Direct Polo Direct Polo (Time) PAST Criterion PAST Criterion (Time)
advantagePRP.ptrs YES YES YES YES 1.9 YES 2.1 YES 2.3
boundLoop0.ptrs NO YES YES YES 2.1 YES 4.1 MAYBE 2.0
boundLoop1.ptrs NO YES YES YES 2.5 MAYBE 1.7 YES 2.1
boundLoop2.ptrs NO YES YES YES 2.3 MAYBE 2.5 MAYBE 4.0
chainCritCompleteCounter0.ptrs NO YES YES MAYBE 2.1 YES 2.0 YES 5.5
chainCritCompleteCounter1.ptrs NO YES YES MAYBE 2.3 MAYBE 2.1 MAYBE 2.0
condLoop0.ptrs YES YES YES YES 2.7 MAYBE 2.1 MAYBE 2.5
condLoop1.ptrs NO YES YES MAYBE 2.2 MAYBE 2.3 MAYBE 5.6
condLoop2.ptrs NO YES YES YES 2.4 MAYBE 2.2 MAYBE 2.3
condLoop3.ptrs NO YES YES YES 2.3 YES 2.2 YES 2.2
condLoop4.ptrs NO YES YES YES 2.3 MAYBE 2.2 MAYBE 2.2
coupon.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.1
cowboyDuel.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.7
generate0.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.0
generate1.ptrs NO YES YES YES 2.8 YES 1.9 YES 2.2
generate2.ptrs NO YES YES YES 2.3 YES 2.0 YES 2.1
generate3.ptrs NO YES YES YES 2.1 MAYBE 2.2 MAYBE 2.1
generate4.ptrs YES YES YES YES 2.0 YES 2.0 YES 2.0
initialLoop0.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.0
initialLoop1.ptrs NO YES YES YES 2.9 MAYBE 2.1 MAYBE 2.0
initialLoop2.ptrs NO YES YES YES 2.2 MAYBE 2.2 MAYBE 2.0
initialLoop3.ptrs NO YES YES YES 2.2 MAYBE 2.1 MAYBE 2.0
lists0.ptrs NO YES YES YES 2.3 YES 4.4 YES 2.1
lists1.ptrs NO YES YES YES 2.7 MAYBE 4.2 MAYBE 4.2
lists2.ptrs NO YES YES YES 2.8 MAYBE 4.2 MAYBE 4.0
lists3.ptrs YES YES YES MAYBE 2.2 MAYBE 8.0 MAYBE 4.5
lists4.ptrs NO YES YES MAYBE 2.2 MAYBE 2.6 MAYBE 2.5
lists5.ptrs NO YES YES YES 2.0 YES 2.1 YES 2.3
lists6.ptrs NO YES YES YES 2.2 YES 2.0 YES 3.1
lists7.ptrs NO YES YES YES 2.3 MAYBE 2.4 MAYBE 2.4
lists8.ptrs NO YES YES YES 4.0 MAYBE 2.4 MAYBE 2.6
markovChain0.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.0
markovChain1.ptrs NO YES YES YES 2.1 YES 2.0 YES 5.3
markovChain2.ptrs NO YES YES YES 2.3 YES 2.0 YES 2.0
markovChain3.ptrs NO YES YES YES 2.3 MAYBE 2.0 MAYBE 3.2
markovChain4.ptrs NO YES YES YES 2.4 MAYBE 2.1 MAYBE 2.0
markovChain5.ptrs NO NO NO MAYBE 3.8 MAYBE 7.1 MAYBE 2.0
numbers0.ptrs NO YES YES YES 2.3 MAYBE 2.2 MAYBE 2.1
numbers1.ptrs NO YES YES YES 4.4 MAYBE 2.4 MAYBE 2.3
randSplayTree.ptrs YES YES YES YES 3.9 YES 1.8 YES 5.2
rw0.ptrs NO YES YES YES 2.1 YES 2.0 MAYBE 2.1
rw1.ptrs NO YES YES YES 2.0 YES 2.0 MAYBE 2.0
rw2.ptrs NO YES YES YES 2.1 YES 2.0 YES 2.0
rw3.ptrs NO NO NO MAYBE 2.1 MAYBE 2.0 MAYBE 2.0
rw4.ptrs NO NO YES YES 2.1 MAYBE 1.9 MAYBE 2.0
rw5.ptrs NO YES YES YES 2.0 MAYBE 2.0 MAYBE 2.0
rw6.ptrs NO YES YES YES 2.1 YES 2.0 YES 5.0
rw7.ptrs NO YES YES YES 2.2 MAYBE 2.0 MAYBE 2.0
rw8.ptrs NO YES YES YES 2.0 YES 1.9 MAYBE 3.0
rw9.ptrs NO YES YES MAYBE 2.1 YES 2.0 MAYBE 2.0
rw10.ptrs NO YES YES MAYBE 1.2 MAYBE 4.2 MAYBE 2.1
rwbin0.ptrs NO YES YES YES 2.4 YES 2.0 MAYBE 2.3
rwbin1.ptrs NO YES YES YES 2.2 YES 2.0 YES 2.1
rwbin2.ptrs NO YES YES YES 2.2 MAYBE 2.3 MAYBE 2.3
rwTree0.ptrs NO YES YES YES 2.2 MAYBE 2.2 MAYBE 5.1
rwTree1.ptrs NO YES YES YES 3.3 MAYBE 2.2 MAYBE 2.6
smallEx0.ptrs NO NO NO MAYBE 2.1 MAYBE 2.1 MAYBE 7.3
smallEx1.ptrs NO YES YES YES 2.1 MAYBE 2.0 MAYBE 2.0
smallEx2.ptrs NO NO YES YES 2.0 MAYBE 2.1 MAYBE 2.0
smallEx3.ptrs NO NO NO MAYBE 2.1 MAYBE 2.0 MAYBE 2.0
spline0.ptrs NO YES YES MAYBE 3.3 MAYBE 2.2 MAYBE 2.1
spline1.ptrs NO YES YES MAYBE 2.2 MAYBE 5.8 MAYBE 2.4
spline2.ptrs NO YES YES YES 2.2 YES 2.3 YES 2.1
spline3.ptrs NO YES YES MAYBE 2.5 MAYBE 2.2 MAYBE 2.1
strings0.ptrs NO YES YES YES 2.1 MAYBE 2.0 MAYBE 2.2
variableCond0.ptrs - - - MAYBE 1.7 MAYBE 4.4 MAYBE 0.4
variableCond1.ptrs - - - MAYBE 4.3 MAYBE 4.3 MAYBE 0.4


The following table shows the overall results of our main approaches compared to the PAST criterion.

Amount AST Amount iAST Amount YES DP Average Time DP Amount YES Polo Average Time Polo Amount YES PAST Crit Average Time PAST Crit
59 61 51 2.8 27 3.0 22 3.07

This shows that the PAST criterion is similar in power to our new AST criterion from Thm.17 on PTRSs that are actually PAST. However, on PTRSs that are only AST (e.g., rw0.ptrs), the PAST criterion cannot be used successfully. Hence, those examples show the real advantage of our new AST criterion of Thm.17. Moreover, the DP framework is clearly much more powerful than the direct application of polynomial orderings. The next table below shows the results for different strategies within the probabilistic DP framework. Here, “UTP” stands for the usable terms processor, “DPG” is the dependency graph processor, and “RPP” is the reduction pair processor.

Amount YES DP without UTP Average Time DP without UTP Amount YES DP without DPG+UTP Average Time DP without DPG+UTP Amount YES DP only RPP Average Time DP only RPP
48 2.55 48 2.92 46 2.75

Our experiments show that disabling processors indeed affects the power of the approach, in particular for larger examples with several defined symbols (e.g., then AProVE cannot prove iAST of the probabilistic quicksort example anymore). So all of our processors are needed to obtain a powerful technique for termination analysis of PTRSs.

Special Examples

Some of our examples demonstrate the strengths and the limits of the DP framework.

Leading Example, Ex. 23 (AST, but not terminating)

The leading example (numbers0.ptrs) from our paper is AST, but not terminating. Here, the direct application of polynomial interpretation via Thm. 17 fails, but the DP framework can prove almost-sure innermost termination automatically.

minus(x, 0)           -> 1 : x 
minus(s(x), s(y))     -> 1 : minus(x, y) 
div(0, s(x))          -> 1 : 0 
div(s(x), s(y))       -> 1/2 : s(div(minus(x, y), s(y))) || 1/2 : div(s(x), s(y))

Symmetric Random Walk, Ex. 10 (AST, but not PAST)

The following PTRS (rw8.ptrs) encodes a symmetric random walk which is AST, but not PAST. Here, both the DP framework and the direct application of polynomial interpretations via Thm. 17 succeed.

g(x)  -> 1/2 : x || 1/2 : g(g(x))

Quicksort, Sect. 5 and App. A.1 (AST, but not terminating)

The following PTRS (lists1.ptrs) is a probabilistic quicksort algorithm, where the random selection of the next pivot element does not terminate but is only AST.

rotate(nil)                 -> 1 : nil
rotate(cons(x,xs))          -> 1/2 : cons(x,xs) || 1/2 : rotate(app(xs, cons(x,nil)))

qs(nil)                     -> 1 : nil
qs(cons(x,xs))              -> 1 : qsHelp(rotate(cons(x,xs)))

qsHelp(cons(x,xs))          -> 1 : app(qs(low(x,xs)),cons(x,qs(high(x,xs))))

low(x,nil)                  -> 1 : nil
low(x,cons(y,ys))           -> 1 : ifLow(leq(x,y),x,cons(y,ys))

ifLow(true,x,cons(y,ys))    -> 1 : low(x,ys) 
ifLow(false,x,cons(y,ys))   -> 1 : cons(y,low(x,ys))

high(x,nil)                 -> 1 : nil
high(x,cons(y,ys))          -> 1 : ifHigh(leq(x,y),x,cons(y,ys))

ifHigh(true,x,cons(y,ys))   -> 1 : cons(y,high(x,ys)) 
ifHigh(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))

We find the next pivot element by rotating the list a random number of times. Once we stop this rotation, we use the current head as the next pivot element. Thm. 17 fails to prove iAST for such a complex example. On the other hand, the DP framework is able to prove iAST because of its modularity. The DP framework splits this problem into 6 different sub-problems using the dependency graph. Afterwards, it analyzes the sub-problems on their own. For 4 of them, it can remove the probabilistic rotate-rules completely via the usable rules processor. Hence, here it can use the non-probabilistic DP framework instead via the probability removal processor.

For the sub-problem containing the dependency tuple resulting from the rotate-rules and for the sub-problem with the dependency tuples from the qs- and qsHelp-rules, the probabilistic reduction pair processor is used to prove that they are iAST.

DP Framework works only for iAST, R2, Sect. 4.1

The following PTRS (smallEx2.ptrs) shows why our framework can currently only deal with iAST instead of (full) AST.

g    -> 1/2 : O || 1/2 : h(g)
h(x) -> 1 : f(x,x,x)

This PTRS is not AST, because we can always apply the h-rule directly after applying the g-rule, which would correspond to the following PTRS.

g    -> 1/2 : O || 1/2 : c(g,g,g)

This is a biased random walk, where we decrease the number of g’s in a term with a chance of 1/2 by 1 and increase the number by 2 also with a chance of 1/2. Hence, this PTRS (and hence, also our original PTRS) are not AST.

However, our original PTRS is iAST, because when we are restricted to the innermost strategy, then we are not able to use the h-rule on terms that contain a g. In contrast, the h-rule can now only be used to copy normal forms.

The dependency tuples for this PTRS are

<G,g>        -> 1/2 : <c0,0> || 1/2 : <c2(H(g),G),h(g)>
<H(x),h(x)>  -> 1 : <c0,f(x,x,x)>

As one can see, the first component of the H-dependency tuple is the compound term c0 without any arguments. This dependency tuple would be deleted directly by the dependency graph. But then, there is no way to duplicate g terms anymore and hence, the proof of iAST succeeds.

So in order to modify the DP framework into a technique which proves (full) AST, one has to come up with a new definition of chains and new definitions for most of the processors.

Dependency Pairs vs Dependency Tuples for the RPP, App. A.2

The following PTRS (advantageRPP.ptrs) shows why dependency pairs are easier to handle within the reduction pair processor than dependency tuples.

g(s(x)) -> 1 : f(g(x),g(x),g(x))

If one regards this system as a non-probabilistic TRS, then one obtains the following dependency pair

G(s(x)) -> 1 : G(x)

In contrast, when regarding it as a PTRS, we obtain the following dependency tuple

<G(s(x)),g(s(x))> -> 1 : <c3(G(x),G(x),G(x)),f(g(x),g(x),g(x))>

If we restrict ourselves to linear natural polynomial interpretations, then we can orient the dependency pair strictly (and the original rewrite rule weakly) using an interpretation with coefficients in the range {0,1}. We can simply map s(x) to x+1, G(x) to x, and both g(x) and f(x,y,z) to 0. On the other hand, in order to orient the dependency tuple strictly (and the original rewrite rule weakly), we have to ensure that the first component is strictly decreasing, i.e., Pol(G(s(x))) > Pol(c3(G(x),G(x),G(x))). This is only possible with an interpretation using coefficients in the range {0,1,2,3}. Then we can map s(x) to 3x+1, G(x) to x, and again both g(x) and f(x,y,z) to 0.

If one modifies the example such that the right-hand side contains k occurrences of g(x), then the reduction pair processor for dependency tuples needs coefficients from {0,…,k}, while the reduction pair processor for dependency pairs still succeeds with coefficients in the range {0,1}. Since a wider range for the coefficients means a bigger search space, in general the use of dependency tuples can increase the runtime to search for satisfying polynomial interpretations significantly.

Direct Application vs. DP Framework, App. A.3

The following PTRS (rw9.ptrs) describes a random walk that increases or decreases the number of g’s in a term by 2 with a chance of 1/2. Hence, this PTRS is AST as it corresponds to a fair random walk.

g(g(x)) -> 1/2 : g(g(g(g(x)))) || 1/2 : x

The direct application of polynomial interpretations in Thm. 17 can prove its almost-sure termination using the polynomial interpretation that maps g(x) to the polynomial x+1.

However, currently the DP framework fails in proving iAST. We would first create the following DP tuple for the only rule:

<G(g(x)), g(g(x))> -> 1/2 : <c(G(g(g(g(x)))),G(g(g(x))),G(g(x)),G(x)), g(g(g(g(x))))> || 1/2 : <c,x>

Now, the terms G(g(g(x))) and G(x) are not usable and can be removed by the usable terms processor. Thus, we result in the following DP tuple:

<G(g(x)), g(g(x))>  -> 1/2 : <c(G(g(g(g(x)))),G(g(x))), g(g(g(g(x))))> || 1/2 : <c,x>

At this point we cannot apply any processor except the reduction pair processor. But the reduction pair processor is also unable to find an interpretation for this dependency tuple and we abort the proof. The reason is that we have to take the sum of the polynomial values of the terms G(g(g(g(x)))) and G(g(x)), since they both occur as arguments of the same compound symbol. With the direct application of polynomials, we only have to regard the polynomial value of g(g(g(g(x)))).

Note that the alternative idea of interpreting compound symbols by the maximum instead of the sum is not sound in the probabilistic setting, since in this way one cannot distinguish anymore between examples like R1 and R2 in Sect. 4.1 of our paper, where R1 is AST and R2 is not AST.

For that reason, our implementation uses both the DP framework and the direct application of polynomial interpretations for PTRSs. In future work, we plan to integrate the direct approach into the DP framework by adapting the Rule Removal Processor of the non-probabilistic DP framework.

Incompleteness of the Probabilistic Chain Criterion, App. A.4

The following PTRS (chainCritCompleteCounter0.ptrs) is not only another example that can only be handled by Thm. 17 and not by the DP framework. Moreover, it shows that the chain criterion as described in the paper is not complete.

(1) g     -> 5/8 : f(g) || 3/8 : stop
(2) g     -> 1 : b
(3) f(b)  -> 1 : g

On the one hand, we are able to prove AST via Thm. 17 with the polynomial interpretation that maps f(x) to x + 2, g to 4, b to 3, and stop to 0. On the other hand, the dependency tuples for this PTRS have the form:

(DT(1)) <G,g>         -> 5/8 : <c2(F(g),G),f(g)> || 3/8 : <c0,stop>
(DT(2)) <G,g>         -> 1 : <c0,b>
(DT(3)) <F(b),f(b)>   -> 1 : <c1(G),g>

Now the DP problem (DT(R),R) is not iAST anymore. To see this, consider the following rewrite sequence

           1  : c1(G)
->(DT(1)) 5/8 : c2(F(g),G)  || 3/8 : c0
->((2))   5/8 : c2(F(b),G)  || 3/8 : c0
->(DT(3)) 5/8 : c2(G,G)     || 3/8 : c0

Using these combinations of steps with the dependency tuples (1) and (3) and the probabilistic rewrite rule (2) we essentially end up with a biased random walk with p = 5/8 > 1/2. Hence, (DT(R),R) is not iAST anymore. The problem here is that the terms G and F(g) can both be rewritten to G. When creating the dependency tuples, we lose the information that the g inside the term F(g) corresponds to the second argument G of the compound symbol. In order to obtain a complete chain criterion, one has to extend dependency tuples by positions. Then the second argument G of the compound symbol would be augmented by the position of g in the right-hand side of the rule (1), because this rule was used to generate the dependency tuple.

The Limits of the DP Framework, App. A.5

The following PTRS (lists4.ptrs) describes an implementation of bogosort.

bogo(xs)                          -> 1 : bogohelp(sortR(xs))
bogohelp(xs)                      -> 1 : ifSorted(xs,xs)

sortR(nil)                        -> 1 : nil
sortR(cons(x,nil))                -> 1 : cons(x,nil)
sortR(cons(x,cons(y,xs)))         -> 1/2 : cons(x,sortR(cons(y,xs))) || 1/2 : cons(y,sortR(cons(x,xs)))

ifSorted(nil,zs)                  -> 1 : zs
ifSorted(cons(x,nil),zs)          -> 1 : zs
ifSorted(cons(x,cons(y,ys)),zs)   -> 1 : ifLeq(leq(x,y),cons(y,ys),zs)

ifLeq(true,cons(y,xs),zs)         -> 1 : ifSorted(cons(y,xs),zs)
ifLeq(false,cons(y,xs),zs)        -> 1 : bogo(zs)

leq(0,x)                          -> 1 : true 
leq(s(x),0)                       -> 1 : false
leq(s(x),s(y))                    -> 1 : leq(x,y)

Here, we randomly shuffle the list until we eventually reach a sorted list and stop. This PTRS is AST as in every recursive call of the main function bogo, we use the function sortR that randomly switches some neighboring elements of the list. Hence, there is a certain chance to move towards a ‘more sorted’ list so that we eventually stop the algorithm. However, in order to prove this via the reduction pair processor or via our new Thm. 17, we would have to find an ordering that distinguishes between lists that are ‘more sorted’ than others. Polynomial interpretations are not able to express this comparison by ‘more sortedness’ and this also holds for most other typical orderings on terms that are amenable to automation.

Polynomial AST Criterion vs. PAST Criterion

The following PTRS (boundloop1.ptrs) shows that there are examples where the direct application of polynomial interpretations in ADY20 can prove PAST, whereas our direct application of polynomial interpretations in Thm.17 to prove AST fails.

(1) decreaseX(0, y)     -> 1 : loopGuard(0, y)
(2) decreaseX(s(x), y)  -> 1 : loopGuard(x, y)
(3) loop(x, y)          -> 1/2 : decreaseX(x, y) || 1/2 : decreaseY(x, y)
(4) loopGuard(s(x), y)  -> 1 : loop(s(x), y)
(5) loopGuard(0, 0)     -> 1 : stop
(6) decreaseY(x, 0)     -> 1 : loopGuard(x, 0)
(7) decreaseY(x, s(y))  -> 1 : loopGuard(x, y)
(8) loopGuard(x, s(y))  -> 1 : loop(x, s(y))

The PAST criterion finds the following polynomial interpretation that proves PAST:

    POL(0) = 0
    POL(decreaseX(x_1, x_2)) = 2 + x_1 + 2*x_1*x_2 + 3*x_2
    POL(decreaseY(x_1, x_2)) = 2 + 3*x_1 + x_1*x_2 + x_2
    POL(loop(x_1, x_2)) = 4 + 2*x_1 + 2*x_1*x_2 + 2*x_2
    POL(loopGuard(x_1, x_2)) = 1 + 3*x_1 + 3*x_1*x_2 + 3*x_2
    POL(s(x_1)) = 4 + 3*x_1
    POL(stop) = 0

If we take a closer look at rule (3), we can see that the expected value is indeed strictly decreasing:

    4 + 2x + 2xy + 2y    > 1/2*(2 + x + 2xy + 3y) + 1/2*(2 + 3x + xy + y) = 2 + 2x + 1.5xy + 2y
    loop(x, y)          -> 1/2 : decreaseX(x, y) || 1/2 : decreaseY(x, y)

However, our criterion of Thm.17 cannot be applied with this polynomial interpretation. We have neither a strict decrease from loop(x, y) to decreaseX(x,y) (since 4 + 2x + 2xy + 2y is not greater than 2 + x + 2xy + 3y) nor from loop(x, y) to decreaseX(x,y) (since 4 + 2x + 2xy + 2y is not greater than 2 + 3x + xy + y). Indeed, the implementation of our AST criterion from Thm.17 fails for this example, as it does not find any polynomial interpretation satisfying its constraints. However, we can prove AST using the probabilistic DP framework.