Catálogo de publicaciones - libros

The confluence property is one of the most important properties of term rewriting systems, and various sufficient criteria for proving this property have been widely investigated. A necessary and sufficient criterion for confluence of terminating term rewriting systems, in which every reduction must terminate, was demonstrated by Knuth and Bendix (1970). For non-terminating term rewriting systems, Rosen (1973) proved that left-linear and non-overlapping term rewriting systems (i.e., no variable occurs twice or more in the left-hand side of a rewriting rule and two left-hand sides of rewriting rules must not overlap) are confluent, and the non-overlapping limitation was somewhat relaxed by Huet (1980), Toyama (1988), and van Oostrom (1997). However, few criteria have been proposed for confluence of term rewriting systems that are non-left-linear and non-terminating. Thus, it is still worth while extending criteria for these systems.

A powerful technique for showing confluence of a non-left-linear non-terminating term rewriting system is a divide-and-conquer method based on modularity by Toyama (1987) or persistency by Zantema (1994), Aoto and Toyama (1997). The method guarantees that if the system is decomposed into small subsystems and each of them is confluent then this system has the confluence property. Another useful technique is a transformational method based on conditional-linearization by Klop and de Vrijer (1991), Toyama and Oyamaguchi (1994), or a labelling technique. In this method we apply a non-confluence preserving transformation on a term rewriting system. Then the term rewriting system is confluent if the transformed system is confluent, because of non-confluence preserving. In this talk we will illustrate these techniques through various examples and discuss the relation among them.

We propose two generalizations of innermost rewriting for which we prove that termination of innermost rewriting is equivalent to termination of generalized innermost rewriting. As a consequence, by rewriting in an arbitrary TRS certain non-innermost steps may be allowed by which the termination behavior and efficiency is often much better, but never worse than by only doing innermost rewriting.

This paper shows that the suitable orderings for proving innermost termination are characterized by the , for short. This property may lead to several innermost-specific orderings. Here, an IP-monotonic version of the is presented. This variant can be used (directly or as ingredient of the method) for proving innermost termination of non-terminating term rewrite systems.

A convenient method for defining a quasi-ordering, such as those used for proving termination of rewriting, is to choose the minimum of a set of quasi-orderings satisfying some desired traits. Unfortunately, a minimum in terms of set inclusion can be non-existent even when an intuitive “minimum” exists. We suggest an alternative to set inclusion, called “leanness”, show that leanness is a partial ordering of quasi-orderings, and provide sufficient conditions for the existence of a “leanest” ordering.

Modular rewriting seeks criteria under which rewrite systems inherit properties from their smaller subsystems. This divide and conquer methodology is particularly useful for reasoning about large systems where other techniques fail to scale adequately. Research has typically focused on reasoning about the modularity of specific properties for specific ways of combining specific forms of rewriting.

This paper is, we believe, the first to ask a much more general question. Namely, what can be said about modularity independently of the specific form of rewriting, combination and property at hand. A priori there is no reason to believe that anything can actually be said about modularity without reference to the specifics of the particular systems etc. However, this paper shows that, quite surprisingly, much can indeed be said.

We consider the well-known problem of deciding the union of decidable equational theories. We focus on monadic theories, i.e., theories over signatures with unary function symbols only. The equivalence of the category of monadic equational theories and the category of monoids is used. This equivalence facilitates a translation of the considered decidability problem into the word problem in the pushout of monoids which themselves have decidable word problems. Using monoids, existing results on the union of theories are then restated and proved in a succint way. The idea is then analyzed of first guaranteeing that the union is a “jointly conservative” extension and then using this property to show decidability of the union. It is shown that “joint conservativity” is equivalent to the corresponding monoid amalgam being embeddable; this allows one to apply results from amalgamation theory to this problem. Then we prove that using this property to show decidability is a more difficult matter: it turns out that even if this property and some additional conditions hold, the problem remains undecidable.

Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logic programming or term rewriting systems. Previous work on nominal rewriting and logic programming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic’s equivariance property, these applications require a stronger form of unification, which we call . Unfortunately, equivariant unification and matching are -hard decision problems. This paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for equivariant matching, that is, for matching problems in which the swapping operation does not appear.

Sorting information arises naturally in E-unification problems. This information is used to rule out invalid solutions. We show how to use sorting information to make E-unification procedures more efficient. We illustrate our ideas using Basic Syntactic Mutation. We give classes of problems where E-unification becomes polynomial. We show how -unification can be separated into a polynomial part and a more complicated part using a specialized algorithm. Our approach is motivated by a real problem arising from Cryptographic Protocol Verification.

It has been proposed in [1] to perform deduction modulo leaf permutative theories, which are notoriously hard to handle directly in equational theorem proving. But unification modulo such theories is a difficult task, not tackled in [1]; a subclass of flat equations has been considered only recently, in [2]. Our emphasis on group theoretic structures led us in [6] to the definition of a more general subclass of leaf permutative theories, the theories. They have good semantic and algorithmic properties, which we use here to design a complete unification algorithm.

Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework of higher-order term rewriting without bound variables. In this paper, the dependency pair method of first-order term rewriting introduced by Arts and Giesl (TCS, 2000) is extended in order to show termination of simply typed term rewriting systems. Basic concepts such as dependency pairs and estimated dependency graph in the simply typed term rewriting framework are clarified. The subterm criterion introduced by Hirokawa and Middeldorp (RTA, 2004) is successfully extended to the case where terms of function type are allowed. Finally, an experimental result for a collection of simply typed term rewriting systems is presented. Our method is compared with the direct application of the first-order dependency pair method to a first-order encoding of simply typed term rewriting systems.