Rewriting Techniques and Applications

Technological breakthroughs have enabled complete genomic sequencing and proteomic study of many species, fueling exponential growth in the available biological data relevant to important biological functions. The computational analysis of these datasets has been hampered by many structural and scientific barriers. The application of symbolic toolsets borrowed from the term rewriting and formal methods communities may help accelerate biologists understanding of network effects in complex biochemical systems of interest.

The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions.

We introduce a novel representation for associative-commutative (AC) terms which, for certain important classes of rewrite rules, allows both the AC matching and the AC renormalization steps to be accomplished using time and space that is logarithmic in the size of the flattened AC argument lists involved. This novel representation can be cumbersome for other, more general algorithms and manipulations. Hence, we describe machine efficient techniques for converting to and from a more conventional representation together with a heuristic for deciding at runtime when to convert a term to the new representation. We sketch how our approach can be generalized to order-sorted AC rewriting and to other equational theories. We also present some experimental results using the Maude 2 interpreter.

Several software systems have been developed recently for the automated generation of combustion reactions kinetic mechanisms using different representations of species and reactions and different generation algorithms. In parallel, several software systems based on rewriting have been developed for the easy modeling and prototyping of systems using rules controlled by strategies. This paper presents our current experience in using the rewrite system ELAN for the automated generation of the combustion reactions mechanisms previously implemented in the EXGAS kinetic mechanism generator system. We emphasize the benefits of using rewriting and rule-based programming controlled by strategies for the generation of kinetic mechanisms.

We present a name free λ-calculus with explicit substitutions based on a generalized notion of director strings: we annotate a term with information about how each substitution should be propagated through the term. We first present a calculus where we can simulate arbitrary β-reduction steps, and then simplify the rules to model the evaluation of functional programs (reduction to weak head normal form). We also show that we can derive the closed reduction strategy (a weak strategy which, in contrast with standard weak strategies allows certain reductions to take place inside λ-abstractions thus offering more sharing). Our experimental results confirm that, for large combinator based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.

Rewriting Logic has shown to provide a general and elegant framework for unifying a wide variety of models, including concurrency models and deduction systems. In order to extend the modeling capabilities of rule based languages, it is natural to consider that the firing of rules can be subject to some probabilistic laws. Considering rewrite rules subject to probabilities leads to numerous questions about the underlying notions and results. In this paper, we discuss whether there exists a notion of probabilistic rewrite system with an associated notion of probabilistic rewriting logic.

This paper gives an overview of the Maude 2.0 system. We emphasize the full generality with which rewriting logic and membership equational logic are supported, operational semantics issues, the new built-in modules, the more general Full Maude module algebra, the new META-LEVEL module, the LTL model checker, and new implementation techniques yielding substantial performance improvements in rewriting modulo. We also comment on Maude’s formal tool environment and on applications.

This paper presents an abstract framework and multiple diagram-based methods for proving meaning preservation, i.e., that all rewrite steps of a rewriting system preserve the meaning given by an operational semantics based on a rewriting strategy. While previous rewriting-based methods have generally needed the treated rewriting system as a whole to have such properties as, e.g., confluence, standardization, and/or termination or boundedness of developments, our methods can work when all of these conditions fail, and thus can handle more rewriting systems. We isolate the new lift/project with termination diagram as the key proof idea and show that previous rewritingbased methods (Plotkin’s method based on confluence and standardization and Machkasova and Turbak’s method based on distinct lift and project properties) implicitly use this diagram. Furthermore, our framework and proof methods help reduce the proof burden substantially by, e.g., supporting separate treatment of partitions of the rewrite steps, needing only elementary diagrams for rewrite step interactions, excluding many rewrite step interactions from consideration, needing weaker termination properties, and providing generic support for using developments in combination with any method.

We introduce a new higher-order rewriting formalism, called Expression Reduction Systems with Patterns (ERSP), where abstraction is not only allowed on variables but also on nested patterns. These patterns are built by combining standard algebraic patterns with choice constructors used to denote different possible structures allowed for an abstracted argument. In other words, the non deterministic choice between different rewriting rules which is inherent to classical rewriting formalisms can be lifted here to the level of patterns. We show that confluence holds for a reasonable class of systems and terms.

