JAIST Repository
https://dspace.jaist.ac.jp/

Title

Tyrolean Termination Tool

Author(s)Hirokawa, Nao; Middeldorp, Aart

Citation

Lecture Notes in Computer Science, 3467/2005:
175‑184

Issue Date

2005

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/9058

RightsThis is the author‑created version of Springer,
Nao Hirokawa and Aart Middeldorp, Lecture Notes
in Computer Science, 3467/2005, 2005, 175‑184.
The original publication is available atwww.springerlink.com,
http://dx.doi.org/10.1007/b135673

Description

Proceedings of the 16th International Conference,
RTA 2005, Nara, Japan, April 19‑21, 2005.

Japan Advanced Institute of Science and Technology

Tyrolean Termination Tool?
Nao Hirokawa and Aart Middeldorp
Institute of Computer Science
University of Innsbruck
6020 Innsbruck, Austria{nao.hirokawa,aart.middeldorp}@uibk.ac.at

1

Introduction

This paper describes the Tyrolean Termination Tool (TTT in the sequel), thesuccessor of the Tsukuba Termination Tool [12]. We describe the differences
between the two and explain the new features, some of which are not (yet) available in any other termination tool, in some detail. TTT is a tool for automaticallyproving termination of rewrite systems based on the dependency pair methodof Arts and Giesl [3]. It produces high-quality output and has a convenient webinterface. The tool is available at
http://cl2-informatik.uibk.ac.at/ttt
TTT incorporates several new improvements to the dependency pair method. In
addition, it is now possible to run the tool in fully automatic mode on a collectionof rewrite systems. Moreover, besides ordinary (first-order) rewrite systems, thetool accepts simply-typed applicative rewrite systems which are transformed into
ordinary rewrite systems by the recent method of Aoto and Yamada [2].
In the next section we describe the differences between the semi automatic
mode and the Tsukuba Termination Tool. Section 3 describes the fully automaticmode. In Section 4 we show a termination proof of a simply-typed applicative
system obtained by TTT. In Section 5 we describe how to input a collection ofrewrite systems and how to interpret the resulting output. Some implementation
details are given in Section 6. The final section contains a short comparison withother tools for automatically proving termination.

2

Semi Automatic Mode

Figure 1 shows the web interface.
This menu corresponds to the options that were available in the Tsukuba
Termination Tool. A first difference is that we now support the dependency pairmethod for innermost termination [3]. A second difference is that dependency
A preliminary description of the Tyrolean Termination Tool appeared in theproceedings of the 7th International Workshop on Termination, Technical Report
AIB-2004-07, RWTH Aachen, pages 249–268, 2004.

Fig. 1. A screen shot of the semi automatic mode of TTT.

pairs that are covered by the subterm criterion of Dershowitz [7] are excluded.
The other differences are described in the following paragraphs.
First of all, when approximating the (innermost) dependency graph the original estimations of [3] are no longer available since the approximations describedin [15] generally produce smaller graphs while the computational overhead is
negligible.
Secondly, the user can no longer select the cycle analysis method (all cycles separately, all strongly connected components separately, or the recursive
SCC algorithm of [15]). Extensive experiments reveal that the latter method
outperforms the other two, so this is now the only supported method in TTT.
Finally, the default method to search for appropriate argument filterings has
been changed from enumeration to the divide and conquer algorithm of [15].
By using dynamic programming techniques, the divide and conquer method
has been improved (cf. [15]) to the extent that for most examples it is more
efficient than the straightforward enumeration method. Still, there are TRSs
where enumeration is more effective, so the user has the option to change thesearch strategy (by clicking the enumerate box).
2

New features include (1) a very useful criterion based on the subterm relation
to discard SCCs of the dependency graph without considering any rewrite rulesand (2) a very powerful modularity criterion for termination inspired by theusable rules of [3] for innermost termination. These features are described indetail in [13]. The first one is selected by clicking the subterm criterion box
and the second by clicking the usable rules box. In addition, linear polynomialinterpretations with coefficients from {−1, 0, 1} can be used as base order. In[14] it is explained how polynomial interpretations with negative coefficients,
like x − 1 for a unary function symbol or x − y for a binary function symbol, canbe effectively used in connection with the dependency pair method.

