Rewriting Techniques and Applications

Frontmatter

Automatic Termination

Abstract

We give an overview of applications of weighted finite automata to automatically prove termination of rewriting. Instances of this approach are: standard and arctic matrix interpretations, and the match bound technique. These methods have been developed in recent years, and they are being used by today’s leading automated termination prover software.

Johannes Waldmann

Loops under Strategies

Abstract

Most techniques to automatically disprove termination of term rewrite systems search for a loop. Whereas a loop implies non-termination for full rewriting, this is not necessarily the case if one considers rewriting under strategies. Therefore, in this paper we first generalize the notion of a loop to a loop under a given strategy. In a second step we present two novel decision procedures to check whether a given loop is a context-sensitive or an outermost loop. We implemented and successfully evaluated our method in the termination prover \({\textsf{T\kern-0.2em\raisebox{-0.3em}T\kern-0.2emT\kern-0.2em\raisebox{-0.3em}2}}\).

René Thiemann, Christian Sternagel

Proving Termination of Integer Term Rewriting

Abstract

When using rewrite techniques for termination analysis of programs, a main problem are pre-defined data types like integers. We extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically.

Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, Stephan Falke

Dependency Pairs and Polynomial Path Orders

Abstract

We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify polynomial runtime complexity of term rewrite systems and the polytime computability of the functions computed. The established techniques have been implemented and we provide ample experimental data to assess the new method.

Martin Avanzini, Georg Moser

Unique Normalization for Shallow TRS

Abstract

Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS \(\mathcal{R}\) states that any starting term can reach at most one normal form when \(\mathcal{R}\) is used, i.e. that the computation with \(\mathcal{R}\) is unique.

We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules).

We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization, etc. are decidable for this class of TRS.

Guillem Godoy, Florent Jacquemard

The Existential Fragment of the One-Step Parallel Rewriting Theory

Abstract

It is known that the first-order theory with a single predicate → that denotes a one-step rewriting reduction on terms is undecidable already for formulae with ∃ ∀ prefix. Several decidability results exist for the fragment of the theory in which the formulae start with the ∃ prefix only. This paper considers a similar fragment for a predicate → ^p which denotes the parallel one-step rewriting reduction. We show that the first-order theory of → ^p is undecidable already for formulae with ∃ ⁷ prefix and left-linear rewrite systems.

Aleksy Schubert

Proving Confluence of Term Rewriting Systems Automatically

Abstract

We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide–and–conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.

Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

A Proof Theoretic Analysis of Intruder Theories

Abstract

We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages Γ under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural-deduction-like systems and proving decidability requires significant effort in showing that the rules are “local” in some sense. By using the well-known translation between natural deduction and sequent calculus, we recast the intruder deduction problem as proof search in sequent calculus, in which locality is immediate. Using standard proof theoretic methods, such as permutability of rules and cut elimination, we show that the intruder deduction problem can be reduced, in polynomial time, to the elementary deduction problems, which amounts to solving certain equations in the underlying individual equational theories. We further show that this result extends to combinations of disjoint AC-convergent theories whereby the decidability of intruder deduction under the combined theory reduces to the decidability of elementary deduction in each constituent theory. Although various researchers have reported similar results for individual cases, our work shows that these results can be obtained using a systematic and uniform methodology based on the sequent calculus.

Alwen Tiu, Rajeev Goré

Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case

Abstract

In cryptographic protocols with the single blind copying restriction, at most one piece of unknown data is allowed to be copied in each step of the protocol. The secrecy problem for such protocols can be modeled as the satisfiability problem for the class of first-order Horn clauses called flat and one-variable Horn clauses, and is known to be DEXPTIME-complete. We show that when an XOR operator is additionally present, then the secrecy problem is decidable in 3-EXPTIME. We also note that replacing XOR by the theory of associativity-commutativity or by the theory of Abelian groups, or removing some of the syntactic restrictions on the clauses, leads to undecidability.

Helmut Seidl, Kumar Neeraj Verma

Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions

Abstract

We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the security primitives, for instance Abelian group properties. We propose a general method for deriving decision algorithms, splitting the task into 4 properties of the rewriting system describing the intruder capabilities: locality, conservativity, finite variant property and decidability of one-step deducibility constraints. We illustrate this method on a non trivial example, combining several Abelian Group properties, exponentiation and a homomorphism, showing a decidability result for this combination.

Sergiu Bursuc, Hubert Comon-Lundh

YAPA: A Generic Tool for Computing Intruder Knowledge

Abstract

Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far.

We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers all the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the more general tool ProVerif.

Mathieu Baudet, Véronique Cortier, Stéphanie Delaune

Well-Definedness of Streams by Termination