Residuals have been studied for various forms of rewriting and residual systems have been defined to capture residuals in an abstract setting. In this article we study residuals in orthogonal Pattern Rewriting Systems (PRSs). First, the rewrite relation is defined by means of a higher-order rewriting logic, and proof terms are defined that witness reductions. Then, we have the formal machinery to define a residual operator for PRSs, and we will prove that an orthogonal PRS together with the residual operator mentioned above, is a residual system. As a side-effect, all results of (abstract)residual theory are inherited by orthogonal PRSs, such as confluence, and the notion of permutation equivalence of reductions.

In this paper we describe the implementation of the UNITY formalism as an extension of general-purpose languages and show its translation to C abstract syntax using PHOBOS, our generic front-end in the Mojave compiler. PHOBOS uses term rewriting to define the syntax and semantics of programming languages, and automates their translation to an internal compiler representation. Furthermore, it provides access to formal reasoning capabilities using the integrated MetaPRL theorem prover, through which advanced optimizations and transformations can be implemented or formal proofs derived.

We consider a new extension of the Skolem class for first-order logic and prove its decidability by resolution techniques. We then extend this class including the built-in equational theory of exclusive or. Again, we prove the decidability of the class by resolution techniques. Considering such fragments of first-order logic is motivated by the automatic verification of cryptographic protocols, for an arbitrary number of sessions; the first-order formalization is an approximation of the set of possible traces, for instance relaxing the nonce freshness assumption. As a consequence, we get some new decidability results for the verification of cryptographic protocols with exclusive or.

Modular multiplication and exponentiation are common operations in modern cryptography. Unification problems with respect to some equational theories that these operations satisfy are investigated. Two different but related equational theories are analyzed. A unification algorithm is given for one of the theories which relies on solving syzygies over multivariate integral polynomials with noncommuting indeterminates. For the other theory, in which the distributivity property of exponentiation over multiplication is assumed, the unifiability problem is shown to be undecidable by adapting a construction developed by one of the authors to reduce Hilbert’s 10th problem to the solvability problem for linear equations over semi-rings. A new algorithm for computing strong Gröbner bases of right ideals over the polynomial ring Z<X₁, . . . , X_n> is proposed; unlike earlier algorithms proposed by Baader as well as by Madlener and Reinert which work only for right admissible term orderings with the boundedness property, this algorithm works for any right admissible term ordering. The algorithms for some of these unification problems are expected to be integrated into Naval Research Lab.’s Protocol Analyzer (NPA), a tool developed by Catherine Meadows, which has been successfully used to analyze cryptographic protocols, particularly emerging standards such as the Internet Engineering Task Force’s (IETF) Internet Key Exchange [11] and Group Domain of Interpretation [12] protocols. Techniques from several different fields — particularly symbolic computation (ideal theory and Gröebner basis algorithms) and unification theory — are thus used to address problems arising in state-based cryptographic protocol analysis.

We study two-way tree automata modulo equational theories. We deal with the theories of Abelian groups (ACUM), idempotent commutative monoids (ACUI), and the theory of exclusive-or (ACUX), as well as some variants including the theory of commutative monoids (ACU). We show that the one-way automata for all these theories are closed under union and intersection, and emptiness is decidable. For two-way automata the situation is more complex. In all these theories except ACUI, we show that two-way automata can be effectively reduced to one-way automata, provided some care is taken in the definition of the so-called push clauses. (The ACUI case is open.) In particular, the two-way automata modulo these theories are closed under union and intersection, and emptiness is decidable. We also note that alternating variants have undecidable emptiness problem for most theories, contrarily to the non-equational case where alternation is essentially harmless.

Dimensional safety policy checking is an old topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Scientific and/or navigation software is routinely dimensional and violations of measurement unit safety policies can hide significant domain-specific errors which are hard or impossible to find otherwise. Dimensional analysis of programs written in conventional programming languages is addressed in this paper. We draw general design principles for dimensional analysis tools and then discuss our prototypes, implemented by rewriting, which include both dynamic and static checkers. Our approach is based on assume/assert annotations of code which are properly interpreted by our tools and ignored by standard compilers/interpreters. The output of our prototypes consists of warnings that list those expressions violating the unit safety policy. These prototypes are implemented in the rewriting system Maude.

I take the opportunity given by this invited talk to promote two ideas: (1) a topological point of view can fertilize the notion of rewriting and (2) this topological approach of rewriting is at the core of the modeling and the simulation of an emerging class of dynamical systems (DS): the DS that exhibit a dynamical structure (or (DS)2 in the rest of this paper).

We prove that linear second-order matching in the linear λ-calculus with linear occurrences of the unknowns is NP-complete. This result shows that context matching and second-order matching in the linear λ-calculus are, in fact, two different problems.

