Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
FSCD Conference 2023 Conference Paper
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.
FSCD Conference 2022 Conference Paper
In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.
LPAR Conference 2012 Conference Paper
Abstract Rewrite systems form an attractive model of computation. In the past decades numerous methods have been developed to prove rewrite systems terminating. Spurred by the International Termination Competition, the emphasis in recent years is on powerful methods that can be automated.
LPAR Conference 2012 Conference Paper
Abstract Matrix interpretations are a powerful technique for proving termination of term rewrite systems. Depending on the underlying domain of interpretation, one distinguishes between matrix interpretations over the real, rational and natural numbers. In this paper we clarify the relationship between all three variants, showing that matrix interpretations over the reals are more powerful than matrix interpretations over the rationals, which are in turn more powerful than matrix interpretations over the natural numbers. We also clarify the ramifications of matrix dimension on termination proving power. To this end, we establish a hierarchy of matrix interpretations with respect to matrix dimension and show it to be infinite, with each level properly subsuming its predecessor.
LPAR Conference 2012 Conference Paper
Abstract In this paper we consider a hierarchy of three versions of Knuth-Bendix orders. (1) We show that the standard definition can be (slightly) simplified without affecting the ordering relation. (2) For the extension of transfinite Knuth-Bendix orders we show that transfinite ordinals are not needed as weights, as far as termination of finite rewrite systems is concerned. (3) Nevertheless termination proving benefits from transfinite ordinals when used in the setting of general Knuth-Bendix orders defined over a weakly monotone algebra. We investigate the relationship to polynomial interpretations and present experimental results for both termination analysis and ordered completion. For the latter it is essential that the order is totalizable on ground terms.
I&C Journal 2009 Journal Article
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.
LPAR Conference 2008 Conference Paper
Abstract First-order applicative term rewrite systems provide a natural framework for modeling higher-order aspects. In this paper 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 present a version for dependency pairs.
SAT Conference 2007 Conference Paper
Abstract Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.
I&C Journal 2007 Journal Article
The Tyrolean Termination Tool (T T T 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 T T 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 T T and provide some implementation details.
I&C Journal 2005 Journal Article
Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area in the past few years. The dependency pair method of Arts and Giesl is one of the most popular such methods. However, there are several obstacles that hamper its automation. In this paper we present new ideas to overcome these obstacles. We provide ample numerical data supporting our ideas.
I&C Journal 2005 Journal Article
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 show how the use of approximations and elementary tree automata techniques allows one to obtain decidable conditions in a simple and elegant way. Surprisingly, by avoiding complicated concepts like index and sequentiality we are able to cover much larger classes of rewrite systems. We also study modularity aspects of the classes in our hierarchy. It turns out that none of the classes is preserved under signature extension. By imposing various conditions we recover the preservation under signature extension. By imposing some more conditions we are able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations.
I&C Journal 2002 Journal Article
For a hierarchy of properties of term rewriting systems related to confluence we prove relative undecidability, i. e. , for implications X⇒Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For some of the implications either X or ¬X is semi-decidable, for others neither X nor ¬X is semi-decidable. We prove most of these results for linear term rewrite systems.
I&C Journal 2002 Journal Article
For a hierarchy of properties of term rewriting systems related to termination we prove relative undecidability: For implications X⇒Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For most implications we obtain this result for term rewriting systems consisting of a single rewrite rule.
CSL Conference 2000 Conference Paper
Abstract Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in Zantema [ 24 ] is however rather limited. In this paper we introduce a stronger version of equational semantical labelling, parameterized by three choices: (1) the order on the underlying algebra (partial order vs. quasi-order), (2) the relation between the algebra and the rewrite system (model vs. quasi-model), and (3) the labelling of the function symbols appearing in the equations (forbidden vs. allowed). We present soundness and completeness results for the various instantiations and analyze the relationships between them. Applications of our equational semantic labelling technique include a short proof of the main result of Ferreira et al. [ 7 ]—the correctness of a version of dummy elimination for AC-rewriting which completely removes the AC-axioms— and an extension of Zantema’s distribution elimination technique [ 23 ] to the equational setting.
TCS Journal 2000 Journal Article
A conditional term rewriting system is called logical if it has the same logical strength as the underlying conditional equational system. In this paper we summarize known logicality results and we present new sufficient conditions for logicality of the important class of oriented conditional term rewriting systems.
CSL Conference 1999 Conference Paper
Abstract Term rewriting is an important computational model with applications in algebra, software engineering, declarative programming, and theorem proving. In term rewriting, computation is achieved by directed equations and pattern matching. In this tutorial we give an introduction to term rewriting. The tutorial is organized as follows. After presenting several motivating examples, we explain the basic concepts and results in term rewriting: abstract rewriting, equational reasoning, termination techniques, confluence criteria, completion, strategies, and modularity. The tutorial concludes with a selection of more specialized topics as well as more recent developments in term rewriting: narrowing, advanced termination techniques (dependency pairs), conditional rewriting, rewriting modulo, tree automata techniques, and higher-order rewriting.
CSL Conference 1997 Conference Paper
Abstract For two hierarchies of properties of term rewriting systems related to confluence and termination, respectively, we prove relative undecidability: for implications X⇒Y in the hierarchies the property X is undecidable for term rewriting systems satisfying Y.
TCS Journal 1997 Journal Article
In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic ingredient of a simplification order is the subterm property, but in the literature two different definitions are given: one based on (strict) partial orders and another one based on preorders (or quasi-orders). We argue that there is no reason to choose the second one as the first one has certain advantages. Simplification orders are known to be well-founded orders on terms over a finite signature. This important result no longer holds if we consider infinite signatures. Nevertheless, well-known simplification orders like the recursive path order are also well-founded on terms over infinite signatures, provided the underlying precedence is well-founded. We propose a new definition of simplification order, which coincides with the old one (based on partial orders) in case of finite signatures, but which is also well-founded over infinite signatures and covers orders like the recursive path order. We investigate the properties of the ensuing class of simply terminating systems.
TCS Journal 1996 Journal Article
Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable sequential reduction strategy similar in scope, but simpler and more general. Our strategy can be thought of as an outermost-fair-like strategy that is allowed to be unfair to some redex of a term when contracting the redex is useless for the normalization of the term. Unlike the strategy of Kennaway, our strategy does not rely on syntactic restrictions that imply confluence. On the contrary, it can easily be applied to any term rewriting system, and we show that the class of term rewriting systems for which our strategy is normalizing properly includes all (almost) orthogonal systems. Our strategy is more versatile; in case of (almost) orthogonal term rewriting systems, it can be used to detect certain cases of non-termination. Our normalization proof is more accessible than Kennaway's. We also show that our sequential strategy sometimes succeeds where the parallel-outermost strategy fails.
TCS Journal 1996 Journal Article
Narrowing is an important method for solving unification problems in equational theories that are presented by confluent term rewriting systems. Because narrowing is a rather complicated operation, several authors studied calculi in which narrowing is replaced by more simple inference rules. This paper is concerned with one such calculus. Contrary to what has been stated in the literature, we show that the calculus lacks strong completeness, so selection functions to cut down the search space are not applicable. We prove completeness of the calculus and we establish an interesting connection between its strong completeness and the completeness of basic narrowing. We also address the eager variable elimination problem. It is known that many redundant derivations can be avoided if the variable elimination rule, one of the inference rules of our calculus, is given precedence over the other inference rules. We prove the completeness of a restricted variant of eager variable elimination in the case of orthogonal term rewriting systems.