3

Fully Automatic ModeIn this mode TTT uses a simple strategy to (recursively) solve the ordering constraints for each SCC of the approximated dependency graph. The strategy isbased on the new features described in the previous section and uses LPO (bothwith strict and quasi-precedence) with some argument filterings [15] and linear
polynomial interpretations with coefficients from {−1, 0, 1} as base orders.
After computing the SCCs of the approximated (innermost) dependency
graph, the strategy subjects each SCC to the following algorithm:
1. First we check whether the new subterm criterion is applicable.
2. If the subterm criterion was unsuccessful, we compute the usable rules.
3. The resulting (usable rules and dependency pairs) constraints are subjectedto the natural (see [14]) polynomial interpretation with coefficients from{0, 1}.
4. If the constraints could not be solved in step 3, we employ the divide andconquer algorithm for computing suitable argument filterings with respect
to the some heuristic [15] and LPO with strict precedence.
5. If the previous step was unsuccessful, we repeat step 3 with arbitrary polynomial interpretations with coefficients from {0, 1}.
6. Next we repeat step 4 with the variant of LPO based on quasi-precedences
and a small increase in the search space for argument filterings (see below).
7. If the constraints could still not be solved, we try linear polynomial interpretations with coefficients from {−1, 0, 1}.
If only part of an SCC could be handled, we subject the resulting new SCCs
recursively to the same algorithm.
If the current set of constraints can be solved in step 3 or 4, then they canalso be solved in step 5 or 6, respectively, but the reverse is not true. The sole
reason for adopting LPO and polynomial interpretations in alternating layers
is efficiency; the search space in steps 3 and 4 is significantly smaller than insteps 5 and 6. The reason for putting the subterm criterion first is that with thiscriterion many SCCs can be eliminated very quickly, cf. the third paragraph of
Section 6. The extension of the search space for argument filterings mentioned instep 6 is obtained by also considering the full reverse argument filtering [n, . . . , 1]
3

Fig. 2. Output produced by TTT.

for every n-ary function symbol. The advantage of this extension is that there
is no need for a specialized version of LPO with right-to-left status.
The effectiveness of the automatic strategy can be seen from the data presented in Figure 2, which were obtained by running TTT in fully automatic modeon the 89 terminating TRSs (66 in Section 3 and 23 in Section 4) of [4]. An explanation of the data is given in Section 5.
Our automatic strategy differs from the “Meta-Combination Algorithm” described in [11]; we avoid transforming SCC constraints using techniques likenarrowing and instantiation because they tend to complicate the produced termination proofs. Instead, we rely on techniques (subterm criterion and polynomial interpretations with negative coefficients) that lead to termination proofs
that are (relatively) easy to understand.
4

4

Simply-Typed Applicative Rewrite Systems

Besides ordinary first-order TRSs, TTT accepts simply-typed applicative rewrite
systems (STARSs) [1]. Applicative terms are built from variables, constants,
and a single binary operator ·, called application. Constants and variables areequipped with a simple type such that the rewrite rules typecheck. A typicalexample is provided by the following rules for the map function(map · f ) · nil → nil(map · f ) · ((cons · x) · y) → (cons · (f · x)) · ((map · f ) · y)with the type declaration nil : α, cons : β → α → α, map : (β → β) → α → α,
f : β → β, x : β, and y : α. Here α is the list type and β the type of elements oflists. STARSs are useful to model higher-order functions in a first-order setting.
As usual, the application operator · is suppressed in the notation and parentheses
are removed under the “association to the left” rule. The above rules then become
map f nil → nil
map f (cons x y) → cons (f x) (map f y)
This corresponds to the syntax of STARSs in TTT. The types of constants must
be declared by the keyword TYPES. The types of variables is automatically inferred when typechecking the rules, which follow the RULES keyword. So theabove STARS would be inputted to TTT as
TYPES
nil : acons : b => (a => a)
map : (b => b) => a => a

;
;
;

