TNT is a tool developed by
Germán Vidal and
Naoki Nishida
to analyze the termination of
narrowing.
It takes a term-rewriting system (TRS) and a sequence of
abstract terms
that specify which arguments are ground for some
user-defined functions; for instance, the abstract term
append(g,v) specifies that the first argument of
function append is
ground and the second one is possibly a variable.
This is similar to the notion of "modes" in logic programming.
The transformation then proceeds
basically as follows:
First, a "safe" argument filtering is inferred, i.e., a mapping that
specifies which are the ground arguments of every user-defined function
in every possible narrowing computation (starting from any possible
instance of the abstract term).
Optionally, you can check the 'labeling' box so that some rules
of the original TRS may be duplicated and labeled. This pre-processing
produces more
accurate results in some cases (check, e.g., the example
labeling/test.trs with and without labeling).
Also, you can check the box 'deletion of non-reachable rules'
so that some rules which are not reachable from the abstract
term are deleted.
Then, the (possibly labeled) TRS is transformed so that only the
ground arguments
of user-defined functions remain and, most importantly, so that the
termination of the transformed TRS implies the termination of
the original TRS.
Therefore, once the (possibly) non-ground arguments are filtered away,
the termination of the transformed program can be analyzed with any
termination prover for TRSs,
like AProVE
A more detailed account of the technique can be found in this
paper
You can either write down the initial TRS or choose one from (a small
selection of) the termination problem
database (and then edit it). TRSs should basically follow the
syntax of TRS
input files (with some restrictions, e.g., the specification of a
"strategy" is not allowed).
Once the TRS is loaded in, you can provide an abstract call (e.g., a
call of the form app(g,v) in TRS
tpdb-4.0/TRS/AG01/#3.12.trs or take(g,g,v) in TRS
tpdb-4.0/TRS/SchneiderKamp/trs/otto02.trs, etc) and press the
"Filter TRS" button to get the transformed TRS.
Initial TRS
Transformed TRS
Choose a file:
Abstract call:
Now you can use any termination prover for TRSs in order to
analyze the termination of the transformed TRS (e.g.,
AProVE).
Or you can simply click
to check the termination of the transformed
TRS using the web interface of the AProVE termination prover (using a
fixed timeout of 60 secs).
Contact me at gvidal at dsic.upv.es if you want
the source code.