Wanda experiments for FSCD 2020

These experiments were done for the paper WANDA – a Higher Order Termination Tool, presented at FSCD 2020. All experiments were performed with Wanda version 2.2, on a 60 second timeout.

We performed four series of experiments, three of which are (patially) noted in the paper. In the first, we evaluated WANDA on the Termination Problem Database (TPDB), version 10.6. We used various configurations, to evaluate the power of various techniques described in the paper. This gives the following results:

The second set of experiments is not included in the paper. This set of experiments considers the TPDB without the two subdirectories Uncurried_Applicative_11 and Hamana_Kikuchi_18. The reason for this separation is that those two directories seem to contain largely generated benchmarks – there is a lot of repetition of the same few rules (mostly fold, rec and map), coupled with different first-order systems or called in slightly different ways. While it is interesting to see how tools perform on these variations, it does carry a significant risk of skewing the results. So, we isolated the results on the remaining benchmarks, which allows us to more accurately assess the power on truly higher-order systems. This gives the following results:

As the remaining benchmarks do not have a significant first-order section, the first-order tool makes very little difference. It is also notable that StarHorpo and Polynomial Interpretations perform much more equally, as do static and dynamic dependency pairs.

The third set of experiments is mentioned in the paper, although the tables were not included. This set of experiments tests WANDA's performance when coupled with different first-order termination back-ends. The first three tests couple WANDA with AProVE, NaTT and MU-TERM respectively for both termination and non-termination; the last test uses NaTT for termination and AProVE for non-termination. The first table below considers all benchmarks in the TPDB; the second table considers all except the most recently added category, since the difference is remarkable.

It is notable that NaTT's advantage is very local; on the benchmarks in the 2017 TPDB, all three tools perform equally. It seems likely that later updates of MU-TERM and AProVE will also handle the tools in Hamana_Kikuchi_18/. Otherwise, what we can observe by investigating the cases where a first-order tool is needed to conclude YES is that all these benchmarks have a simple higher-order part: in all cases, a proof with static dependency pairs and the subterm criterion (or computable subterm criterion) suffices for the higher-order part. This may suggest that using a first-order tool for termination analysis is not worthwhile when the higher-order part has a different form. However, it might also just be a case of the database: for most benchmarks, a first-order tool is not needed at all, and the few where it is needed here are not a sufficiently diverse sample space to confidently draw any conclusions.

The final set of experiments considers WANDA's power on the Confluence Problems database (COPS), 2019 version. As WANDA cannot read HRS input, the benchmarks were converted by CSI^ho, with some manual changes (this was necessary because, due to lacking documentation on WANDA's input restrictions, some of the generated AFSMs could not be read by WANDA). We used the same configurations as before, except the "simplifying fake patterns" configuration, which only makes sense for AFS input.

The longer average time when using dependency pairs is largely due to a single benchmark (433) for which rule removal is very effective, but which the non-monotonic reduction pair processor takes much longer to handle.