Abstract

Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. We propose a transformation from such a stream specification to a TRS in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. As a consequence, proving such well-definedness of several interesting stream specifications can be done fully automatically using present powerful tools for proving TRS termination.

Hans Zantema

Modularity of Convergence in Infinitary Rewriting

Abstract

Properties of Term Rewriting Systems are called modular iff they are preserved under disjoint union, i.e. when combining two Term Rewriting Systems with disjoint signatures. Convergence is the property of Infinitary Term Rewriting Systems that all reduction sequences converge to a limit. Strong Convergence requires in addition that no redex position in a reduction sequence is used infinitely often.

In this paper it is shown that Strong Convergence is a modular property, lifting a restriction from a known result by Simonsen, and that Convergence is modular for non-collapsing Infinitary Term Rewriting Systems.

Stefan Kahrs

A Heterogeneous Pushout Approach to Term-Graph Transformation

Abstract

We address the problem of cyclic termgraph rewriting. We propose a new framework where rewrite rules are tuples of the form (L,R,τ, σ) such that L and R are termgraphs representing the left-hand and the right-hand sides of the rule, τ is a mapping from the nodes of L to those of R and σ is a partial function from nodes of R to nodes of L. The mapping τ describes how incident edges of the nodes in L are connected in R, it is not required to be a graph morphism as in classical algebraic approaches of graph transformation. The role of σ is to indicate the parts of L to be cloned (copied). Furthermore, we introduce a notion of heterogeneous pushout and define rewrite steps as heterogeneous pushouts in a given category. Among the features of the proposed rewrite systems, we quote the ability to perform local and global redirection of pointers, addition and deletion of nodes as well as cloning and collapsing substructures.

Dominique Duval, Rachid Echahed, Frédéric Prost

An Explicit Framework for Interaction Nets

Abstract

Interaction nets are a graphical formalism inspired by Linear Logic proof-nets often used for studying higher order rewriting e.g. β-reduction. Traditional presentations of interaction nets are based on graph theory and rely on elementary properties of graph theory. We give here a more explicit presentation based on notions borrowed from Girard’s Geometry of Interaction: interaction nets are presented as partial permutations and a composition of nets, the gluing, is derived from the execution formula. We then define contexts and reduction as the context closure of rules. We prove strong confluence of the reduction within our framework and show how interaction nets can be viewed as the quotient of some generalized proof-nets.

Marc de Falco

Dual Calculus with Inductive and Coinductive Types

Abstract

This paper gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this paper presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus.

Daisuke Kimura, Makoto Tatsuta

Comparing Böhm-Like Trees

Abstract

Extending the infinitary rewriting definition of Böhm-like trees to infinitary Combinatory Reduction Systems (iCRSs), we show that each Böhm-like tree defined by means of infinitary rewriting can also be defined by means of a direct approximant function. In addition, we show that counterexamples exists to the reverse implication.

Jeroen Ketema

The Derivational Complexity Induced by the Dependency Pair Method

Abstract

We study the derivational complexity induced by the (basic) dependency pair method. Suppose the derivational complexity induced by a termination method is closed under elementary functions. We show that the derivational complexity induced by the dependency pair method based on this termination technique is the same as for the direct technique. Therefore, the derivational complexity induced by the dependency pair method based on lexicographic path orders or multiset path orders is multiple recursive or primitive recursive, respectively. Moreover for the dependency pair method based on Knuth-Bendix orders, we obtain that the derivational complexity function is majorised by the Ackermann function. These characterisations are essentially optimal.

Georg Moser, Andreas Schnabl

Local Termination

Abstract

The characterization of termination using well-founded monotone algebras has been a milestone on the way to automated termination techniques, of which we have seen an extensive development over the past years. Both the semantic characterization and most known termination methods are concerned with global termination, uniformly of all the terms of a term rewriting system (TRS). In this paper we consider local termination, of specific sets of terms within a given TRS.

The principal goal of this paper is generalizing the semantic characterization of global termination to local termination. This is made possible by admitting the well-founded monotone algebras to be partial. We show that our results can be applied in the development of techniques for proving local termination. We give several examples, among which a verifiable characterization of the terminating S-terms in CL.

Jörg Endrullis, Roel de Vrijer, Johannes Waldmann

VMTL–A Modular Termination Laboratory

Abstract

The automated analysis of termination of term rewriting systems (TRSs) has drawn a lot of attention in the scientific community during the last decades and many different methods and approaches have been developed for this purpose. We present VMTL (Vienna Modular Termination Laboratory), a tool implementing some of the most recent and powerful algorithms for termination analysis of TRSs, while providing an open interface that allows users to easily plug in new algorithms in a modular fashion according to the widely adopted dependency pair framework. Apart from modular extensibility, VMTL focuses on analyzing the termination behaviour of conditional term rewriting systems (CTRSs). Using one of the latest transformational techniques, the resulting restricted termination problems (for unconditional context-sensitive TRSs) are processed with dedicated algorithms.