RULES
map f nil-> nil;map f (cons x y) -> cons (f x) (map f y) ;In order to prove termination of STARSs, TTT uses the two-phase transformation developed by Aoto and Yamada [2]. In the first phase all head variables(e.g. f in f x) are removed by the head variable instantiation technique. The
soundness of this phase relies on the ground term existence condition, which basically states that all simple types are inhabited by at least one ground term.
Users need not be concerned about this technicality as TTT automatically adds
fresh constants of the appropriate types to the signature so that the ground term
existence condition is satisfied. (Moreover, the termination status of the original
STARS is not affected by adding fresh constants.) After the first phase an ordinary TRS is obtained in which the application symbol is the only non-constantsymbol. Such TRSs are not easily proved terminating since the root symbol ofevery term that has at least two symbols is the application symbol and thus
provides no information which could be put to good use. In the second phase5

applicative terms are transformed into ordinary terms by the translation to functional form technique. This technique removes all occurrences of the application
symbol. We refer to [2] for a complete description of the transformation. We
contend ourselves with showing the Postscript output (in Figure 3) producedby TTT on the following variation of combinatory logic (inspired by a recent
question posted on the TYPES Forum by Jeremy Dawson):
TYPES
I : o => o;
W : (o => o => o) => o => o;
S : (o => o => o) => (o => o) => o => o ;
RULES
I x
-> x
;
W f x
-> f x x;
S x y z -> x z (y z) ;Note that the types are crucial for termination; the untyped version admits thecyclic rewrite step W W W → W W W.

5

A Collection of Rewrite Systems as Input

Single TRSs (or STARSs) are inputted by typing (the type declarations and)the rules into the upper left text area or by uploading a file via the browse
button. Besides the original TTT syntax (which is obtained by clicking the TRSlink), TTT supports the official format1 of the Termination Problems Data Base.
The user can also upload a zip archive. All files ending in .trs are extracted
from the archive and the termination prover runs on each of these files in turn.
The results are collected and presented in two tables. The first table lists foreach TRS the execution time in seconds together with the status: bold green
indicates success, red italics indicates failure, and gray indicates timeout. By
clicking green (red ) entries the user can view the termination proof (attempt)
in HTML or high-quality Postscript format. The second table gives the numberof successes and failures, both with the average time spent on each TRS, thenumber of timeouts, and the total number of TRSs extracted from the zip archive
together with the total execution time. Figure 2 shows the two tables for the 89
terminating TRSs in Sections 3 and 4 of [4]. Here we used TTT’s fully automatic
mode with a timeout of 1 second (for each TRS). The experiment was performed
on a PC equipped with a 2.20 GHz Mobile Intel Pentium 4 Processor - M and512 MB of memory, using native-compiled code for Linux/Fedora.
1

http://www.lri.fr/~marche/wst2004-competition/format.html

6Termination Proof Scripta
Consider the simply-typed applicative TRS
Ix → x
Wf x → f xx
S x y z → x z (y z)over the signature I : o ⇒ o, W : (o ⇒ o ⇒ o) ⇒ o ⇒ o, and S : (o ⇒ o ⇒ o) ⇒(o ⇒ o) ⇒ o ⇒ o. In order to satisfy the ground term existence condition we extend
the signature by c : o ⇒ o ⇒ o and c0 : o. Instantiating all head variables yields thefollowing rules:
Ix → xWcx → cxx
S c I z → c z (I z)
S c (W w) z → c z (W w z)
S c (S w v) z → c z (S w v z)
S c (c w) z → c z (c w z)
By transforming terms into functional form the TRS
1:I1 (x) → x

2:W2 (c, x) → c2 (x, x)

3:S3 (c, I, z) → c2 (z, I1 (z))

4:S3 (c, W1 (w), z) → c2 (z, W2 (w, z))

5:S3 (c, S2 (w, v), z) → c2 (z, S3 (w, v, z))

6:

S3 (c, c1 (w), z) → c2 (z, c2 (w, z))

is obtained. There are 3 dependency pairs:
7:S]3 (c, I, z) → I]1 (z)8:S]3 (c, W1 (w), z) → W2] (w, z)

9:S]3 (c, S2 (w, v), z) → S]3 (w, v, z)

The approximated dependency graph contains one SCC: {9}.
– Consider the SCC {9}. By taking the simple projection π with π(S]3 ) = 2, thedependency pair simplifies to
9:

S2 (w, v) → v

and is compatible with the proper subterm relation.
aTyrolean Termination Tool (0.03 seconds) — November 18, 2004
Fig. 3. Example output.

7

6

Some Implementation Details

The web interface of TTT is written in Ruby2 and the termination prover underlying TTT is written in Objective Caml (OCaml),3 using the third-party libraries4
findlib, extlib, and pcre-ocaml. We plan to make the OCaml source code
available in the near future.
The termination prover consists of about 13,000 lines of OCaml code. About
20% is used for the manipulation of terms and rules. Another 15% is devoted
to graph manipulations. This part of the code is not only used to computedependency graph approximations, but also for precedences in KBO and LPO,
and for the dependency relation which is used to compute the usable rules. The
various termination methods that are provided by TTT account for less than
10% each. Most of the remaining code deals with I/O: parsing the input andproducing HTML and Postscript output. For the official Termination Problems
Data Base format we use parsers written in OCaml by Claude Marché. A richOCaml library for the manipulation of terms (or rose trees) and graphs would
have made our task much easier!
It is interesting to note that two of the original techniques that make TTT
fast, the recursive SCC algorithm and the subterm criterion, account for just
13 and 20 lines, respectively. Especially the latter should be the method offirst choice in any termination prover. To wit, of the 628 (full) termination
problems for pure first-order term and string rewrite systems in the Termination
Problems Data Base, 215 are proved terminating by the subterm criterion; thetotal time to check the whole collection is a mere 32 seconds (on the architecture
mentioned in the previous section). Several of these 215 rewrite systems cannot
be proved terminating by the latest release of CiME [5]. (See the next section
for a comparison between TTT and other termination provers.)
Concerning the implementation of simply-typed applicative rewrite systems,
we use the Damas-Milner type reconstruction algorithm (see e.g. [17]) to infer
the types of variables.
We conclude this section with some remarks on the implementation of baseorders in TTT. The implementation of LPO follows [12] but we first check whether
the current pair of terms can be oriented by the embedding order in every recursive call to LPO. This improves the efficiency by about 20%. The implementationof KBO is based on [16]. We use the “method for complete description” [8] tocompute a suitable weight function. The implementation of polynomial interpretations with coefficients from {0, 1} is based on [6, Figure 1] together with thesimplification rules described in Section 4.4.1 of the same paper. The current
implementation of polynomial interpretations with coefficients from {−1, 0, 1}
in TTT is rather naive. We anticipate that the recent techniques of [6] can beextended to handle negative coefficients.
2

http://www.ruby-lang.org/
http://www.ocaml.org/
4
http://caml.inria.fr/humps/
3

8

7

Comparison

Needless to say, TTT is not the only available tool for proving termination ofrewrite systems. In this final section we compare our tool with the other systems
that participated in the TRS category5 of the termination competition that wasorganized as part of the 7th International Workshop on Termination.6– We start our discussion with CiME [5], the very first tool for automaticallyproving termination of rewrite systems that is still available. CiME is a toolwith powerful techniques for finding termination proofs based on polynomial interpretations in connection with the dependency pair method. Since
CiME does not support (yet) the most recent insights in the dependency
pair method, it is less powerful than AProVE (described below) or TTT. In
contrast to TTT, CiME can handle rewrite systems with AC operators. As amatter of fact, termination is only a side-issue in CiME. Its main strengthlies in completing equational theories modulo theories like AC and C.
– CARIBOO [9] is a tool specializing in termination proofs for a particularevaluation strategy, like innermost evaluation or the strategies used in OBJlike languages. The underlying proof method is based on an inductive processakin to narrowing, but its termination proving power comes from CiME,
which is used as an external solver. TTT supports innermost termination,
but no other strategies.
– Matchbox [19] is a tool that is entirely based on methods from formal language theory. These methods are especially useful for proving terminationof string rewrite systems. Matchbox tries to establish termination or nontermination by using recent results on match-bounded rewriting [10]. Matchbox is not intended as a general-purpose termination prover (as its author
writes in [19]).
– AProVE is the most powerful tool. Besides ordinary TRSs, it can handle logic
programs, conditional rewrite systems, context-sensitive rewrite systems, andit supports rewriting modulo AC. Version 1.0 of AProVE is described in [11].
Of all existing tools, AProVE supports the most base orders and even offers several different algorithms implementing these. It incorporates virtually
all recent refinements of the dependency pair method. AProVE has several
methods that are not available in any other tool. We mention here the sizechange principle [18], transformations for dependency pairs like narrowing
and instantiation, and a modular refinement where the set of usable rules isdetermined after a suitable argument filtering has been computed. Despite
all this, last year’s termination competition version of AProVE, which further
includes the methods derived from match-bounded rewriting, could handle
only a few more systems than TTT.
We conclude the paper by listing what we believe to be the main attractions of
TTT (in no particular order):56

http://www.lri.fr/~marche/wst2004-competition/webform.cgi?command=trs
http://www-i2.informatik.rwth-aachen.de/WST04/

9

– TTT comes equipped with a very user-friendly web interface,– TTT produces readable and beautifully typeset proofs,– TTT is a very fast termination tool,– TTT is a very powerful tool based on relatively few techniques.

References
1. T. Aoto and T. Yamada. Termination of simply typed term rewriting by translationand labelling. In Proc. 14th RTA, volume 2706 of LNCS, pages 380–394, 2003.
2. T. Aoto and T. Yamada. Termination of simply-typed applicative term rewriting
systems. In Proc. 2nd HOR, Technical Report AIB-2004-03, RWTH Aachen, pages
61–65, 2004.
3. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
4. T. Arts and J. Giesl. A collection of examples for termination of term rewriting
using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen, 2001.
5. E. Contejean, C. Marché, B. Monate, and X. Urbain. CiME version 2, 2000.
Available at http://cime.lri.fr/.
6. E. Contejean, C. Marché, A.-P. Tomás, and X. Urbain. Mechanically proving
termination using polynomial interpretations. Research Report 1382, LRI, 2004.
7. N. Dershowitz. Termination by abstraction. In Proc. 20th ICLP, volume 3132 of
LNCS, pages 1–18, 2004.
8. J. Dick, J. Kalmus, and U. Martin. Automating the Knuth-Bendix ordering. Acta
Infomatica, 28:95–119, 1990.
9. O. Fissore, I. Gnaedig, and H. Kirchner. CARIBOO: An induction based proof
tool for termination with strategies. In Proc. 4th PPDP, pages 62–73. ACM Press,
2002.
10. Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Match-bounded string
rewriting. Applicable Algebra in Engineering, Communication and Computing,
15:149–171, 2004.
11. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination
proofs with AProVE. In Proc. 15th RTA, volume 3091 of LNCS, pages 210–220,
2004.
12. N. Hirokawa and A. Middeldorp. Tsukuba termination tool. In Proc. 14th RTA,
volume 2706 of LNCS, pages 311–320, 2003.
13. N. Hirokawa and A. Middeldorp. Dependency pairs revisited. In Proc. 15th RTA,
volume 3091 of LNCS, pages 249–268, 2004.
14. N. Hirokawa and A. Middeldorp. Polynomial interpretations with negative coefficients. In Proc. 7th AISC, volume 3249 of LNAI, pages 185–198, 2004.
15. N. Hirokawa and A. Middeldorp. Automating the dependency pair method. Information and Computation, 2005. To appear. A preliminary version appeared inProc. 19th CADE, volume 2741 of LNAI, pages 32–46, 2003.
16. K. Korovin and A. Voronkov. Orienting rewrite rules with the Knuth-Bendix order.
Information and Computation, 183:165–186, 2003.
17. B.C. Pierce. Types and Programming Languages. MIT Press, 2002.
18. R. Thiemann and J. Giesl. Size-change termination for term rewriting. In Proc.
14th RTA, volume 2706 of LNCS, pages 264–278, 2003.
19. J. Waldmann. Matchbox: A tool for match-bounded string rewriting. In Proc. 15th
RTA, volume 3091 of LNCS, pages 85–94, 2004.

10