XML documents, and other forms of semi-structured data, may be roughly described as edge labeled trees; it is therefore natural to use tree automata to reason on them. This idea has already been successfully applied in the context of Document Type Definition (DTD), the simplest standard for defining XML documents validity, but additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. In this paper, we define a tree logic that directly embeds XML Schema as a plain subset as well as a new class of automata for unranked trees, used to decide this logic, which is well-suited to the processing of XML documents and schemas.

In [13], a new size-change principle was proposed to verify termination of functional programs automatically. We extend this principle in order to prove termination and innermost termination of arbitrary term rewrite systems (TRSs). Moreover, we compare this approach with existing techniques for termination analysis of TRSs (such as recursive path orderings or dependency pairs). It turns out that the size-change principle on its own fails for many examples that can be handled by standard techniques for rewriting, but there are also TRSs where it succeeds whereas existing rewriting techniques fail. In order to benefit from their respective advantages, we show how to combine the size-change principle with classical orderings and with dependency pairs. In this way, we obtain a new approach for automated termination proofs of TRSs which is more powerful than previous approaches.

Polynomial interpretations and RPO-like orderings allow one to prove termination of Associative and Commutative (AC-)rewriting by only checking the rules of the given rewrite system. However, these methods have important limitations as termination proving tools.To overcome these limitations, more powerful methods like the dependency pair method have been extended to the AC-case. Unfortunately, in order to ensure AC-termination, the so-called extended rules, which, in general, are hard to prove, must be added to the rewrite system.In this paper we present a fully monotonic AC-compatible semantic path ordering. This monotonic AC-ordering defines a new automatable termination proving method for AC-rewriting which does not need to consider extended rules. As a hint of the power of this method, we can easily prove several non-trivial examples appearing in the literature, including one that, to our knowledge, can be handled by no other automatic method.

In this article we introduce the notion of a generalized system of fundamental sequences and we define its associated slow-growing hierarchy. We claim that these concepts are genuinely related to the classification of the complexity—the derivation length— of rewrite systems for which termination is provable by a standard termination ordering. To substantiate this claim, we re-obtain multiple recursive bounds on the the derivation length for rewrite systems terminating under lexicographic path ordering, originally established by the second author.

We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new ideas that make the method more efficient. The tool produces high-quality output and has a convenient web interface.

In this paper, we show how the problem of verifying liveness properties is related to termination of term rewrite systems (TRSs). We formalize liveness in the framework of rewriting and present a sound and complete transformation to transform particular liveness problems into TRSs. Then the transformed TRS terminates if and only if the original liveness property holds. This shows that liveness and termination are essentially equivalent. To apply our approach in practice, we introduce a simpler sound transformation which only satisfies the ‘only if’-part. By refining existing techniques for proving termination of TRSs we show how liveness properties can be verified automatically. As examples, we prove a liveness property of a waiting line protocol for a network of processes and a liveness property of a protocol on a ring of processes.

The bytecode verifier (BCV), which performs a static analysis to reject potentially insecure programs, is a key security function of the Java(Card) platform. Over the last few years there have been numerous projects to prove formally the correctness of bytecode verification, but relatively little effort has been made to provide methodologies, techniques and tools that help such formalisations. In earlier work, we develop a methodology and a specification environment featuring a neutral mathematical language based on conditional rewriting, that considerably reduce the cost of specifying virtual machines.In this work, we show that such a neutral mathematical language based on conditional rewriting is also beneficial for performing automatic verifications on the specifications, and illustrate in particular how implicit induction techniques can be used for the validation of the Java(Card) Platform. More precisely, we report on the use of SPIKE, a first-order theorem prover based on implicit induction, to establish the correctness of the BCV. The results are encouraging, as many of the intermediate lemmas required to prove the BCV correct can be proved with SPIKE.

A key new concept, term partition, allows to design a new method for proving theorems whose proof usually requires mathematical induction. A term partition of a term t is a well-defined splitting of t into a pair (a, b) of terms that describes the language of normal forms of the ground instances of t.If $$ \mathcal{A} $$ is a monomorphic set of axioms (rules) and (a, b) is a term partition of t, then the normal form (obtained by using $$ \mathcal{A} $$) of any ground instance of t can be “divided” into the normal forms (obtained by using $$ \mathcal{A} $$) of the corresponding ground instances of a and b. Given a conjecture t = s to be checked for inductive validity in the theory of A, a partition (a, b) of t and a partition (c, d) of s is computed. If a = c and b = d, then t = s is an inductive theorem for $$ \mathcal{A} $$.The method is conceptually different to the classical theorem proving approaches. It allows to obtain proofs of a large number of conjectures (including non-linear ones) without additional lemmas or generalizations.

