Rewriting Techniques and Applications

Frontmatter

Modular Termination of Basic Narrowing

Abstract

Basic narrowing is a restricted form of narrowing which constrains narrowing steps to a set of non-blocked (or basic) positions. Basic narrowing has a number of important applications including equational unification in canonical theories. Another application is analyzing termination of narrowing by checking the termination of basic narrowing, as done in pioneering work by Hullot. In this work, we study the modularity of termination of basic narrowing in hierarchical combinations of TRSs, including a generalization of proper extensions with shared subsystem. This provides new algorithmic criteria to prove termination of basic narrowing.

María Alpuente, Santiago Escobar, José Iborra

Linear-algebraic λ-calculus: higher-order, encodings, and confluence.

Abstract

We introduce a minimal language combining higher-order computation and linear algebra. This language extends the λ-calculus with the possibility to make arbitrary linear combinations of terms α.t + β.u. We describe how to “execute” this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally we prove the confluence of the calculus, this is our main result.

Pablo Arrighi, Gilles Dowek

Term-Graph Rewriting Via Explicit Paths

Abstract

The notion of path is classical in graph theory but not directly used in the term rewriting community. The main idea of this work is to raise the notion of path to the level of first-order terms, i.e. paths become part of the terms and not just meta-information about them. These paths are represented by words of integers (positive or negative) and are interpreted as relative addresses in terms. In this way, paths can also be seen as a generalization of the classical notion of position for the first-order terms and are inspired by de Bruijn indexes.

In this paper, we define an original framework called Referenced Term Rewriting where paths are used to represent pointers between subterms. Using this approach, any term-graph rewriting systems can be simulated using a term rewrite-based environment.

Emilie Balland, Pierre-Etienne Moreau

Finer Is Better: Abstraction Refinement for Rewriting Approximations

Abstract

Term rewriting systems are now commonly used as a modeling language for programs or systems. On those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth-Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term t can be shown by computing an over-approximation of the set of reachable terms and prove that t is not in the over-approximation. However, when the term t is in the approximation, nothing can be said.

In this paper, we improve this approach as follows: given a term t, we try to compute an over-approximation which does not contain t by using an approximation refinement that we propose. If the approximation refinement fails then t is a reachable term. This semi-algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the interest of such an approach w.r.t. verification on rewriting models.

Yohan Boichut, Roméo Courbis, Pierre-Cyrille Héam, Olga Kouchnarenko

A Needed Rewriting Strategy for Data-Structures with Pointers

Abstract

We propose a reduction strategy for systems of rewrite rules operating on term-graphs. These term-graphs are intended to encode pointer-based data-structures that are commonly used in programming, with cycles and sharing. We show that this reduction strategy is optimal w.r.t. a given dependency schema, which intuitively encodes the “interferences” among the nodes in the term-graphs. We provide a new way of computing such dependency schemata.

Rachid Echahed, Nicolas Peltier

Effectively Checking the Finite Variant Property

Abstract

An equational theory decomposed into a set B of equational axioms and a set Δ of rewrite rules has the finite variant (FV) property in the sense of Comon-Lundh and Delaune iff for each term t there is a finite set {t ₁,...,t _n } of →_Δ,B-normalized instances of t so that any instance of t normalizes to an instance of some t _i modulo B. This is a very useful property for cryptographic protocol analysis, and for solving both unification and disunification problems. Yet, at present the property has to be established by hand, giving a separate mathematical proof for each given theory: no checking algorithms seem to be known. In this paper we give both a necessary and a sufficient condition for FV from which we derive an algorithm ensuring the sufficient condition, and thus FV. This algorithm can check automatically a number of examples of FV known in the literature.

Santiago Escobar, José Meseguer, Ralf Sasse

Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures

Abstract