Felix Schernhammer, Bernhard Gramlich

Tyrolean Termination Tool 2

Abstract

This paper describes the second edition of the Tyrolean Termination Tool—a fully automatic termination analyzer for first-order term rewrite systems. The main features of this tool are its (non-)termination proving power, its speed, its flexibility due to a strategy language, and the fact that the source code of the whole project is freely available. The clean design together with a stand-alone OCaml library for term rewriting, make it a perfect starting point for other tools concerned with rewriting as well as experimental implementations of new termination methods.

Martin Korp, Christian Sternagel, Harald Zankl, Aart Middeldorp

From Outermost to Context-Sensitive Rewriting

Abstract

We define a transformation from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. For the class of left-linear TRSs the transformation is complete. Thereby state-of-the-art termination methods and automated termination provers for context-sensitive rewriting become available for proving termination of outermost rewriting. The translation has been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.

Jörg Endrullis, Dimitri Hendriks

A Fully Abstract Semantics for Constructor Systems

Abstract

Constructor-based term rewriting systems are a useful subclass of TRS, in particular for programming purposes. In this kind of systems constructors determine a universe of values, which are the expected output of the computations. Then it would be natural to think of a semantics associating each expression to the set of its reachable values. Somehow surprisingly, the resulting semantics has poor properties, for it is not compositional nor fully abstract when non-confluent systems are considered. In this paper we propose a novel semantics for expressions in constructor systems, which is compositional and fully abstract (with respect to sensible observation functions, in particular the set of reachable values for an expression), and therefore can serve as appropriate basis for semantic based analysis or manipulation of such kind of rewrite systems.

Francisco Javier López-Fraguas, Juan Rodríguez-Hortalá, Jaime Sánchez-Hernández

The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)

Abstract

Most of the standard pleasant properties of term rewriting systems are undecidable; to wit: local confluence, confluence, normalization, termination, and completeness.

Mere undecidability is insufficient to rule out a number of possibly useful properties: For instance, if the set of normalizing term rewriting systems were recursively enumerable, there would be a program yielding “yes” in finite time if applied to any normalizing term rewriting system.

The contribution of this paper is to show (the uniform version of) each member of the list of properties above (as well as the property of being a productive specification of a stream) complete for the class \(\Pi^0_2\). Thus, there is neither a program that can enumerate the set of rewriting systems enjoying any one of the properties, nor is there a program enumerating the set of systems that do not.

For normalization and termination we show both the ordinary version and the ground versions (where rules may contain variables, but only ground terms may be rewritten) \(\Pi^0_2\)-complete. For local confluence, confluence and completeness, we show the ground versions \(\Pi^0_2\)-complete.

Jakob Grue Simonsen

Unification in the Description Logic $\mathcal{EL}$

Abstract

The Description Logic \(\mathcal{EL}\) has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, \(\mathcal{EL}\) is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in \(\mathcal{EL}\) is decidable. More precisely, \(\mathcal{EL}\)-unification is NP-complete, and thus has the same complexity as \(\mathcal{EL}\)-matching. We also show that, w.r.t. the unification type, \(\mathcal{EL}\) is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.

Franz Baader, Barbara Morawska

Unification with Singleton Tree Grammars

Abstract

First-order term unification is an essential concept in areas like functional and logic programming, automated deduction, deductive databases, artificial intelligence, information retrieval, compiler design, etc. We build upon recent developments in general grammar-based compression mechanisms for terms, which are more general than dags and investigate algorithms for first-order unification of compressed terms.

We prove that the first-order unification of compressed terms is decidable in polynomial time, and also that a compressed representation of the most general unifier can be computed in polynomial time.

We use several known results on the used tree grammars, called singleton tree grammars (STG)s, like polynomial time computability of several subalgorithmms: certain grammar extensions, deciding equality of represented terms, and generating the preorder traversal. An innovation is a specialized depth of an STG that shows that unifiers can be represented in polynomial space.

Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß

Unification and Narrowing in Maude 2.4

Abstract

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications, and has a relatively large worldwide user and open-source developer base. This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel functions for order-sorted unification modulo some frequently occurring equational axioms. Narrowing is currently supported in its Full Maude extension. We also give a brief summary of the most important features of Maude 2.4 that were not part of Maude 2.0 and earlier releases. These features include communication with external objects, a new implementation of its module algebra, and new predefined libraries. We also review some new Maude applications.

Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Backmatter