The equational prover of the Theorema system is described. It is implemented on Mathematica and is designed for unit equalities in the first order or in the applicative higher order form. A (restricted) usage of sequence variables and Mathematica built-in functions is allowed.

Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted first-order TRSs and show that termination problem of STTRSs is reduced to that of many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation to facilitate termination proof of them; our labelling employs an extension of semantic labelling where terms are interpreted on a many-sorted algebra.

We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computability closure for ensuring the termination of the combination of rewriting and β-reduction.Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computability closure. This includes equations like associativity and commutativity and provides an original treatment of termination modulo equations.

This paper presents a partial solution to the long standing open problem whether termination of one-rule string rewriting is decidable. Overlaps between the two sides of the rule play a central role in existing termination criteria. We characterize termination of all one-rule string rewriting systems that have one such overlap at either end. This both completes a result of Kurth and generalizes a result of Shikishima-Tsuji et al.

Term rewriting can only be applied if practical implementations of term rewriting engines exist. New rewriting engines are designed and implemented either to experiment with new (theoretical) results or to be able to tackle new application areas. In this paper we present the Meta-Environment: an environment for rapidly implementing the syntax and semantics of term rewriting based formalisms. We provide not only the basic building blocks, but complete interactive programming environments that only need to be instantiated by the details of a new formalism.

This paper gives a bottom-up logic programming formulation of the Hindley-Milner polymorphic type inference algorithm. We show that for programs of bounded order and arity the given algorithm runs in O(nα(n) + dn) time where n is the length of the program, d is the “scheme depth” of the program, and α is the inverse of Ackermann’s function. It is argued that for practical programs d will not exceed 5 even for programs with hundreds of module layers. This formulation of the Hindley-Milner algorithm is intended as a case study in “logical algorithms”, i.e., algorithms presented and analyzed as bottom-up inference rules.

One problem in computational group theory is to find a presentation of the subgroup generated by a set of elements of a group. The Reidemeister-Schreier algorithm was developed in the 1930’s and gives a solution based upon enumerative techniques. This however means the algorithm can only be applied to finite groups. This paper proposes a rewriting based alternative to the Reidemeister-Schreier algorithm which has the advantage of being applicable to infinite groups.

We study orderings ⊴S on reductions in the style of Lévy reflecting the growth of information w.r.t. (super)stable sets S of ‘values’ (such as head-normal forms or Böhm-trees). We show that sets of co-initial reductions ordered by ⊴S form finitary ω-algebraic complete lattices, and hence form computation and Scott domains. As a consequence, we obtain a relativized version of the computational semantics proposed by Boudol for term rewriting systems. Furthermore, we give a pure domain-theoretic characterization of the orderings ⊴S in the spirit of Kahn and Plotkin’s concrete domains. These constructions are carried out in the framework of Stable Deterministic Residual Structures, which are abstract reduction systems with an axiomatized residual relations on redexes, that model all orthogonal (or conflict-free) reduction systems as well as many other interesting computation structures.

This paper provides an algorithm to compute the complement of tree languages recognizable with A-TA (tree automata with associativity axioms [16]). Due to this closure property together with the previously obtained results, we know that the class is boolean closed, while keeping recognizability of A-closures of regular tree languages. In the proof of the main result, a new framework of tree automata, called sequence-tree automata, is introduced as a generalization of Lugiez and Dal Zilio’s multi-tree automata [14] of an associativity case. It is also shown that recognizable A-tree languages are closed under a one-step rewrite relation in case of ground A-term rewriting. This result allows us to compute an under-approximation of A-rewrite descendants of recognizable A-tree languages with arbitrary accuracy.

In this paper we present lower bounds and rewriting algorithms for testing membership of a word in a regular language described by an extended regular expression. Motivated by intuitions from monitoring and testing, where the words to be tested (execution traces) are typically much longer than the size of the regular expressions (patterns or requirements), and by the fact that in many applications the traces are only available incrementally, on an event by event basis, our algorithms are based on an event-consumption idea: a just arrived event is “consumed” by the regular expression, i.e., the regular expression modifies itself into another expression discarding the event. We present an exponential space lower bound for monitoring extended regular expressions and argue that the presented rewriting-based algorithms, besides their simplicity and elegance, are practical and almost as good as one can hope. We experimented with and evaluated our algorithms in Maude.