Selected papers of the "22nd International Conference on Rewriting Techniques and Applications (RTA 2011)"


Editors: Aart Middeldorp, Manfred Schmidt-Schauss

This special issue contains selected papers presented at the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), which was held from May 30 to June 1, 2011 in Novi Sad, Serbia as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2011). RTA is the major forum for the presentation of research on all aspects of rewriting. Six of the 20 papers presented at the conference were invited to submit an extended version to this special issue, including the paper that received the best paper award at the conference: A Rewriting View of Simple Typing by Aaron Stump, Garrin Kimmell, and Ruba El Haj Omar.

The submissions for the special issue underwent a new and thorough reviewing and revision process, in accordance with the high standards of LMCS.

The paper Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems by Takahito Aoto and Yoshihito Toyama presents a new method for establishing confluence of rewrite systems, which is especially useful for systems incorporating associative and commutative axioms. Experiments performed with the automatic confluence prover ACP show the power of the new method.
  • Patrick Bahr investigates in Modes of Convergence for Term Graph Rewriting an extension of infinitary term rewriting on term graphs. The main achievement is a generalization of two modes of convergence from terms to term graphs, showing that infinitary rewriting can smoothly be extended to term graphs.
  • The paper Quantifier-Free Interpolation of a Theory of Arrays by Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise exhibits a novel method which enables easier verification of software that uses arrays. A procedure is designed that computes quantifier-free interpolants for a Skolemized version of the extensional theory of arrays, by solving equations between array updates and exploiting rewriting techniques.
  • Cynthia Kop and Femke van Raamsdonk present in Dynamic Dependency Pairs for Algebraic Functional Systems a new dependency pair approach for higher-order rewriting, which includes a new technique to circumvent the subterm property that was needed in earlier work. They also extends several first-order methods, such as argument filterings and usable rules, and proposes the new method of formative rules.
  • The paper Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity by Naoki Nishida, Masahiko Sakai and Toshiki Sakabe presents new sufficient conditions for the soundness of unraveling transformations from deterministic conditional rewrite systems to unconditional systems. The obtained results hold for systems with extra variables that appear naturally in the study of program inversion. To handle the additional complexity, an interesting extension of basic narrowing is considered.
  • The paper A Rewriting View of Simple Typing by Aaron Stump, Garrin Kimmell, Hans Zantema and Ruba El Haj Omar is an extended, improved and corrected version of their conference paper. It sheds new light on the issues of computing types and checking typability by exploiting term rewriting methods. In particular in variants of simply-typed lambda calculi a small-step abstract reduction on terms enriched with type expressions is viewed as term rewriting and successfully analyzed.

We thank the authors and the reviewers for their hard work producing the contents of this issue, and the managing editor for special issues Benjamin Pierce for encouraging us to edit this volume.

Manfred Schmidt-Schauss (PC chair of RTA 2011) and Aart Middeldorp
Guest Editors

1. A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

Takahito Aoto ; Yoshihito Toyama.
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also (partially) works even if the system is not terminating modulo E. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

2. Quantifier-Free Interpolation of a Theory of Arrays

Roberto Bruttomesso ; Silvio Ghilardi ; Silvio Ranise.
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier- free interpolants in general. In this paper, we show that it is possible to obtain quantifier-free interpolants for a Skolemized version of the extensional theory of arrays. We prove this in two ways: (1) non-constructively, by using the model theoretic notion of amalgamation, which is known to be equivalent to admit quantifier-free interpolation for universal theories; and (2) constructively, by designing an interpolating procedure, based on solving equations between array updates. (Interestingly, rewriting techniques are used in the key steps of the solver and its proof of correctness.) To the best of our knowledge, this is the first successful attempt of computing quantifier- free interpolants for a variant of the theory of arrays with extensionality.

3. Modes of Convergence for Term Graph Rewriting

Patrick Bahr.
Term graph rewriting provides a simple mechanism to finitely represent restricted forms of infinitary term rewriting. The correspondence between infinitary term rewriting and term graph rewriting has been studied to some extent. However, this endeavour is impaired by the lack of an appropriate counterpart of infinitary rewriting on the side of term graphs. We aim to fill this gap by devising two modes of convergence based on a partial order respectively a metric on term graphs. The thus obtained structures generalise corresponding modes of convergence that are usually studied in infinitary term rewriting. We argue that this yields a common framework in which both term rewriting and term graph rewriting can be studied. In order to substantiate our claim, we compare convergence on term graphs and on terms. In particular, we show that the modes of convergence on term graphs are conservative extensions of the corresponding modes of convergence on terms and are preserved under unravelling term graphs to terms. Moreover, we show that many of the properties known from infinitary term rewriting are preserved. This includes the intrinsic completeness of both modes of convergence and the fact that convergence via the partial order is a conservative extension of the metric convergence.

4. Dynamic Dependency Pairs for Algebraic Functional Systems

Cynthia Kop ; Femke van Raamsdonk.
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate {\beta}-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.

5. Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Naoki Nishida ; Masahiko Sakai ; Toshiki Sakabe.
Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling.

6. A Rewriting View of Simple Typing

Aaron Stump ; Garrin Kimmell ; Hans Zantema ; Ruba El Haj Omar.
This paper shows how a recently developed view of typing as small-step abstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast the development of simple type theory from a rewriting perspective. We show how standard meta-theoretic results can be proved in a completely new way, using the rewriting view of simple typing. These meta-theoretic results include standard type preservation and progress properties for simply typed lambda calculus, as well as generalized versions where typing is taken to include both abstract and concrete reduction. We show how automated analysis tools developed in the term-rewriting community can be used to help automate the proofs for this meta-theory. Finally, we show how to adapt a standard proof of normalization of simply typed lambda calculus, for the rewriting approach to typing.