This paper defines an expressive class of constrained equational rewrite systems that supports the use of semantic data structures (e.g., sets or multisets) and contains built-in numbers, thus extending our previous work presented at CADE 2007 [6]. These rewrite systems, which are based on normalized rewriting on constructor terms, allow the specification of algorithms in a natural and elegant way. Built-in numbers are helpful for this since numbers are a primitive data type in every programming language. We develop a dependency pair framework for these rewrite systems, resulting in a flexible and powerful method for showing termination that can be automated effectively. Various powerful techniques are developed within this framework, including a subterm criterion and reduction pairs that need to consider only subsets of the rules and equations. It is well-known from the dependency pair framework for ordinary rewriting that these techniques are often crucial for a successful automatic termination proof. Termination of a large collection of examples can be established using the presented techniques.

Stephan Falke, Deepak Kapur

Maximal Termination

Abstract

We present a new approach for termination proofs that uses polynomial interpretations (with possibly negative coefficients) together with the “maximum” function. To obtain a powerful automatic method, we solve two main challenges: (1) We show how to adapt the latest developments in the dependency pair framework to our setting. (2) We show how to automate the search for such interpretations by integrating “ max ” into recent SAT-based methods for polynomial interpretations. Experimental results support our approach.

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl

Usable Rules for Context-Sensitive Rewrite Systems

Abstract

Recently, the dependency pairs (DP) approach has been generalized to context-sensitive rewriting (CSR). Although the context-sensitive dependency pairs (CS-DP) approach provides a very good basis for proving termination of CSR, the current developments basically correspond to a ten-years-old DP approach. Thus, the task of adapting all recently introduced dependency pairs techniques to get a more powerful approach becomes an important issue. In this direction, usable rules are one of the most interesting and powerful notions. Actually usable rule have been investigated in connection with proofs of innermost termination of CSR. However, the existing results apply to a quite restricted class of systems. In this paper, we introduce a notion of usable rules that can be used in proofs of termination of CSR with arbitrary systems. Our benchmarks show that the performance of the CS-DP approach is much better when such usable rules are considered in proofs of termination of CSR.

Raúl Gutiérrez, Salvador Lucas, Xavier Urbain

Combining Equational Tree Automata over AC and ACI Theories

Abstract

In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories \({\mathcal{E}}_1\) and \({\mathcal{E}}_2\) imply similar decidability results in the combined theory \({\mathcal{E}}_1 \cup {\mathcal{E}}_2\); (2) checking emptiness of a language obtained from the Boolean combination of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a non-modular property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule f(x,x) →x rather than an equation f(x,x) = x, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If \({\mathcal{E}}\) contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular \({\mathcal{E}}\)-tree languages?

Joe Hendrix, Hitoshi Ohsaki

Closure of Hedge-Automata Languages by Hedge Rewriting

Abstract

We consider rewriting systems for unranked ordered terms, i.e. trees where the number of successors of a node is not determined by its label, and is not a priori bounded. The rewriting systems are defined such that variables in the rewrite rules can be substituted by hedges (sequences of terms) instead of just terms. Consequently, this notion of rewriting subsumes both standard term rewriting and word rewriting.

We investigate some preservation properties for two classes of languages of unranked ordered terms under this generalization of term rewriting. The considered classes include languages of hedge automata (HA) and some extension (called CF-HA) with context-free languages in transitions, instead of regular languages.

In particular, we show that the set of unranked terms reachable from a given HA language, using a so called inverse context-free rewrite system, is a HA language. The proof, based on a HA completion procedure, reuses and combines known techniques with non-trivial adaptations. Moreover, we prove, with different techniques, that the closure of CF-HA languages with respect to restricted context-free rewrite systems, the symmetric case of the above rewrite systems, is a CF-HA language. As a consequence, the problems of ground reachability and regular hedge model checking are decidable in both cases. We give several counter examples showing that we cannot relax the restrictions.

Florent Jacquemard, Michael Rusinowitch

On Normalisation of Infinitary Combinatory Reduction Systems

Abstract

For fully-extended, orthogonal infinitary Combinatory Reduction Systems, we prove that terms with perpetual reductions starting from them do not have (head) normal forms. Using this, we show that

1

needed reduction strategies are normalising for fully-extended, orthogonal infinitary Combinatory Reduction Systems, and that

 

1

weak and strong normalisation coincide for such systems as a whole and, in case reductions are non-erasing, also for terms.

 

Jeroen Ketema

Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems

Abstract

A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the reachability is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.

In this paper, we show that innermost reachability and contextsensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties.

Yoshiharu Kojima, Masahiko Sakai

Arctic Termination ...Below Zero

Abstract

We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with -∞,with the operations ”max” and ”plus”. This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the Dependency Pairs transformation, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers ”below zero”: integers extended with -∞.This allows to treat some termination problems with symbols that require a predecessor semantics. The contents of the paper has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method. We also report on experiments with an implementation of this method which, compared to results from 2007, outperforms TPA (winner of the certified termination competition for term rewriting), and in the string rewriting category is as powerful as Matchbox was but now all of the proofs are certified.

Adam Koprowski, Johannes Waldmann

Logics and Automata for Totally Ordered Trees

Abstract

A totally ordered tree is a tree equipped with an additional total order on its nodes. It provides a formal model for data that comes with both a hierarchical and a sequential structure; one example for such data are natural language sentences, where a sequential structure is given by word order, and a hierarchical structure is given by grammatical relations between words. In this paper, we study monadic second-order logic (MSO) for totally ordered terms. We show that the MSO satisfiability problem of unrestricted structures is undecidable, but give a decision procedure for practically relevant sub-classes, based on tree automata.

Marco Kuhlmann, Joachim Niehren

Diagram Rewriting for Orthogonal Matrices: A Study of Critical Peaks

Abstract

Orthogonal diagrams represent decompositions of isometries of ℝ ⁿ into symmetries and rotations. Some convergent (that is noetherian and confluent) rewrite system for this structure was introduced by the first author. One of the rules is similar to Yang-Baxter equation. It involves a map h : ]0, π[³ →]0, π[³.

In order to obtain the algebraic properties of h, we study the confluence of critical peaks (or critical pairs) for our rewrite system. For that purpose, we introduce parametric diagrams describing the calculation of angles of rotations generated by rewriting. In particular, one of those properties is related to the tetrahedron equation (also called Zamolodchikov equation).

Yves Lafont, Pierre Rannou

Nominal Unification from a Higher-Order Perspective

Abstract

Nominal Logic is an extension of first-order logic with equality, name-binding, name-swapping, and freshness of names. Contrarily to higher-order logic, bound variables are treated as atoms, and only free variables are proper unknowns in nominal unification. This allows “variable capture”, breaking a fundamental principle of lambda-calculus. Despite this difference, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be reduced to a particular fragment of higher-order unification problems: higher-order patterns unification. This reduction proves that nominal unification can be decided in quadratic deterministic time.

Jordi Levy, Mateu Villaret

Functional-Logic Graph Parser Combinators

Abstract

Parser combinators are a popular technique among functional programmers for writing parsers. They allow the definition of parsers for string languages in a manner quite similar to BNF rules. In recent papers we have shown that the combinator approach is also beneficial for graph parsing. However, we have noted as well that certain graph languages are difficult to describe in a purely functional way.

In this paper we demonstrate that functional-logic languages can be used to conveniently implement graph parsers. Therefore, we provide a direct mapping from hyperedge replacement grammars to graph parsers. As in the string setting, our combinators closely reflect the building blocks of this grammar formalism. Finally, we show by example that our framework is strictly more powerful than hyperedge replacement grammars.

We make heavy use of key features of both the functional and the logic programming approach: Higher-order functions allow the treatment of parsers as first class citizens. Non-determinism and logical variables are beneficial for dealing with errors and incomplete information. Parsers can even be applied backwards and thus be used as generators or for graph completion.

Steffen Mazanek, Mark Minas

Proving Quadratic Derivational Complexities Using Context Dependent Interpretations

Abstract

In this paper we study context dependent interpretations, a semantic termination method extending interpretations over the natural numbers, introduced by Hofbauer. We present two subclasses of context dependent interpretations and establish tight upper bounds on the induced derivational complexities. In particular we delineate a class of interpretations that induces quadratic derivational complexity. Furthermore, we present an algorithm for mechanically proving termination of rewrite systems with context dependent interpretations. This algorithm has been implemented and we present ample numerical data for the assessment of the viability of the method.

Georg Moser, Andreas Schnabl

Tree Automata for Non-linear Arithmetic

Abstract

Tree automata modulo associativity and commutativity axioms, called AC tree automata, accept trees by iterating the transition modulo equational reasoning. The class of languages accepted by monotone AC tree automata is known to include the solution set of the inequality \(x \times y \geqslant z\), which implies that the class properly includes the AC closure of regular tree languages. In the paper, we characterize more precisely the expressiveness of monotone AC tree automata, based on the observation that, in addition to polynomials, a class of exponential constraints (called monotone exponential Diophantine inequalities) can be expressed by monotone AC tree automata with a minimal signature. Moreover, we show that a class of arithmetic logic consisting of monotone exponential Diophantine inequalities is definable by monotone AC tree automata. The results presented in the paper are obtained by applying our novel tree automata technique, called linearly bounded projection.

Naoki Kobayashi, Hitoshi Ohsaki

Confluence by Decreasing Diagrams

Converted

Abstract

The decreasing diagrams technique is a complete method to reduce confluence of a rewrite relation to local confluence. Whereas previous presentations have focussed on the proof the technique is correct, here we focus on applicability. We present a simple but powerful generalisation of the technique, requiring peaks to be closed only by conversions instead of valleys, which is demonstrated to further ease applicability.

Vincent van Oostrom

A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case

Abstract

The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as non-determinism, makes known approaches to prove that simulation implies contextual preorder, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.

Manfred Schmidt-Schauss, Elena Machkasova

Root-Labeling

Abstract

In 2006 Jambox, a termination prover developed by Endrullis, surprised the termination community by winning the string rewriting division and almost beating AProVE in the term rewriting division of the international termination competition. The success of Jambox for strings is partly due to a very special case of semantic labeling. In this paper we integrate this technique, which we call root-labeling, into the dependency pair framework. The result is a simple processor with help of which T _T T ₂ surprised the termination community in 2007 by producing the first automatically generated termination proof of a string rewrite system with non-primitive recursive complexity (Touzet, 1998). Unlike many other recent termination methods, the root-labeling processor is trivial to automate and completely unsuitable for producing human readable proofs.

Christian Sternagel, Aart Middeldorp

Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities

Abstract

We propose a new (Noetherian) induction schema to reason on equalities and show how to integrate it into implicit induction-based inference systems. Non-orientable conjectures of the form lhs = rhs and their instances can be soundly used as induction hypotheses in rewrite operations. It covers the most important rewriting-based induction proof techniques: i)term rewriting induction if lhs = rhs is orientable, ii) enhanced rewriting induction if lhs and rhs are comparable, iii)ordered rewriting induction if the instances of lhs = rhs are orientable, and iv) relaxed rewriting induction if the instances of lhs = rhs are not comparable.In practice, it helps to automatize the (rewrite-based) reasoning on a larger class of non-orientable equalities, like the permutative and associativity equalities.

Sorin Stratulat

Deciding Innermost Loops

Abstract

We present the first method to disprove innermost termination of term rewrite systems automatically. To this end, we first develop a suitable notion of an innermost loop. Second, we show how to detect innermost loops: One can start with any technique amenable to find loops. Then our novel procedure can be applied to decide whether a given loop is an innermost loop. We implemented and successfully evaluated our method in the termination prover AProVE.

René Thiemann, Jürgen Giesl, Peter Schneider-Kamp

Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations

Abstract

S-expression rewriting systems were proposed by the author (RTA 2004) for termination analysis of Lisp-like untyped higher-order functional programs. This paper presents a short and direct proof for the fact that every finite S-expression rewriting system is terminating if it is compatible with a recursive path relation with status. By considering well-founded binary relations instead of well-founded orders, we give a much simpler proof than the one depending on Kruskal’s tree theorem.

Yoshihito Toyama

Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting

Abstract

Fine-grained reformulation of the lambda calculus is expected to solve several difficulties with the notion of substitutions—definition, implementation and cost properties. However, previous attempts including those using explicit substitutions and those using Interaction Nets were not ideally simple when it came to the encoding of the pure (as opposed to weak) lambda calculus. This paper presents a novel, fine-grained, and highly asynchronous encoding of the pure lambda calculus using LMNtal, a hierarchical graph rewriting language, and discusses its properties. The major strength of the encoding is that it is significantly simpler than previous encodings, making it promising as an alternative formulation, rather than just the encoding, of the pure lambda calculus. The membrane construct of LMNtal plays an essential role in encoding colored tokens and operations on them. The encoding has been tested using the publicly available LMNtal implementation.

Kazunori Ueda

Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof

Abstract

Powerful proof techniques, such as logical relation arguments, have been developed for establishing the strong normalisation property of term- rewriting systems. The first author used such a logical relation argument to establish strong normalising for a cut-elimination procedure in classical logic. He presented a rather complicated, but informal, proof establishing this property. The difficulties in this proof arise from a quite subtle substitution operation, which implements proof transformation that permute cuts over other inference rules. We have formalised this proof in the theorem prover Isabelle/HOL using the Nominal Datatype Package, closely following the informal proof given by the first author in his PhD-thesis. In the process, we identified and resolved a gap in one central lemma and a number of smaller problems in others. We also needed to make one informal definition rigorous. We thus show that the original proof is indeed a proof and that present automated proving technology is adequate for formalising such difficult proofs.

Christian Urban, Bozhi Zhu

Reduction Under Substitution

Abstract

The Reduction-under-Substitution Lemma (RuS) , due to van Daalen [Daa80] , provides an answer to the following question concerning the lambda calculus: given a reduction \(M[{x}:={L}] \twoheadrightarrow N\), what can we say about the contribution of the substitution to the result N. It is related to a not very well-known lemma that was conjectured by Barendregt in the early 70’s, addressing the similar question as to the contribution of the argument M in a reduction \(FM \twoheadrightarrow N\). The origin of Barendregt’s Lemma lies in undefinablity proofs, whereas van Daalen’s interest came from its application to the so-called Square Brackets Lemma, which is used in proofs of strong normalization.

In this paper we compare various forms of RuS. We strengthen RuS to multiple substitution and context filling and show how it can be used to give short and perspicuous proofs of undefinability results. Most of these are known as consequences of Berry’s Sequentiality Theorem, but some fall outside its scope. We show that RuS can also be used to prove the sequentiality theorem itself. To that purpose we give a further adaptation of RuS, now also involving “bottom” reduction rules, sending unsolvable terms to a bottom element and in the limit producing Böhm trees.

Jörg Endrullis, Roel de Vrijer

Normalization of Infinite Terms

Abstract

We investigate the property SN ^∞ being the natural concept related to termination when considering term rewriting applied to infinite terms. It turns out that this property can be fully characterized by a variant of monotone algebras equipped with a metric. A fruitful special case is obtained when the algebra is finite and the required metric properties are obtained for free. It turns out that the matrix method can be applied to find proofs of SN ^∞ based on these observations. In this way SN ^∞ can be proved fully automatically for some interesting examples related to combinatory logic.

Hans Zantema

Backmatter