In the paper Deciding Innermost Loops,
we present the first method to disprove innermost termination
of term rewrite systems automatically. The paper introduces a suitable
notion of an innermost loop and shows how to detect such an innermost
loop: One can start with any technique amenable to detect loops.
Then our novel procedure can be applied to decide whether a given
loop is an innermost loop.
In our experiments, we want to assess the power of our new method.
Therefore, we compare it to existing techniques to detect non-termination
for full rewriting, as used by various tools in the previous
termination competition.
We are not aware of any other existing
tool for disproving innermost termination.
Implementation in AProVE
We integrated our approach in the
termination tool AProVE. To experiment with this new version of AProVE,
please use the AProVE web
interface.
Examples and Settings
We tested the new version of AProVE
on the Termination Problem Data Base (TPDB) 4.0.
The TPDB is the collection
of problems used in the annual International Termination Competition.
In our experiments below, we regard the
129 TRSs from the TPDB where at least one tool has been able to disprove termination in the
competition in 2007.
As we want to determine the power of our method for disproving innermost termination,
we transformed these termination problems into termination problems for
innermost rewriting (by adding
the declaration "(STRATEGY INNERMOST)" to the top of the file).
For our experiments, AProVE was run on Dual Intel Xeons at 2.33 GHz.
For each example, we imposed a time limit of 60 seconds (corresponding to the way
tools were evaluated in most of the previous competitions).
Of course AProVE can also disprove innermost termination of Example 1 from
the paper. Please click on
the following button to load the TRS into the web interface:
Experiments
In the following table, we list the results of the new AProVE version
on the 129 examples described above. The result "NO" means that
innermost termination could be disproved while "YES" indicates
that the example could be shown to be innermost terminating.
The result "MAYBE" means that no proof was found
and "KILLED" indicates a time-out. Please click on any example to
load it into the AProVE web interface (one has to insert the line
"(STRATEGY INNERMOST)" manually) or on the indicated runtime
to view the proof.
The below table clearly demonstrates the power of our method. With the
results of this paper, AProVE now also disproves innermost termination for
93 of these 129 TRSs. Note that from the remaining 36 TRSs at least 30 are
innermost terminating.