Context-sensitive dependency pairs (CS-DPs) are currently the most
powerful method for automated termination analysis of
context-sensitive rewriting. However, compared to DPs for ordinary
rewriting, CS-DPs suffer from two main drawbacks:
CS-DPs can be collapsing. This complicates the handling
of CS-DPs and makes them less powerful in practice.
There does not exist a "DP framework" for CS-DPs which would
allow to apply them in a flexible and modular way.
In the paper
Improving Context-Sensitive Dependency Pairs,
we solve Drawback (a) by
introducing a new definition of CS-DPs. With our definition, CS-DPs
are always non-collapsing and, thus, they can be handled like
ordinary DPs. This allows us to solve Drawback (b) as well, i.e.,
we extend the existing DP framework for ordinary DPs to
context-sensitive rewriting.
Implementation in AProVE
We have integrated our approach
into the automated termination prover AProVE.
To experiment with this new version of
AProVE, please use the AProVE
web interface.
Examples and Settings
In our experiments below, we want to assess the power of our new method.
Therefore, we tested the new version of AProVE
on the Termination Problem Data Base (TPDB) 4.0.
This is the collection of problems used in the annual International
Termination Competition 2007. We compared the performance of our
new version of AProVE against Mu-Term 4.5a.
This version is identical in power to Mu-Term 4.4 that was the
most powerful tool for context-sensitive rewriting in
the termination competition 2007.
For our experiments, both tools were run on Dual Intel Xeons at 2.33 GHz.
For each example, we imposed a time limit of 120 seconds (corresponding to the way
tools were evaluated in the termination competition 2007).
Results and Discussion
While Mu-Term 4.5a was the most powerful tool for termination analysis of
context-sensitive rewriting up to now, due to
our new notion of CS-DPs, AProVE has become substantially more
powerful. For instance, AProVE automatically proves termination of our leading
example from the paper, whereas Mu-Term fails.
Please click on the following button to load the the leading example
into AProVE's web interface: