Increasing interpretations

The article at hand introduces a refinement of interpretation-based termination criteria for term rewrite systems in the dependency pair setting. Traditional methods share the property that—in order to be successful—all rewrite rules must (weakly) decrease with respect to some measure. One novelty of our approach is that we allow some rules to increase the interpreted value. These rules are found by simultaneously searching for adequate polynomial interpretations while considering the information of the dependency graph. We prove that our method extends the termination proving power of linear interpretations. Furthermore, this generalization perfectly fits the dependency pair framework which is implemented in virtually every termination prover dealing with term rewrite systems. We present two dependency pair processors for increasing interpretations. The novelty of the second one is that it can be used to eliminate single edges from the dependency graph.     

Proving termination of (conditional) rewrite systems

In this paper an important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a rewrite systemR, do not suffice for proving termination ofR. Indeed sometimes semantic information is needed to orient a rewrite rule. Therefore we integrate a semantic interpretation of rewrite systems and terms into a well-founded ordering on terms: the notion ofsemantic ordering is the first main contribution of this paper. The use and usefulness of the semantic ordering in proving termination is illustrated by means of some realistic examples.Furthermore the concept of semantic information induces a novel approach for proving termination inconditional rewrite systems. The idea is to employ not only semantic information contained in the terms that are to be compared, but also extra (semantic) information contained in the premiss of the conditional equation in which the terms appear. This leads to our second contribution in the termination problem area: the notion ofcontextual ordering andcontextual semantic ordering. Thecontextual approach allows to prove termination of conditional rewrite systems where all classical partial orderings would fail.     

Mechanically Proving Termination Using Polynomial Interpretations

For a long time, term orderings defined by polynomial interpretations were scarcely used in computer-aided termination proof of TRSs. But recently, the introduction of the dependency pairs approach achieved considerable progress w.r.t. automated termination proof, in particular by requiring from the underlying ordering much weaker properties than the classical approach. As a consequence, the noticeable power of a combination dependency pairs/polynomial orderings yielded a regain of interest for these interpretations. We describe criteria on polynomial interpretations for them to define weakly monotonic orderings. From these criteria, we obtain new techniques both for mechanically checking termination using a given polynomial interpretation and for finding such interpretations with full automation. With regard to automated search, we propose an original method for solving Diophantine constraints. We implemented these techniques into the CiME rewrite tool, and we provide some experimental results that show how useful polynomial orderings actually are in practice.     

Type introduction for equational rewriting

Abstract. Type introduction is a useful technique for simplifying the task of proving properties of rewrite systems by restricting the set of terms that have to be considered to the well-typed terms according to any many-sorted type discipline which is compatible with the rewrite system under consideration. A property of rewrite systems for which type introduction is correct is called persistent. Zantema showed that termination is a persistent property of non-collapsing rewrite systems and non-duplicating rewrite systems. We extend his result to the more complicated case of equational rewriting. As a simple application we prove the undecidability of AC-termination for terminating rewrite systems. We also present sufficient conditions for the persistence of acyclicity and non-loopingness, two properties which guarantee the absence of certain kinds of infinite rewrite sequences. In the final part of the paper we show how our results on persistence give rise to new modularity results. Received 30 June 1998 / 12 January 2000     

Match-bounds revisited

The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend their work to non-left-linear rewrite systems. The key to this extension is the introduction of so-called raise rules and the use of tree automata that are not quite deterministic. Furthermore, to increase the applicability of the method we show how it can be incorporated into the dependency pair framework. To achieve this we introduce two new enrichments which take the special properties of dependency pair problems into account.     

Relative Termination via Dependency Pairs

A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.     

Termination Proofs for String Rewriting Systems via Inverse Match-Bounds

Annotating a letter by a number, one can record information about its history during a rewrite derivation. In each rewrite step, numbers in the reduct are updated depending on the redex numbering. A string rewriting system is called match-bounded if there is a global upper bound to these numbers. Match-boundedness is known to be a strong sufficient criterion for both termination and preservation of regular languages. We show that the string rewriting systems whose inverse (left and right hand sides exchanged) is match-bounded, also have exceptional properties, but slightly different ones. Inverse match-bounded systems need not terminate; they effectively preserve context-free languages; their sets of normalizable strings and their sets of immortal strings are effectively regular. These languages can be used to decide the normalization, the uniform normalization, the termination and the uniform termination problem for inverse match-bounded systems. We also prove that the termination problem is decidable in linear time, and that a certain strong reachability problem is decidable, thereby solving two open problems of McNaughton’s. Like match-bounds, inverse match-bounds entail linear derivational complexity on the set of terminating strings.     

Tyrolean termination tool: Techniques and features

The Tyrolean Termination Tool (T_TT for short) is a powerful tool for automatically proving termination of rewrite systems. It incorporates several new refinements of the dependency pair method that are easy to implement, increase the power of the method, result in simpler termination proofs, and make the method more efficient. T_TT employs polynomial interpretations with negative coefficients, like x − 1 for a unary function symbol or x − y for a binary function symbol, which are useful for extending the class of rewrite systems that can be proved terminating automatically. Besides a detailed account of these techniques, we describe the convenient web interface of T_TT and provide some implementation details.     

Uncurrying for Termination and Complexity

First-order applicative rewrite systems provide a natural framework for modeling higher-order aspects. In this article we present a transformation from untyped applicative term rewrite systems to functional term rewrite systems that preserves and reflects termination. Our transformation is less restrictive than other approaches. In particular, head variables in right-hand sides of rewrite rules can be handled. To further increase the applicability of our transformation, we study the method for innermost rewriting and derivational complexity, and present a version for dependency pairs.     

Characterizing and proving operational termination of deterministic conditional term rewriting systems

We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms (i.e., terms over the signature of the DCTRS). This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of Duran et al. (2008) [10].     

Mechanizing and Improving Dependency Pairs

The dependency pair technique is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. We improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs that simplify (innermost) termination proofs significantly. To fully mechanize the approach, we show how transformations and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples. Supported by the Deutsche Forschungsgemeinschaft DFG, grant GI 274/5-1.     

Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs

We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adaptation of successful termination techniques from the dependency pair framework in order to use them for complexity analysis. By extensive experimental results, we demonstrate the power of our method compared to existing techniques.     

Abstract abstract reduction

We propose novel algebraic proof techniques for rewrite systems. Church–Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.     

Narrowing-based simulation of term rewriting systems with extra variables and its Termination Proof

Term rewriting systems (TRSs) extended by allowing to contain extra variables in their rewrite rules are called EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper shows that narrowing can simulate reduction sequences of EV-TRSs as narrowing sequences starting from ground terms. We prove the soundness of ground narrowing sequences for the reduction sequences. We prove the completeness for the case of right-linear systems, and also for the case that any redex reduced in the reduction sequence is not introduced by means of extra variables. Moreover, we give a method to prove the termination of the simulation, extending the dependency pair method to prove termination of TRSs, into that of narrowing on EV-TRSs starting from ground terms. We show that the method is useful for right-linear or constructor systems.     

Approximations for Strategies and Termination

The theorem of Huet and Lévy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if the term under consideration has a normal form, forms the basis of all results on optimal normalizing strategies for orthogonal rewrite systems. However, needed redexes are not computable in general.

In the paper we illustrate, based on the framework introduced in [6], how the use of approximations and their associated tree automata results allows one to obtain decidable conditions in a simple and elegant way.

We further show how the very same ideas can be used to improve [18] the dependency pair method of Arts and Giesl [1] for proving termination of rewrite systems automatically. More precisely, we show how approximations and tree automata techniques provide a better estimation of the dependency graph. This graph determines the ordering constraints that have to be solved in order to conclude termination. Furthermore, we present a new estimation of the dependency graph that does not rely on computationally expensive tree automata techniques.     

A path ordering for proving termination of AC rewrite systems

We describe a method that extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy for proving termination of associative-commutative (AC) rewrite systems. Instead of comparing the arguments of an AC-operator using the multiset extension, wepartition them into disjoint subsets and use each subset only once for comparison. To preserve transitivity, we introduce two techniques —pseudocopying andelevating of arguments of an AC operator. This method imposesno restrictions at all on the underlying precedence relation on function symbols. It can therefore prove termination of a much more extensive class of AC rewrite systems than can previous methods, such as associative path ordering, that restrict AC operators to be minimal or subminimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented inRRL, Rewrite Rule Laboratory, a theorem-proving environment based on rewrite techniques and completion.A preliminary version appears in Proc. of10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India (1990).Partially supported by the National Science Foundation Grant no. CCR-8906678.Partially supported by the National Science Foundation Grant no. CCR-9009755Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.     

Proving Termination by Dependency Pairs and Inductive Theorem Proving

Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.     

Proving convergence of self-stabilizing systems using first-order rewriting and regular languages

Summary. In the framework of self-stabilizing systems, the convergence proof is generally done by exhibiting a measure that strictly decreases until a legitimate configuration is reached. The discovery of such a measure is very specific and requires a deep understanding of the studied transition system. In contrast we propose here a simple method for proving convergence, which regards self-stabilizing systems as string rewrite systems, and adapts a procedure initially designed by Dershowitz for proving termination of string rewrite systems. In order to make the method terminate more often, we also propose an adapted procedure that manipulates “schemes”, i.e. regular sets of words, and incorporates a process of scheme generalization. The interest of the method is illustrated on several nontrivial examples. Received: January 2000 / Accepted: November 2000     

Elimination of Conditions

We formally define and prove the correctness of a transformation from conditional rewrite systems (CTRS) into unconditional ones. The main result states that this transformation applies to any kind of CTRS (including extra variables in conditions) without any restrictions, and that derivations are preserved up to a mapping between terms. We also prove that termination and confluence of the original system are preserved in the transformed one under some natural assumptions.