Two-Way Equational Tree Automata for AC-Like Theories: Decidability and Closure Properties
Kumar Neeraj Verma
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.
Rule-Based Analysis of Dimensional Safety
Feng Chen, Grigore Roşu, Ram Prasad Venkatesan
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.
On the Complexity of Higher-Order Matching in the Linear lambda-Calculus
Sylvain Salvati, Philippe de Groote
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 Schema, Tree Logic and Sheaves Automata
Silvano Dal-Zilio, Denis Lugiez
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.
Size-Change Termination for Term Rewriting
René Thiemann, Jürgen Giesl
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.
Monotonic AC-Compatible Semantic Path Orderings
Cristina Borralleras, Albert Rubio
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.
Relating Derivation Lengths with the Slow-Growing Hierarchy Directly
Georg Moser, Andreas Weiermann
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.
Tsukuba Termination Tool
Nao Hirokawa, Aart Middeldorp
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.
Liveness in Rewriting
Jürgen Giesl, Hans Zantema
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.
Validation of the JavaCard Platform with Implicit Induction Techniques
Gilles Barthe, Sorin Stratulat
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.
Term Partition for Mathematical Induction
Pascal Urso, Emmanuel Kounalis
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 A is a monomorphic set of axioms (rules) and (a, b) is a term partition of t, then the normal form (obtained by using A ) of any ground instance of t can be "divided" into the normal forms (obtained by using 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 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.
Equational Prover of THEOREMA
Temur Kutsia
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.
Termination of Simply Typed Term Rewriting by Translation and Labelling
Takahito Aoto, Toshiyuki Yamada
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.
Rewriting Modulo in Deduction Modulo
Frédéric Blanqui
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.
Termination of String Rewriting Rules That Have One Pair of Overlaps
Alfons Geser
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.
Environments for Term Rewriting Engines for Free
Mark van den Brand, Pierre-Étienne Moreau, Jurgen J. Vinju
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.
A Rewriting Alternative to Reidemeister-Schreier
Neil Ghani, Anne Heyworth
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.
Stable Computational Semantics of Conflict-Free Rewrite Systems (Partial Orders with Duplication)
Zurab Khasidashvili, John R. W. Glauert
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.
Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism
Hitoshi Ohsaki, Hiroyuki Seki, Toshinori Takai
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.
Testing Extended Regular Language Membership Incrementally by Rewriting
Grigore Roşu, Mahesh Viswanathan
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.
2002
Axiomatic Rewriting Theory VI Residual Theory Revisited
Paul-André Melliès
Residual theory is the algebraic theory of confluence for the λ-calculus, and more generally conflict-free rewriting systems (=without critical pairs). The theory took its modern shape in Lévy's PhD thesis, after Church, Rosser and Curry's seminal steps. There, Lévy introduces a permutation equivalence between rewriting paths, and establishes that among all confluence diagrams P → N ← Q completing a span P ← M → Q, there exists a minimum such one, modulo permutation equivalence. Categorically, the diagram is called a pushout.
In this article, we extend Lévy's residual theory, in order to enscope "border-line" rewriting systems, which admit critical pairs but enjoy a strong Church-Rosser property (=existence of pushouts.) Typical examples are the associativity rule and the positive braid rewriting systems. Finally, we show that the resulting theory reformulates and clarifies Lévy's optimality theory for the λ-calculus, and its so-called "extraction procedure".
Static Analysis of Modularity of beta-Reduction in the Hyperbalanced lambda-Calculus
Richard Kennaway, Zurab Khasidashvili, Adolfo Piperno
We investigate the degree of parallelism (or modularity) in the hyperbalanced λ-calculus, λH, a subcalculus of λ-calculus containing all simply typable terms (up to a restricted η-expansion). In technical terms, we study the family relation on redexes in λH, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced λ-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of β-reduction.
Exceptions in the Rewriting Calculus
Germain Faure, Claude Kirchner
In the context of the rewriting calculus, we introduce and study an exception mechanism that allows us to express in a simple way rewriting strategies and that is therefore also useful for expressing theorem proving tactics. The proposed exception mechanism is expressed in a confluent calculus which gives the ability to simply express the semantics of the first tactical and to describe in full details the expression of conditional rewriting.
Deriving Focused Lattice Calculi
Georg Struth
We derive rewrite-based ordered resolution calculi for semilattices, distributive lattices and boolean lattices. Using ordered resolution as a metaprocedure, theory axioms are first transformed into independent bases. Focused inference rules are then extracted from inference patterns in refutations. The derivation is guided by mathematical and procedural background knowledge, in particular by ordered chaining calculi for quasiorderings (forgetting the lattice structure), by ordered resolution (forgetting the clause structure) and by Knuth-Bendix completion for non-symmetric transitive relations (forgetting both structures). Conversely, all three calculi are derived and proven complete in a transparent and generic way as special cases of the lattice calculi.
Layered Transducing Term Rewriting System and Its Recognizability Preserving Property
Hiroyuki Seki, Toshinori Takai, Youhei Fujinaka, Yuichi Kaji
A term rewriting system which effectively preserves recognizability (EPR-TRS) has good mathematical properties. In this paper, a new subclass of TRSs, layered transducing TRSs (LT-TRSs) is defined and its recognizability preserving property is discussed. The class of LT-TRSs contains some EPR-TRSs, e.g., f(x) → f(g(x)) which do not belong to any of the known decidable subclasses of EPR-TRSs. Bottom-up linear tree transducer, which is a well-known computation model in the tree language theory, is a special case of LT-TRS. We present a sufficient condition for an LT-TRS to be an EPR-TRS. Also some properties of LT-TRSs including reachability are shown to be decidable.
Decidability and Closure Properties of Equational Tree Languages
Hitoshi Ohsaki, Toshinori Takai
Equational tree automata provide a powerful tree language framework that facilitates to recognize congruence closures of tree languages. In the paper we show the emptiness problem for AC-tree automata and the intersection-emptiness problem for regular AC-tree automata, each of which was open in our previous work [20], are decidable, by a straightforward reduction to the reachability problem for ground AC-term rewriting. The newly obtained results generalize decidability of so-called reachable property problem of Mayr and Rusinowitch [17]. We then discuss complexity issue of AC-tree automata. Moreover, in order to solve some other questions about regular A- and AC-tree automata, we recall the basic connection between word languages and tree languages.
Regular Sets of Descendants by Some Rewrite Strategies
Pierre Réty, Julie Vuotto
For a constructor-based rewrite system R, a regular set of ground terms E, and assuming some additional restrictions, we build a finite tree automaton that recognizes the descendants of E, i.e. the terms issued from E by rewriting, according to innermost, innermost-leftmost, and outermost strategies.
Rewrite Games
Johannes Waldmann
For a terminating rewrite system R, and a ground term t1, two players alternate in doing R-reductions t1 →R t2 →R t3 →R ... That is, player 1 choses the redex in t1, t3,..., and player 2 choses the redex in t2, t4,... The player who cannot move (because tn is a normal form), loses.
In this note, we propose some challenging problems related to certain rewrite games. In particular, we re-formulate an open problem from combinatorial game theory (do all finite octal games have an ultimately periodic Sprague-Grundy sequence?) as a question about rationality of some tree languages.
We propose to attack this question by methods from set constraint systems, and show some cases where this works directly.
Finally we present rewrite games from to combinatory logic, and their relation to algebraic tree languages.
An Extensional Böhm Model
Paula Severi, Fer-Jan de Vries
We show the existence of an infinitary confluent and normalising extension of the finite extensional lambda calculus with beta and eta. Besides infinite beta reductions also infinite eta reductions are possible in this extension, and terms without head normal form can be reduced to bottom. As corollaries we obtain a simple, syntax based construction of an extensional Böhm model of the finite lambda calculus; and a simple, syntax based proof that two lambda terms have the same semantics in this model if and only if they have the same eta-Böhm tree if and only if they are observationally equivalent wrt to beta normal forms. The confluence proof reduces confluence of beta, bottom and eta via infinitary commutation and postponement arguments to confluence of beta and bottom and confluence of eta.
We give counterexamples against confluence of similar extensions based on the identification of the terms without weak head normal form and the terms without top normal form (rootactive terms) respectively.
A Weak Calculus with Explicit Operators for Pattern Matching and Substitution
Julien Forest
In this paper we propose a Weak Lambda Calculus called λPw having explicit operators for Pattern Matching and Substitution. This formalism is able to specify functions defined by cases via pattern matching constructors as done by most modern functional programming languages such as OCAML. We show the main property enjoyed by λPw, namely subject reduction, confluence and strong normalization.
Tradeoffs in the Intensional Representation of Lambda Terms
Chuck Liang, Gopalan Nadathur
Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined: the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.
Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen
A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NF-CTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NF-CTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.
Conditions for Efficiency Improvement by Tree Transducer Composition
Janis Voigtländer
We study the question of efficiency improvement or deterioration for a semantic-preserving program transformation technique based on macro tree transducer composition. By annotating functional programs to reflect the internal property "computation time" explicitly in the computed output, and by manipulating such annotations, we formally prove syntactic conditions under which the composed program is guaranteed to be more efficient than the original program, with respect to call-by-need reduction to normal form. The developed criteria can be checked automatically, and thus are suitable for integration into an optimizing functional compiler.
Rewriting Strategies for Instruction Selection
Martin Bravenboer, Eelco Visser
Instruction selection (mapping IR trees to machine instructions) can be expressed by means of rewrite rules. Typically, such sets of rewrite rules are highly ambiguous. Therefore, standard rewriting engines based on fixed, exhaustive strategies are not appropriate for the execution of instruction selection. Code generator generators use special purpose implementations employing dynamic programming. In this paper we show how rewriting strategies for instruction selection can be encoded concisely in Stratego, a language for program transformation based on the paradigm of programmable rewriting strategies. This embedding obviates the need for a language dedicated to code generation, and makes it easy to combine code generation with other optimizations.
Probabilistic Rewrite Strategies. Applications to ELAN
Olivier Bournez, Claude Kirchner
Recently rule based languages focussed on the use of rewriting as a modeling tool which results in making specifications executable. To extend the modeling capabilities of rule based languages, we explore the possibility of making the rule applications subject to probabilistic choices.
We propose an extension of the ELAN strategy language to deal with randomized systems. We argue through several examples that we propose indeed a natural setting to model systems with randomized choices. This leads us to interesting new problems, and we address the generalization of the usual concepts in abstract reduction systems to randomized systems.
Loops of Superexponential Lengths in One-Rule String Rewriting
Alfons Geser
Loops are the most frequent cause of non-termination in string rewriting. In the general case, non-terminating, non-looping string rewriting systems exist, and the uniform termination problem is undecidable. For rewriting with only one string rewriting rule, it is unknown whether non-terminating, non-looping systems exist and whether uniform termination is decidable. If in the one-rule case, non-termination is equivalent to the existence of loops, as McNaughton conjectures, then a decision procedure for the existence of loops also solves the uniform termination problem. As the existence of loops of bounded lengths is decidable, the question is raised how long shortest loops may be. We show that string rewriting rules exist whose shortest loops have superexponential lengths in the size of the rule.
Recursive Derivational Length Bounds for Confluent Term Rewrite Systems
Elias Tahhan-Bittar
Let F be a signature and R a term rewrite system on ground terms of F. We define the concepts of a context-free potential redex in a term and of bounded confluent terms. We bound recursively the lengths of derivations of a bounded confluent term t by a function of the length of derivations of context-free potential redexes of this term. We define the concept of inner redex and we apply the recursive bounds that we obtained to prove that, whenever R is a confluent overlay term rewrite system, the derivational length bound for arbitrary terms is an iteration of the derivational length bound for inner redexes.
Termination of (Canonical) Context-Sensitive Rewriting
Salvador Lucas
Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. A replacement map discriminates, for each symbol of the signature, the argument positions on which replacements are allowed. If the replacement restrictions are less restrictive than those expressed by the so-called canonical replacement map, then CSR can be used for computing (infinite) normal forms of terms. Termination of such canonical CSR is desirable when using CSR for these purposes. Existing transformations for proving termination of CSR fulfill a number of new properties when used for proving termination of canonical CSR.
Atomic Set Constraints with Projection
Witold Charatonik, Jean-Marc Talbot
We investigate a class of set constraints defined as atomic set constraints augmented with projection. This class subsumes some already studied classes such as atomic set constraints with left-hand side projection and INES constraints. All these classes enjoy the nice property that satisfiability can be tested in cubic time. This is in contrast to several other classes of set constraints, such as definite set constraints and positive set constraints, for which satisfiability ranges from DEXPTIME-complete to NEXPTIME-complete. However, these latter classes allow set operators such as intersection or union which is not the case for the class studied here. In the case of atomic set constraints with projection one might expect that satisfiability remains polynomial. Unfortunately, we show that that the satisfiability problem for this class is no longer polynomial, but CoNP-hard. Furthermore, we devise a PSPACE algorithm to solve this satisfiability problem.
Currying Second-Order Unification Problems
Jordi Levy, Mateu Villaret
The Curry form of a term, like f(a, b), allows us to write it, using just a single binary function symbol, as @(@(f,a),b). Using this technique we prove that the signature is not relevant in second-order unification, and conclude that one binary symbol is enough.
By currying variable applications, like X(a), as @(X,a), we can transform second-order terms into first-order terms, but we have to add beta-reduction as a theory. This is roughly what it is done in explicit unification. We prove that by currying only constant applications we can reduce second-order unification to second-order unification with just one binary function symbol. Both problems are already known to be undecidable, but applying the same idea to context unification, for which decidability is still unknown, we reduce the problem to context unification with just one binary function symbol.
We also discuss about the difficulties of applying the same ideas to third or higher order unification.
A Decidable Variant of Higher Order Matching
Daniel J. Dougherty, Tomasz Wierzbicki
A lambda term is k-duplicating if every occurrence of a lambda abstractor binds at most k variable occurrences. We prove that the problem of higher order matching where solutions are required to be k-duplicating (but with no constraints on the problem instance itself) is decidable. We also show that the problem of higher order matching in the affine lambda calculus (where both the problem instance and the solutions are constrained to be 1-duplicating) is in NP, generalizing de Groote's result for the linear lambda calculus [4].
Combining Decision Procedures for Positive Theories Sharing Constructors
Franz Baader, Cesare Tinelli
This paper addresses the following combination problem: given two equational theories E1 and E2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of E1 ∪ E2? For theories over disjoint signatures, this problem was solved by Baader and Schulz in 1995. This paper is a first step towards extending this result to the case of theories sharing constructors. Since there is a close connection between positive theories and unification problems, this also extends to the non-disjoint case the work on combining decision procedures for unification modulo equational theories.
JITty: A Rewriter with Strategy Annotations
Jaco van de Pol
We demonstrate JITty, a simple rewrite implementation with strategy annotations, along the lines of the Just-In-Time rewrite strategy, explained and justified in [4]. Our tool has the following distinguishing features:
Autowrite: A Tool for Checking Properties of Term Rewriting Systems
Irène Durand
Huet and Lévy [6] showed that for the class of orthogonal term rewriting systems (TRSs) every term not in normal form contains a needed redex (i.e., a redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results in a normal form if it exists. However, neededness is in general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs.
TTSLI: An Implementation of Tree-Tuple Synchronized Languages
Benoit Lecland, Pierre Réty
Tree-Tuple Synchronized Languages have first been introduced by means of Tree-Tuple Synchronized Grammars (TTSG) [3], and have been reformulated recently by means of (so-called) Constraint Systems (CS), which allowed to prove more properties [2,1]. A number of applications to rewriting and to concurrency have been presented (see [5] for a survey).
in2 : A Graphical Interpreter for Interaction Nets
Sylvain Lippi
in2 can be considered as an attractive and didactic tool to approach the interaction net paradigm. But it is also an implementation in C of the core of a real programming language featuring a user-friendly graphical syntax and an efficient garbage collector free execution.
2001
Universal Interaction Systems with Only Two Agents
Denis Béchet
In the framework of interaction nets [6], Yves Lafont has proved [8] that every interaction system can be simulated by a system composed of 3 symbols named γ, δ and ε. One may wonder if it is possible to find a similar universal system with less symbols. In this paper, we show a way to simulate every interaction system with a specific interaction system constituted of only 2 symbols. By transitivity, we prove that we can find a universal interaction system with only 2 agents. Moreover, we show how to find such a system where agents have no more than 3 auxiliary ports.
General Recursion on Second Order Term Algebras
Alessandro Berarducci, Corrado Böhm
Extensions of the simply typed lambda calculus have been used as a metalanguage to represent "higher order term algebras", such as, for instance, formulas of the predicate calculus. In this representation bound variables of the object language are represented by bound variables of the metalanguage. This choice has various advantages but makes the notion of "recursive definition" on higher order term algebras more subtle than the corresponding notion on first order term algebras. Despeyroux, Pfenning and Schürmann pointed out the problems that arise in the proof of a canonical form theorem when one combines higher order representations with primitive recursion.
In this paper we consider a stronger scheme of recursion and we prove that it captures all partial recursive functions on second order term algebras. We illustrate the system by considering typed programs to reduce to normal form terms of the untyped lambda calculus, encoded as elements of a second order term algebra. First order encodings based on de Bruijn indexes are also considered. The examples also show that a version of the intersection type disciplines can be helpful in some cases to prove the existence of a canonical form. Finally we consider interpretations of our typed systems in the pure lambda calculus and a new gödelization of the pure lambda calculus.
Beta Reduction Constraints
Manuel Bodirsky, Katrin Erk, Alexander Koller, Joachim Niehren
The constraint language for lambda structures (CLLS) can model lambda terms that are known only partially. In this paper, we introduce beta reduction constraints to describe beta reduction steps between partially known lambda terms. We show that beta reduction constraints can be expressed in an extension of CLLS by group parallelism. We then extend a known semi-decision procedure for CLLS to also deal with group parallelism and thus with beta-reduction constraints.
From Higher-Order to First-Order Rewriting
Eduardo Bonelli, Delia Kesner, Alejandro Ríos
We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory ε. We obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε = 0). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitution calculus used in the translation.
Combining Pattern E-Unification Algorithms
Alexandre Boudet, Évelyne Contejean
We present an algorithm for unification of higher-order patterns modulo combinations of disjoint first-order equational theories. This algorithm is highly non-deterministic, in the spirit of those by Schmidt-Schauß [20] and Baader-Schulz [1] in the first-order case. We redefine the properties required for elementary pattern unification algorithms of pure problems in this context, then we show that some theories of interest have elementary unification algorithms fitting our requirements. This provides a unification algorithm for patterns modulo the combination of theories such as the free theory, commutativity, one-sided distributivity, associativity-commutativity and some of its extensions, including Abelian groups.
Matching Power
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
In this paper we give a simple and uniform presentation of the rewriting calculus, also called Rho Calculus. In addition to its simplicity, this formulation explicitly allows us to encode complex structures such as lists, sets, and objects. We provide extensive examples of the calculus, and we focus on its ability to represent some object oriented calculi, namely the Lambda Calculus of Objects of Fisher, Honsell, and Mitchell, and the Object Calculus of Abadi and Cardelli. Furthermore, the calculus allows us to get object oriented constructions unreachable in other calculi. In summa, we intend to show that because of its matching ability, the Rho Calculus represents a lingua franca to naturally encode many paradigms of computations. This enlightens the capabilities of the rewriting calculus based language ELAN to be used as a logical as well as powerful semantical framework.
Dependency Pairs for Equational Rewriting
Jürgen Giesl, Deepak Kapur
The dependency pair technique of Arts and Giesl [1,2,3] for termination proofs of term rewrite systems (TRSs) is extended to rewriting modulo equations. Up to now, such an extension was only known in the special case of AC-rewriting [15,17]. In contrast to that, the proposed technique works for arbitrary non-collapsing equations (satisfying a certain linearity condition). With the proposed approach, it is now possible to perform automated termination proofs for many systems where this was not possible before. In other words, the power of dependency pairs can now also be used for rewriting modulo equations.
Termination Proofs by Context-Dependent Interpretations
Dieter Hofbauer
Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated.
Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.
Uniform Normalisation beyond Orthogonality
Zurab Khasidashvili, Mizuhito Ogawa, Vincent van Oostrom
A rewrite system is called uniformly normalising if all its steps are perpetual, i.e. are such that if s → t and s has an infinite reduction, then t has one too. For such systems termination (SN) is equivalent to normalisation (WN). A well-known fact is uniform normalisation of orthogonal non-erasing term rewrite systems, e.g. the λI-calculus. In the present paper both restrictions are analysed. Orthogonality is seen to pertain to the linear part and non-erasingness to the non-linear part of rewrite steps. Based on this analysis, a modular proof method for uniform normalisation is presented which allows to go beyond orthogonality. The method is shown applicable to biclosed first- and second-order term rewrite systems as well as to a λ-calculus with explicit substitutions.
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order
Konstantin Korovin, Andrei Voronkov
We consider two decision problems related to the Knuth-Bendix order (KBO). The first problem is orientability: given a system of rewrite rules R, does there exist some KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given KBO orients a rewrite rule. This problem can also be reformulated as the problem of solving a single ordering constraint for the KBO. We prove that both problems can be solved in polynomial time. The algorithm builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. Also we show that if a system is orientable using a real-valued KBO, then it is also orientable using an integer-valued KBO.
Relating Accumulative and Non-accumulative Functional Programs
Armin Kühnemann, Robert Glück, Kazuhiko Kakehi
We study the problem to transform functional programs, which intensively use append functions (like inefficient list reversal), into programs, which use accumulating parameters instead (like eficient list reversal). We give an (automatic) transformation algorithm for our problem and identify a class of functional programs, namely restricted 2-modular tree transducers, to which it can be applied. Moreover, since we get macro tree transducers as transformation result and since we also give the inverse transformation algorithm, we have a new characterization for the class of functions induced by macro tree transducers.
Context Unification and Traversal Equations
Jordi Levy, Mateu Villaret
Context unification was originally defined by H. Comon in ICALP'92, as the problem of finding a unifier for a set of equations containing first-order variables and context variables. These context variables have arguments, and can be instantiated by contexts. In other words, they are second-order variables that are restricted to be instantiated by linear terms (a linear term is a λ-expression λx1...λxn.t where every xi occurs exactly once in t).
In this paper, we prove that, if the so called rank-bound conjecture is true, then the context unification problem is decidable. This is done reducing context unification to solvability of traversal equations (a kind of word unification modulo certain permutations) and then, reducing traversal equations to word equations with regular constraints.
Weakly Regular Relations and Applications
Sébastien Limet, Pierre Réty, Helmut Seidl
A new class of tree-tuple languages is introduced: the weakly regular relations. It is an extension of the regular case (regular relations) and a restriction of tree-tuple synchronized languages, that has all usual nice properties, except closure under complement. Two applications are presented: to unification modulo a rewrite system, and to one-step rewriting.
On the Parallel Complexity of Tree Automata
Markus Lohrey
We determine the parallel complexity of several (uniform) membership problems for recognizable tree languages. Furthermore we show that the word problem for a fixed finitely presented algebra is in DLOGTIME-uniform NC1.
Transfinite Rewriting Semantics for Term Rewriting Systems
Salvador Lucas
We provide some new results concerning the use of transfinite rewriting for giving semantics to rewrite systems. We especially (but not only) consider the computation of possibly infinite constructor terms by transfinite rewriting due to their interest in many programming languages. We reconsider the problem of compressing transfinite rewrite sequences into shorter (possibly finite) ones. We also investigate the role that (finitary) con uence plays in transfinite rewriting. We consider different (quite standard) rewriting semantics (mappings from input terms to sets of reducts obtained by (transfinite-rewriting) in a unified framework and investigate their algebraic structure. Such a framework is used to formulate, connect, and approximate different properties of TRSs.
Goal-Directed E-Unification
Christopher Lynch, Barbara Morawska
We give a general goal directed method for solving the E-unification problem. Our inference system is a generalization of the inference rules for Syntactic Theories, except that our inference system is proved complete for any equational theory. We also show how to easily modify our inference system into a more restricted inference system for Syntactic Theories, and show that our completeness techniques prove completeness there also.
The Unification Problem for Confluent Right-Ground Term Rewriting Systems
Michio Oyamaguchi, Yoshikatsu Ohta
The unification problem for term rewriting systems(TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R (i.e., Mθ ↔*R Nθ). In this paper, the unification problem for con uent right-ground TRSs is shown to be decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm of obtaining a substitution whose range is in minimal terms is proposed. Our result extends the decidability of unification for canonical (i.e., confluent and terminating) right-ground TRSs given by Hullot (1980) in the sense that the termination condition can be omitted. It is also exemplified that Hullot's narrowing technique does not work in this case. Our result is compared with the undecidability of the word (and also unification) problem for terminating right-ground TRSs.
On Termination of Higher-Order Rewriting
Femke van Raamsdonk
We discuss the termination methods using the higher-order recursive path ordering and the general scheme for higher-order rewriting systems and combinatory reduction systems.
Matching with Free Function Symbols - A Simple Extension of Matching
Christophe Ringeissen
Matching is a solving process which is crucial in declarative (rule-based) programming languages. In order to apply rules, one has to match the left-hand side of a rule with the term to be rewritten. In several declarative programming languages, programs involve operators that may also satisfy some structural axioms. Therefore, their evaluation mechanism must implement powerful matching algorithms working modulo equational theories. In this paper, we show the existence of an equational theory where matching is decidable (resp. finitary) but matching in presence of additional (free) operators is undecidable (resp. infinitary). The interest of this result is to easily prove the existence of a frontier between matching and matching with free operators.
Deriving Focused Calculi for Transitive Relations
Georg Struth
We propose a new method for deriving focused ordered resolution calculi, exemplified by chaining calculi for transitive relations. Previously, inference rules were postulated and a posteriori verified in semantic completeness proofs. We derive them from the theory axioms. Completeness of our calculi then follows from correctness of this synthesis. Our method clearly separates deductive and procedural aspects: relating ordered chaining to Knuth-Bendix completion for transitive relations provides the semantic background that drives the synthesis towards its goal. This yields a more restrictive and transparent chaining calculus. The method also supports the development of approximate focused calculi and a modular approach to theory hierarchies.
A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names
René Vestergaard, James Brotherston
We present the titular proof development which has been implemented in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive induction principles of the standard syntax and the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show (i) that our presentation coincides with Curry's and Hindley's when terms are considered equal up-to α and (ii) that the con uence properties of all considered calculi are equivalent.
A Normal Form for Church-Rosser Language Systems
Jens R. Woinowski
In this paper the context-splittable normal form for rewritings systems defining Church-Rosser languages is introduced. Context-splittable rewriting rules look like rules of context-sensitive grammars with swapped sides. To be more precise, they have the form uvw → uxw with u, v, w being words, v being nonempty and x being a single letter or the empty word. It is proved that this normal form can be achieved for each Church-Rosser language and that the construction is effective.
Confluence and Termination of Simply Typed Term Rewriting Systems
Toshiyuki Yamada
We propose simply typed term rewriting systems (STTRSs), which extend first-order rewriting by allowing higher-order functions. We study a simple proof method for con uence which employs a characterization of the diamond property of a parallel reduction. By an application of the proof method, we obtain a new con uence result for orthogonal conditional STTRSs. We also discuss a semantic method for proving termination of STTRSs based on monotone interpretation.
Parallel Evaluation of Interaction Nets with MPINE
Jorge Sousa Pinto
We describe the MPINE tool, a multi-threaded evaluator for Interaction Nets. The evaluator is an implementation of the present author's Abstract Machine for Interaction Nets [5] and uses POSIX threads to achieve concurrent execution. When running on a multi-processor machine (say an SMP architecture), parallel execution is achieved effortlessly, allowing for desktop parallelism on commonly available machines.
Stratego: A Language for Program Transformation Based on Rewriting Strategies
Eelco Visser
Program transformation is used in many areas of software engineering. Examples include compilation, optimization, synthesis, refactoring, migration, normalization and improvement [15]. Rewrite rules are a natural formalism for expressing single program transformations. However, using a standard strategy for normalizing a program with a set of rewrite rules is not adequate for implementing program transformation systems. It may be necessary to apply a rule only in some phase of a transformation, to apply rules in some order, or to apply a rule only to part of a program. These restrictions may be necessary to avoid non-termination or to choose a specific path in a non-con uent rewrite system.
Stratego is a language for the specification of program transformation systems based on the paradigm of rewriting strategies. It supports the separation of strategies from transformation rules, thus allowing careful control over the application of these rules. As a result of this separation, transformation rules are reusable in multiple difierent transformations and generic strategies capturing patterns of control can be described independently of the transformation rules they apply. Such strategies can even be formulated independently of the object language by means of the generic term traversal capabilities of Stratego.
In this short paper I give a description of version 0.5 of the Stratego system, discussing the features of the language (Section 2), the library (Section 3), the compiler (Section 4) and some of the applications that have been built (Section 5). Stratego is available as free software under the GNU General Public License from http://www.stratego-language.org.
2000
Absolute Explicit Unification
Nikolaj Bjørner, César A. Muñoz
This paper presents a system for explicit substitutions in Pure Type Systems (PTS). The system allows to solve type checking, type inhabitation, higher-order unification, and type inference for PTS using purely first-order machinery. A novel feature of our system is that it combines substitutions and variable declarations. This allows as a side-effect to type check let-bindings. Our treatment of meta-variables is also explicit, such that instantiations of meta-variables is internalized in the calculus. This produces a confluent λ-calculus with distinguished holes and explicit substitutions that is insensitive to α-conversion, and allows directly embedding the system into rewriting logic.
Termination and Confluence of Higher-Order Rewrite Systems
Frédéric Blanqui
In the last twenty years, several approaches to higher-order rewriting have been proposed, among which Klop's Combinatory Rewrite Systems (CRSs), Nipkow's Higher-order Rewrite Systems (HRSs) and Jouannaud and Okada's higher-order algebraic specification languages, of which only the last one considers typed terms. The later approach has been extended by Jouannaud, Okada and the present author into Inductive Data Type Systems (IDTSs). In this paper, we extend IDTSs with the CRS higher-order pattern-matching mechanism, resulting in simply-typed CRSs. Then, we show how the termination criterion developed for IDTSs with first-order pattern-matching, called the General Schema, can be extended so as to prove the strong normalization of IDTSs with higher-order pattern-matching. Next, we compare the unified approach with HRSs. We first prove that the extended General Schema can also be applied to HRSs. Second, we show how Nipkow's higher-order critical pair analysis technique for proving local confluence can be applied to IDTSs.
A de Bruijn Notation for Higher-Order Rewriting
Eduardo Bonelli, Delia Kesner, Alejandro Ríos
We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express general higher-order rewrite systems. We give formal translations from higher-order rewriting with names to higher-order rewriting with de Bruijn indices, and vice-versa. These translations can be viewed as an interface in programming languages based on higher-order rewrite systems, and they are also used to show some properties, namely, that both formalisms are operationally equivalent, and that confluence is preserved when translating one formalism into the other.
Rewriting Techniques in Theoretical Physics
Évelyne Contejean, Antoine Coste, Benjamin Monate
This paper presents a general method for studying some quotients of the special linear group SL2 over the integers, which are of fundamental interest in the field of statistical physics. Our method automatically helps in validating some conjectures due to physicists, such as conjectures stating that a set of equations completely describes a finite given quotient of SL2. In a first step, we show that in the cases we are interested in, the usual presentation of finitely generated groups with some constant generators and a binary concatenation can be turned into an equivalent one with unary generators. In a second step, when the completion of the transformed set of equations terminates, we show how to compute directly the associated normal forms automaton. According to the presence of loops, we are able to decide the finiteness of the quotient, and to compute its cardinality. When the quotient is infinite, the automaton gives some hints on what kind of equations are needed in order to insure the finiteness of the quotient.
Normal Forms and Reduction for Theories of Binary Relations
Daniel J. Dougherty, Claudio Gutiérrez
We consider equational theories of binary relations, in a language expressing composition, converse, and lattice operations. We treat the equations valid in the standard model of sets and also define a hierarchy of equational axiomatisations stratifying the standard theory. By working directly with a presentation of relation-expressions as graphs we are able to define a notion of reduction which is confluent and strongly normalising, in sharp contrast to traditional treatments based on first-order terms. As consequences we obtain unique normal forms, decidability of the decision problem for equality for each theory. In particular we show a non-deterministic polynomial-time upper bound for the complexity of the decision problems.
Parallelism Constraints
Katrin Erk, Joachim Niehren
Parallelism constraints are logical descriptions of trees. They are as expressive as context unification, i.e. second-order linear unification. We present a semi-decision procedure enumerating all 'most general unifiers' of a parallelism constraint and prove it sound and complete. In contrast to all known procedures for context unification, the presented procedure terminates for the important fragment of dominance constraints and performs reasonably well in a recent application to underspecified natural language semantics.
Linear Higher-Order Matching Is NP-Complete
Philippe de Groote
We consider the problem of higher-order matching restricted to the set of linear λ-terms (i.e., λ-terms where each abstraction λx. M is such that there is exactly one free occurrence of x in M). We prove that this problem is decidable by showing that it belongs to NP. Then we prove that this problem is in fact NP-complete. Finally, we discuss some heuristics for a practical algorithm.
Standardization and Confluence for a Lambda Calculus with Generalized Applications
Felix Joachimski, Ralph Matthes
As a minimal environment for the study of permutative reductions an extension ΛJ of the untyped λ-calculus is considered. In this non-terminating system with non-trivial critical pairs, confluence is established by studying triangle properties that allow to treat permutative reductions modularly and could be extended to more complex term systems with permutations. Standardization is shown by means of an inductive definition of standard reduction that closely follows the inductive term structure and captures the intuitive notion of standardness even for permutative reductions.
Linear Second-Order Unification and Context Unification with Tree-Regular Constraints
Jordi Levy, Mateu Villaret
Linear Second-Order Unification and Context Unification are closely related problems. However, their equivalence was never formally proved. Context unification is a restriction of linear second-order unification. Here we prove that linear second-order unification can be reduced to context unification with tree-regular constraints.
Decidability of context unification is still an open question. We comment on the possibility that linear second-order unification is decidable, if context unification is, and how to get rid of the tree-regular constraints. This is done by reducing rank-bound tree-regular constraints to word-regular constraints.
Word Problems and Confluence Problems for Restricted Semi-Thue Systems
Markus Lohrey
We investigate word problems and confluence problems for the following four classes of terminating semi-Thue systems: length-reducing systems, weight-reducing systems, length-lexicographic systems, and weight-lexicographic systems. For each of these four classes we determine the complexity of several variants of the word problem and confluence problem. Finally we show that the variable membership problem for quasi context-sensitive grammars is EXPSPACE-complete.
The Explicit Representability of Implicit Generalizations
Reinhard Pichler
In [9], implicit generalizations over some Herbrand universe H were introduced as constructs of the form I = t/t1 ∨ ... ∨ tm with the intended meaning that I represents all H-ground instances of t that are not instances of any term ti on the right-hand side. More generally, we can also consider disjunctions I = I1 ∨ ... ∨ In of implicit generalizations, where I contains all ground terms from H that are contained in at least one of the implicit generalizations Ij. Implicit generalizations have applications to many areas of Computer Science. For the actual work, the so-called finite explicit representability problem plays an important role, i.e.: Given a disjunction of implicit generalizations I = I1 ∨ ... ∨ In, do there exist terms r1,...,rl, s.t. the ground terms represented by I coincide with the union of the H-ground instances of the terms rj? In this paper, we prove the coNP-completeness of this decision problem.
On the Word Problem for Combinators
Richard Statman
In 1936 Alonzo Church observed that the "word problem" for combinators is undecidable. He used his student Kleene's representation of partial recursive functions as lambda terms. This illustrates very well the point that "word problems" are good problems in the sense that a solution either way - decidable or undecidable - can give useful information. In particular, this undecidability proof shows us how to program arbitrary partial recursive functions as combinators.
I never thought that this result was the end of the story for combinators. In particular, it leaves open the possibility that the unsolvable problem can be approximated by solvable ones. It also says nothing about word problems for interesting fragments i.e., sets of combinators not combinatorially complete.
Perhaps the most famous subproblem is the problem for S terms. Recently, Waldmann has made significant progress on this problem. Prior, we solved the word problem for the Lark, a relative of S. Similar solutions can be given for the Owl (S*) and Turing's bird U. Familiar decidable fragments include linear combinators and various sorts of typed combinators. Here we would like to consider several fragments of much greater scope. We shall present several theorems and an open problem.
An Algebra of Resolution
Georg Struth
We propose an algebraic reconstruction of resolution as Knuth-Bendix completion. The basic idea is to model propositional ordered Horn resolution and resolution as rewrite-based solutions to the uniform word problems for semilattices and distributive lattices. Completion for non-symmetric transitive relations and a variant of symmetrization normalize and simplify the presentation. The procedural content of resolution, its refutational completeness and redundancy elimination techniques thereby reduce to standard algebraic completion techniques. The reconstruction is analogous to that of the Buchberger algorithm by equational completion.
Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems
Jürgen Stuber
We show how to derive refutationally complete ground superposition calculi systematically from convergent term rewriting systems for equational theories, in order to make automated theorem proving in these theories more effective. In particular we consider abelian groups and commutative rings. These are difficult for automated theorem provers, since their axioms of associativity, commutativity, distributivity and the inverse law can generate many variations of the same equation. For these theories ordering restrictions can be strengthened so that inferences apply only to maximal summands, and superpositions into the inverse law that move summands from one side of an equation to the other can be replaced by an isolation rule that isolates the maximal terms on one side. Additional inferences arise from superpositions of extended clauses, but we can show that most of these are redundant. In particular, none are needed in the case of abelian groups, and at most one for any pair of ground clauses in the case of commutative rings.
Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability
Toshinori Takai, Yuichi Kaji, Hiroyuki Seki
Right-linear finite path overlapping TRS are shown to effectively preserve recognizability. The class of right-linear finite path overlapping TRS properly includes the class of linear generalized semi-monadic TRS and the class of inverse left-linear growing TRS, which are known to effectively preserve recognizability. Approximations by inverse right-linear finite path overlapping TRS are also discussed.
System Description: The Dependency Pair Method
Thomas Arts
The dependency pair method refers to the approach for proving (innermost) termination of term rewriting systems by showing that no infinite chain of so-called dependency pairs exists (for an overview of the method see [AG00]). The method generates inequalities that should be satisfied by a suitable well-founded ordering. Well-known techniques for searching simplification orderings (such as path orderings or polynomial interpretations) may be used to find such an ordering. The key point is that, even if the TRS is not simply terminating, the dependency pair method often generates a set of inequalities that can be satisfied by a simplification ordering and herewith can prove termination of the TRS.
REM (Reduce Elan Machine): Core of the New ELAN Compiler
Pierre-Étienne Moreau
ELAN is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. It offers a natural and simple logical framework for the combination of the computation and deduction paradigms. It supports the design of theorem provers, logic programming languages, constraint solvers and decision procedures.
TALP: A Tool for the Termination Analysis of Logic Programs
Enno Ohlebusch, Claus Claves, Claude Marché
In the last decade, the automatic termination analysis of logic programs has been receiving increasing attention. Among other methods, techniques have been proposed that transform a well-moded logic program into a term rewriting system (TRS) so that termination of the TRS implies termination of the logic program under Prolog's selection rule. In [Ohl99] it has been shown that the two-stage transformation obtained by combining the transformations of [GW93] into deterministic conditional TRSs (CTRSs) with a further transformation into TRSs [CR93] yields the transformation proposed in [AZ96], and that these three transformations are equally powerful. In most cases simplification orderings are not sufficient to prove termination of the TRSs obtained by the two-stage transformation. However, if one uses the dependency pair method [AG00] in combination with polynomial interpretations instead, then most of the examples described in the literature can automatically be proven terminating. Based on these observations, we have implemented a tool for proving termination of logic programs automatically. This tool consists of a front-end which implements the two-stage transformation and a back-end, the CiME system [CiM], for proving termination of the generated TRS. Experiments show that our tool can compete with other tools [DSV99 ]based on sophisticated norm-based approaches.
1999
Solved Forms for Path Ordering Constraints
Robert Nieuwenhuis, José Miguel Rivero
A usual technique in symbolic constraint solving is to apply transformation rules until a solved form is reached for which the problem becomes simple. Ordering constraints are well-known to be reducible to (a disjunction of) solved forms, but unfortunately no polynomial algorithm deciding the satisfiability of these solved forms is known.
Here we deal with a different notion of solved form, where fundamental properties of orderings like transitivity and monotonicity are taken into account. This leads to a new family of constraint solving algorithms for the full recursive path ordering with status (RPOS), and hence as well for other path orderings like LPO, MPO, KNS and RDO, and for all possible total precedences and signatures. Apart from simplicity and elegance from the theoretical point of view, the main contribution of these algorithms is on efficiency in practice. Since guessing is minimized, and, in particular, no linear orderings between the subterms are guessed, a practical improvement in performance of several orders of magnitude over previous algorithms is obtained, as shown by our experiments.
Jeopardy
Nachum Dershowitz, Subrata Mitra
We consider functions defined by ground-convergent left-linear rewrite systems. By restricting the depth of left sides and disallowing defined symbols at the top of right sides, we obtain an algorithm for function inversion.
Strategic Pattern Matching
Eelco Visser
Stratego is a language for the specification of transformation rules and strategies for applying them. The basic actions of transformations are matching and building instantiations of first-order term patterns. The language supports concise formulation of generic and data type-specific term traversals. One of the unusual features of Stratego is the separation of scope from matching, allowing sharing of variables through traversals. The combination of first-order patterns with strategies forms an expressive formalism for pattern matching. In this paper we discuss three examples of strategic pattern matching: (1) Contextual rules allow matching and replacement of a pattern at an arbitrary depth of a subterm of the root pattern. (2) Recursive patterns can be used to characterize concisely the structure of languages that form a restriction of a larger language. (3) Overlays serve to hide the representation of a language in another (more generic) language. These techniques are illustrated by means of specifications in Stratego.
On the Strong Normalisation of Natural Deduction with Permutation-Conversions
Philippe de Groote
We present a modular proof of the strong normalisation of intuitionistic logic with permutation-conversions. This proof is based on the notions of negative translation and CPS-simulation.
Normalisation in Weakly Orthogonal Rewriting
Vincent van Oostrom
A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. Outermost-fair rewriting is known to be (head-)normalising for almost orthogonal rewrite systems. We study (head-)normalisation for the larger class of weakly orthogonal rewrite systems. (Infinitary) normalisation is established and a counterexample against head-normalisation is given.
Strong Normalization of Proof Nets Modulo Structural Congruences
Roberto Di Cosmo, Stefano Guerrini
This paper proposes a notion of reduction for the proof nets of Linear Logic modulo an equivalence relation on the contraction links, that essentially amounts to consider the contraction as an associative commutative binary operator that can float freely in and out of proof net boxes. The need for such a system comes, on one side, from the desire to make proof nets an even more parallel syntax for Linear Logic, and on the other side from the application of proof nets to l-calculus with or without explicit substitutions, which needs a notion of reduction more flexible than those present in the literature. The main result of the paper is that this relaxed notion of rewriting is still strongly normalizing.
Undecidability of the exists*forall* Part of the Theory of Ground Term Algebra Modulo an AC Symbol
Jerzy Marcinkowski
We show that the ∃*∀* part of the equational theory modulo an AC symbol is undecidable. This solves the open problem 25 from the RTA list ([DJK91],[DJK93],[DJK95]).
Deciding the Satisfiability of Quantifier free Formulae on One-Step Rewriting
Anne-Cécile Caron, Franck Seynhaeve, Sophie Tison, Marc Tommasi
We consider quantifier free formulae of a first order theory without functions and with predicates x rewrites to y in one step with given rewrite systems. Variables are interpreted in the set of finite trees. The full theory is undecidable [Tre96] and recent results [STT97], [Mar97], [Vor97] have strengthened the undecidability result to formulae with small prefixes (∃*∀*) and very restricted classes of rewriting systems (e.g. linear, shallow and convergent in [STTT98]). Decidability of the positive existential fragment has been shown in [NPR97]. We give a decision procedure for positive and negative existential formulae in the case when the rewrite systems are quasi-shallow, that is all variables in the rewrite rules occur at depth one. Our result extends to formulae with equalities and memberships relations of the form x ∈ L where L is a recognizable set of terms.
A New Result about the Decidability of the Existential One-Step Rewriting Theory
Sébastien Limet, Pierre Réty
We give a decision procedure for the whole existential fragment of one-step rewriting first-order theory, in the case where rewrite systems are linear, non left-left-overlapping (i.e. without critical pairs), and non ∈-left-right-overlapping (i.e. no left-hand-side overlaps on top with the right-hand-side of the same rewrite rule). The procedure is defined by means of tree-tuple synchronized grammars.
A Fully Syntactic AC-RPO
Albert Rubio
We present the first fully syntactic (i.e., non-interpretationbased) AC-compatible recursive path ordering (RPO). It is simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. The ordering is AC-total, and defined uniformly for both ground and non-ground terms, as well as for partial precedences. More importantly, it is the first one that can deal incrementally with partial precedences, an aspect that is essential, together with its intuitive behaviour, for interactive applications like Knuth-Bendix completion.
Theory Path Orderings
Jürgen Stuber
We introduce the notion of a theory path ordering (TPO), which simplifies the construction of term orderings for superposition theorem proving in algebraic theories. To achieve refutational completeness of such calculi we need total, E-compatible and E-antisymmetric simplification quasi-orderings. The construction of a TPO takes as its ingredients a status function for interpreted function symbols and a precedence that makes the interpreted function symbols minimal. The properties of the ordering then follow from related properties of the status function. Theory path orderings generalize associative path orderings.
A Characterisation of Multiply Recursive Functions with Higman's Lemma
Hélène Touzet
We prove that string rewriting systems which reduce by Higman's lemma exhaust the multiply recursive functions. This result provides a full characterisation of the expressiveness of Higman's lemma when applied to rewriting theory. The underlying argument of our construction is to connect the order type and the derivation length via the Hardy hierarchy.
Deciding the Word Problem in the Union of Equational Theories Sharing Constructors
Franz Baader, Cesare Tinelli
The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories sharing "constructors." The notion of constructors adopted in this paper has a nice algebraic definition and is more general than a related notion introduced in previous work on the combination problem.
Normalization via Rewrite Closures
Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari
We present an abstract completion-based method for finding normal forms of terms with respect to given rewrite systems. The method uses the concept of a rewrite closure, which is a generalization of the idea of a congruence closure. Our results generalize previous results on congruence closure-based normalization methods. The description of known methods within our formalism also allows a better understanding of these procedures.
Test Sets for the Universal and Existential Closure of Regular Tree Languages
Dieter Hofbauer, Maria Huber
Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large.
In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.
The Maude System
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Jose F. Quesada
TODO
TOY : A Multiparadigm Declarative System
Francisco Javier López-Fraguas, Jaime Sánchez-Hernández
TOY is the concrete implementation of CRWL, a wide theoretical framework for declarative programming whose basis is a constructor based rewriting logic with lazy non-deterministic functions as the core notion. Other aspects of CRWL supported by TOY are: polymorphic types; HO features; equality and disequality constraints over terms and linear constraints over real numbers; goal solving by needed narrowing combined with constraint solving. The implementation is based on a compilation of TOY programs into Prolog.
UNIMOK: A System for Combining Equational Unification Algorithm
Stephan Kepser, Jörn Richts
TODO
L→R2 : A Laboratory for Rapid Term Graph Rewriting
Rakesh M. Verma, Shalitha Senanayake
TODO
Decidability for Left-Linaer Growing Term Rewriting Systems
Takashi Nagaya, Yoshihito Toyama
A term rewriting system is called growing if each variable occurring both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-non-linear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for rightground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems.
Transforming Context-Sensitive Rewrite Systems
Jürgen Giesl, Aart Middeldorp
We present two new transformation techniques for proving termination of context-sensitive rewriting. Our first method is simple, sound, and more powerful than previously suggested transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. This latter result can be interpreted as stating that from a termination perspective there is no reason to study context-sensitive rewriting.
Context-Sensitive AC-Rewriting
Maria C. F. Ferreira, A. L. Ribeiro
Context-sensitive rewriting was introduced in [7] and consists of syntactical restrictions imposed on a Term Rewriting System indicating how reductions can be performed. So context-sensitive rewriting is a restriction of the usual rewrite relation which reduces the reduction space and allows for a finer control of the reductions of a term. In this paper we extend the concept of context-sensitive rewriting to the framework rewriting modulo an associative-commutative theory in two ways: by restricting reductions and restricting AC-steps, and we then study this new relation with respect to the property of termination.
The Calculus of algebraic Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types equipped with higher-order primitive recursion, by providing definitions of functions by pattern-matching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition. CAC also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules.
HOL-λσ : An Intentional First-Order Expression of Higher-Order Logic
Gilles Dowek, Thérèse Hardin, Claude Kirchner
We propose a first-order presentation of higher-order logic based on explicit substitutions. It is intentionally equivalent to the usual presentation of higher-order logic based on λ-calculus, i.e. a proposition can be proved without the extensionality axioms in one theory if and only if it can in the other. The tiExtended Narrowing and Resolution first-order proof-search method can be applied to this theory. This allows to simulate higher-order resolution step by step and furthermore leaves room for further optimizations and extensions.
A Rewrite System Associated with Quadratic Pisot Units
Christiane Frougny, Jacques Sakarovitch
The main point is to show that the rewrite system made up by the relations that generate γθ, though non-confluent, behaves as if it were confluent.
Fast Rewriting of Symmetric Polynomials
Manfred Göbel
This note presents a fast version of the classical algorithm to represent any symmetric function in a unique way as a polynomial in the elementary symmetric polynomials by using power sums of variables. We analyze the worst case complexity for both algorithms, the original and the fast version, and confirm our results by empirical run-time experiments. Our main result is a fast algorithm with a polynomial worst case complexity w.r.t. the total degree of the input polynomial compared to the classical algorithm with its exponential worst case complexity.
On Implementation of Tree Synchronized Languages
Frédéric Saubion, Igor Stéphan
Tree languages have been extensively studied and have many applications related to the rewriting framework such as order sorted specifications, higher order matching or unification. In this paper, we focus on the implementation of such languages and, inspired by the Definite Clause Grammars that allows to write word grammars as Horn clauses in a Prolog environment, we propose to build a similar framework for particular tree languages (TTSG) which introduces a notion of synchronization between production rules. Our main idea is to define a proof theoretical semantics for grammars and thus to change from syntactical tree manipulations to logical deduction. This is achieved by a sequent calculus proof system which can be refined and translated into Prolog Horn clauses. This work provides a scheme to build goal directed procedures for the recognition of tree languages.
1998
Simultaneous Critical Pairs and Church-Rosser Property
Satoshi Okui
We introduce simultaneous critical pairs, which account for simultaneous overlapping of several rewrite rules. Based on this, we introduce a new CR-criterion widely applicable to arbitrary left-linear term rewriting systems. Our result extends the well-known criterion given by Huet (1980), Toyama (1988), and Oostrom (1997) and incomparable with other well-known criteria for left-linear systems.
Church-Rosser Theorems for Abstract Reduction Modulo an Equivalence Relation
Enno Ohlebusch
A very powerful method for proving the Church-Rosser property for abstract rewriting systems has been developed by van Oostrom. In this paper, his technique is extended in two ways to abstract rewriting modulo an equivalence relation. It is shown that known Church-Rosser theorems can be viewed as special cases of the new criteria. Moreover, applications of the new criteria yield several new results.
Automatic Monoids Versus Monoids with Finite Convergent Presentations
Friedrich Otto, Andrea Sattler-Klein, Klaus Madlener
Due to their many nice properties groups with automatic structure (automatic groups) have received a lot of attention in the literature. The multiplication of an automatic group can be realized through finite automata based on a regular set of (not necessarily unique) representatives for the group, and hence, each automatic group has a tractable word problem and low derivational complexity. Consequently it has been asked whether corresponding results also hold for monoids with automatic structure. Here we show that there exist finitely presented monoids with automatic structure that cannot be presented through finite and convergent string-rewriting systems, thus answering a question in the negative that is still open for the class of automatic groups. Secondly, we present an automatic monoid that has an exponential derivational complexity, which establishes another difference to the class of automatic groups. In fact, both our example monoids are bi-automatic. In addition, it follows from the first of our examples that a monoid which is given through a finite, noetherian, and weakly confluent string-rewriting system need not have finite derivation type.
Decidable and Undecidable Second-Order Unification Problems
Jordi Levy
There is a close relationship between word unification and second-order unification. This similarity has been exploited for instance for proving decidability of monadic second-order unification. Word unification. can be easily decided by transformation rules (similar to the ones applied in higher-order unification procedures) when variables are restricted to occur at most twice. Hence a well-known open question was the decidability of second-order unification under this same restriction. Here we answer this question negatively by reducing simultaneous rigid E-unification to second-order unification. This reduction, together with an inverse reduction found by Degtyarev and Voronkov, states an equivalence relationship between both unification problems.
Our reduction is in some sense reversible, providing decidability results for cases when simultaneous rigid E-unification is decidable. This happens, for example, for one-variable problems where the variable occurs at most twice (because rigid E-unification is decidable for just one equation). We also prove decidability when no variable occurs more than once, hence significantly narrowing the gap between decidable and undecidable second-order unification problems with variable occurrence restrictions.
On the Exponent of Periodicity of Minimal Solutions of Context Equation
Manfred Schmidt-Schauß, Klaus U. Schulz
Context unification is a generalisation of string unification where words are generalized to terms with one hole. Though decidability of string unification was proved by Makanin, the decidability of context unification is currently an open question. This paper provides a step in understanding the complexity of context unification and the structure of unifiers. It is shown, that if a context unification problem of size d is unifiable, then there is also a unifier with an exponent of periodicity smaller than O(21.07d). We also prove NP-hardness for restricted cases of the context unification problem and compare the complexity of general context unification with that of general string unification.
Unification in Extension of Shallow Equational Theories
Florent Jacquemard, Christoph Meyer, Christoph Weidenbach
We show that unification in certain extensions of shallow equational theories is decidable. Our extensions generalize the known classes of shallow or standard equational theories. In order to prove decidability of unification in the extensions, a class of Horn clause sets called sorted shallow equational theories is introduced. This class is a natural extension of tree automata with equality constraints between brother subterms as well as shallow sort theories. We show that saturation under sorted superposition is effective on sorted shallow equational theories. So called semi-linear equational theories can be effectively transformed into equivalent sorted shallow equational theories and generalize the classes of shallow and standard equational theories.
Unification and Matching in Process Algebras
Qing Guo, Paliath Narendran, Sandeep K. Shukla
We consider the compatibility checking problem for a simple fragment of CCS, called BCCSP[12], using equational unification techniques. Two high-level specifications given as two process algebraic terms with free variables are said to be compatible modulo some equivalence relation if a substitution on the free variables can make the resulting terms equivalent modulo that relation. We formulate this compatibility (modulo an equivalence relation) checking problems as unification problems in the equational theory of the the corresponding equivalence relation. We use van Glabbeek's equational axiomatizations [12] for some interesting process algebraic relations. Specifically, we consider equational axiomatizations for bisimulation equivalence and trace equivalence and establish complexity lower bounds and upper bounds for the corresponding unification and matching problems. We also show some special cases for which efficient algorithmic solutions exist.
E-Unification for Subsystems of S4
Renate A. Schmidt
This paper is concerned with the unification problem in the path logics associated by the optimised functional translation method with the propositional modal logics K, KD, KT, KD4, S4 and S5. It presents improved unification algorithms for certain forms of the right identity and associativity laws. The algorithms employ mutation rules, which have the advantage that terms are worked off from the outside inward, making paramodulating into terms superfluous.
Solving Disequations Modulo Some Class of Rewrite Systems
Sébastien Limet, Pierre Réty
This paper gives a procedure for solving disequations modulo equational theories, and to decide existence of solutions. For this, we assume that the equational theory is specified by a confluent and constructor-based rewrite system, and that four additional restrictions are satisfied. The procedure represents the possibly infinite set of solutions thanks to a grammar, and decides existence of solutions thanks to an emptiness test. As a consequence, checking whether a linear equality is an inductive theorem is decidable, if assuming moreover sufficient completeness.
Normalization of S-Terms is Decidable
Johannes Waldmann
The combinator S has the reduction rule S x y z ↝ x z (y z). We investigate properties of ground terms built from S alone. We show that it is decidable whether such an S-term has a normal form. The decision procedure makes use of rational tree languages. We also exemplify and summarize other properties of S-terms and hint at open questions.
Decidable Approximations of Sets of Descendants and Sets of Normal Forms
Thomas Genet
We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the context of rewriting logic, a Term Rewriting System is a program, and a normal form is a result of the program. Thus, approximations of sets of descendants and sets of normal forms provide tools for analysing a few properties of programs: we show how to compute a superset of results, to prove the sufficient completeness property, or to find a criterion for proving termination under a specific strategy, the sequential reduction strategy. The main technical contribution of the paper is the construction of an approximation automaton which recognises a superset of the set of normal forms of terms in a set E, w.r.t. a Term Rewriting System R.
Algorithms and Reductions for Rewriting Problems
Rakesh M. Verma, Michaël Rusinowitch, Denis Lugiez
In this paper we initiate a study of polynomial-time reductions for some basic decision problems of rewrite systems. We then give a polynomial-time algorithm for Unique-normal-form property of ground systems for the first time. Next we prove undecidability of these problems for a fixed string rewriting system using our reductions. Finally, we prove partial decidability results for Confluence of commutative semi-thue systems. The Confluence and Unique-normal-form property are shown Expspace-hard for commutative semi-thue systems. We also show that there is a family of string rewrite systems for which the word problem is trivially decidable but confluence undecidable, and we show a linear equational theory with decidable word problem but undecidable linear equational matching.
The Decidability of Simultaneous Rigid E-Unification with One Variable
Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
We show that simultaneous rigid E-unification, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the ∀*∃∀* fragment of intuitionistic logic with equality is decidable. Together with a previous result regarding the undecidability of the ∃∃-fragment, we obtain a complete classification of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix. It is also proved that SREU with one variable and a constant bound on the number of rigid equations is P-complete.
Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic
Martin Müller, Joachim Niehren
The system FT≤ of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints over feature trees. We investigate decidability and complexity questions for fragments of the first-order theory of FT≤. It is well-known that the first-order theory of FT is decidable and that several of its fragments can be decided in quasi-linear time, including the satisfiability problem of FT and its entailment problem with existential quantification φ⊧∃x1..xnφ'. Much less is known on the first-order theory of FT≤. The satisfiability problem of FT≤ can be decided in cubic time, as well as its entailment problem without existential quantification. Our main result is that the entailment problem of FT≤ with existential quantifiers is decidable but PSPACE-hard. Our decidability proof is based on a new technique where feature constraints are expressed in second-order monadic logic with countably many successors SωS. We thereby reduce the entailment problem of FT≤ with existential quantification to Rabin's famous theorem on tree automata.
Co-definite Set Constraints
Witold Charatonik, Andreas Podelski
In this paper, we introduce the class of co-definite set constraints. This is a natural subclass of set constraints which, when satisfiable, have a greatest solution. It is practically motivated by the set-based analysis of logic programs with the greatest-model semantics. We present an algorithm solving co-definite set constraints and show that their satisfiability problem is DEXPTIME-complete.
Modularity of Termination Using Dependency pairs
Thomas Arts, Jürgen Giesl
The framework of dependency pairs allows automated termination and innermost termination proofs for many TRSs where such proofs were not possible before. In this paper we present a refinement of this framework in order to prove termination in a modular way. Our modularity results significantly increase the class of term rewriting systems where termination resp. innermost termination can be proved automatically. Moreover, the modular approach to dependency pairs yields new modularity criteria which extend previous results in this area. In particular, existing results for modularity of innermost termination can easily be obtained as direct consequences of our new criteria.
Termination of Associative-Commutative Rewriting by Dependency Pairs
Claude Marché, Xavier Urbain
A new criterion for termination of rewriting has been described by Arts and Giesl in 1997. We show how this criterion can be generalized to rewriting modulo associativity and commutativity. We also show how one can build weak AC-compatible reduction orderings which may be used in this criterion.
Termination Transformation by Tree Lifting Ordering
Takahito Aoto, Yoshihito Toyama
An extension of a modular termination result for term rewriting systems (TRSs, for short) by A. Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination transformation by M. C. F. Ferreira and H. Zantema (1995) under the presence of a non-collapsing non-duplicating terminating TRS whose function symbols are all to be eliminated. We propose a tree lifting ordering induced from a reduction order and a set G of function symbols, and use this ordering to transform a TRS R into R'; termination of R' implies that of RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l → r in R (1) the root symbol of r is in G whenever that of l is in G; and (2) no variable appears directly below a symbol from G in l when G contains a constant. Because of conditions (1) and (2), our technique covers only a part of the dummy elimination technique; however, even when S is empty, there are cases that our technique has an advantage over the dummy elimination technique.
Towards Automated Termination Proofs through "Freezing"
Hongwei Xi
We present a transformation technique called freezing to facilitate automatic termination proofs for left-linear term rewriting systems. The significant merits of this technique lie in its simplicity, its amenability to automation and its effectiveness, especially, when combined with other well-known methods such as recursive path orderings and polynomial interpretations. We prove that applying the freezing technique to a left-linear term rewriting system always terminates. We also show that many interesting TRSs in the literature can be handled with the help of freezing while they elude a lot of other approaches aiming for generating termination proofs automatically for term rewriting systems. We have mechanically verified all the left-linear examples presented in this paper.
Higher-Order Rewriting and Partial Evaluation
Olivier Danvy, Kristoffer Høgsbro Rose
We demonstrate the usefulness of higher-order rewriting techniques for specializing programs, i.e., for partial evaluation. More precisely, we demonstrate how casting program specializers as combinatory reduction systems (CRSs) makes it possible to formalize the corresponding program transformations as meta-reductions, i.e., reductions in the internal "substitution calculus." For partial-evaluation problems, this means that instead of having to prove on a case-by-case basis that one's "two-level functions" operate properly, one can concisely formalize them as a combinatory reduction system and obtain as a corollary that static reduction does not go wrong and yields a well-formed residual program.
We have found that the CRS substitution calculus provides an adequate expressive power to formalize partial evaluation: it provides sufficient termination strength while avoiding the need for additional restrictions such as types that would complicate the description unnecessarily (for our purpose).
In addition, partial evaluation provides a number of examples of higher-order rewriting where being higher order is a central (rather than an occasional or merely exotic) property. We illustrate this by demonstrating how standard but non-trivial partial-evaluation examples are handled with higher-order rewriting.
SN Combinators and Partial Combinatory Algebras
Yohji Akama
We introduce an intersection typing system for combinatory logic. We prove the soundness and completeness for the class of partial combinatory algebras. We derive that a term of combinatory logic is typeable iff it is SN. Let F be the class of non-empty filters which consist of types. Then F is an extensional non-total partial combinatory algebra. Furthermore, it is a fully abstract model with respect to the set of sn c terms of combinatory logic. By F, we can solve Bethke-Klop's question; "find a suitable representation of the finally collapsed partial combinatory algebra of P". Here, P is a partial combinatory algebra, and is the set of closed sn terms of combinatory logic modulo the inherent equality. Our solution is the following: the finally collapsed partial combinatory algebra of P is representable in F. To be more precise, it is isomorphically embeddable into F.
Coupling Saturation-Based Provers by Exchanging Positive/Negative Information
Dirk Fuchs
We examine different possibilities of coupling saturationbased theorem provers by exchanging positive/negative information. Positive information is given by facts that should be employed for proving a proof goal, negative information is represented by facts that do not appear to be useful. We introduce a basic model for cooperative theorem proving employing both kinds of information. We present theoretical results regarding the exchange of positive/negative information as well as practical methods that allow for a gain of efficiency in comparison with sequential provers. Finally, we report on experimental studies conducted in the areas unfailing completion and superposition.
An On-line Problem Database
Nachum Dershowitz, Ralf Treinen
The Robbins problem was solved in October 1996 [7] by the equational theorem prover EQP [6]. Although the solution was automatic in the sense that the user of the program did not know a solution, it was not a simple matter of giving the conjecture and pushing a button. The user made many computer runs, observed the output, adjusted the search parameters, and made more computer runs. The goal of this kind of iteration is to achieve a well-behaved search. Several of the searches were successful.
The purpose of this presentation is to convey some of the methods that have led to well-behaved searches in our experiments and to speculate on automating the achievement of well-behaved search. First, I give some background on the Robbins problem and its solution.
1997
Goal-Directed Completion Using SOUR Graphs
Christopher Lynch
We give the first Goal-Directed version of the Knuth Bendix Completion Procedure. Our procedure is based on Basic Completion and SOUR Graphs. There are two phases to the procedure. The first phase, which runs in polynomial time, compiles the equations and the goal into a constrained tree automata representing the completed system, and a set of constraints representing goal solutions. The second phase starts with the goal solutions and works its way back to the original equations, solving constraints along the way.
Shostak's Congruence Closure as Completion
Deepak Kapur
Shostak's congruence closure algorithm is demystified, using the framework of ground completion on (possibly nonterminating, non-reduced) rewrite rules. In particular, the canonical rewriting relation induced by the algorithm on ground terms by a given set of ground equations is precisely constructed. The main idea is to extend the signature of the original input to include new constant symbols for nonconstant subterms appearing in the input. A byproduct of this approach is (i) an algorithm for associating a confluent rewriting system with possibly nonterminating ground rewrite rules, and (ii) a new quadratic algorithm for computing a canonical rewriting system from ground equations.
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
Ulrich Kühler, Claus-Peter Wirth
We propose a specification language for the formalization of data types with partial or non-terminating operations as part of a rewrite-based framework for inductive theorem proving. The language requires constructors for designating data items and admits positive/negative conditional equations as axioms in specifications. The (total algebra) semantics for such specifications is based on so-called data models. We develop admissibility conditions that guarantee the unique existence of a distinguished data model. Since admissibility of a specification requires confluence of the induced rewrite relation, we provide an effectively testable confluence criterion which does not presuppose termination.
Cross-Sections for Finitely Presented Monoids with Decidable Word Problems
Friedrich Otto, Masashi Katsura, Yuji Kobayashi
A finitely presented monoid has a decidable word problem if and only if it has a recursive cross-section if and only if it can be presented by some left-recursive convergent string-rewriting system. However, regular cross-sections or even context-free cross-sections do not suffice. This is shown by presenting examples of finitely presented monoids with decidable word problems that do not admit regular cross-sections, and that, hence, cannot be presented by left-regular convergent stringrewriting systems. Also examples of finitely presented monoids with decidable word problems are presented that do not even admit context-free cross-sections. On the other hand, it is shown that each finitely presented monoid with a decidable word problem has a finite presentation that admits a cross-section which is a Church-Rosser language.
New Undecidablility Results for Finitely Presented Monoids
Andrea Sattler-Klein
For finitely presented monoids the finiteness problem, the free monoid problem, the trivial monoid problem, the group problem and the problem of commutativity are undecidable in general. On the other hand, these problems are all decidable for the class of finite presentations involving complete string rewriting systems. Thus the question arises whether these problems are also decidable for the class of finite presentations describing monoids which have decidable word problems. In this paper we present some results from the author's Doctoral Dissertation [Sa96] which answer this question in the negative and show that each of these problems is undecidable for the class of finitely presented monoids with decidable word problems admitting regular complete presentations as well as for the class of finitely presented monoids with tractable word problems.
On the Property of Preserving Regularity for String-Rewriting Systems
Friedrich Otto
Some undecidability results concerning the property of preserving regularity are presented that strengthen corresponding results of Gilleron and Tison (1995). In particular, it is shown that it is undecidable in general whether a finite, length-reducing, and confluent stringre-writing system yields a regular set of normal forms for each regular language.
Rewrite Systems for Natural, Integral, and Rational Arithmetic
Évelyne Contejean, Claude Marché, Landy Rabehasaina
We give algebraic presentations of the sets of natural numbers, integers, and rational numbers by convergent rewrite systems which moreover allow efficient computations of arithmetical expressions. We then use such systems in the general normalised completion algorithm, in order to compute Gröbner bases of polynomial ideals over Q.
D-Bases for Polynomial Ideals over Commutative Noetherian Rings
Leo Bachmair, Ashish Tiwari
We present a completion-like procedure for constructing D-bases for polynomial ideals over commutative Noetherian rings with. unit. The procedure is described at an abstract level, by transition rules. Its termination is proved under certain assumptions about the strategy that controls the application of the transition rules. Correctness is established by proof simplification techniques.
On the Word Problem for Free Lattices
Georg Struth
We prove completeness of a rewrite-based algorithm for the word problem in the variety of lattices and discuss the method of non-symmetric completion with regard to this variety.
A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems
Deepak Kapur, G. Sivakumar
A new path ordering for showing termination of associative-commutative (AC) rewrite systems is defined. If the precedence relation on function symbols is total, the ordering is total on ground terms, but unlike the ordering proposed by Rubio and Nieuwenhuis, this ordering can orient the distributivity property in the proper direction. The ordering is defined in a natural way using recursive path ordering with status as the underlying basis. This settles a longstanding problem in termination orderings for AC rewrite systems. The ordering can be used to define an ordering on nonground terms.
Proving Innermost Normalisation Automatically
Thomas Arts, Jürgen Giesl
We present a technique to prove innermost normalisation of term rewriting systems (TRSs) automatically. In contrast to previous methods, our technique is able to prove innermost normalisation of TRSs that are not terminating.
Our technique can also be used for termination proofs of all TRSs where innermost normalisation implies termination, such as non-overlapping TRSs or locally confluent overlay systems. In this way, termination of many (also non-simply terminating) TRSs can be verified automatically.
Termination of Context-Sensitive Rewriting
Hans Zantema
Context-sensitive term rewriting is a kind of term rewriting in which reduction is not allowed inside some fixed arguments of some function symbols. We introduce two new techniques for proving termination of context-sensitive rewriting. The first one is a modification of the technique of interpretation in a well-founded order, the second one is implied by a transformation in which context-sensitive termination of the original system can be concluded from termination of the transformed one. In combination with purely automatic techniques for proving ordinary termination, the latter technique is purely automatic too.
A New Parallel Closed Condition for Church-Rossser of Left-Linear Term Rewriting Systems
Michio Oyamaguchi, Yoshikatsu Ohta
G. Huet (1980) showed that a left-linear term-rewriting system (TRS) is Church-Rosser (CR) if P -|→ Q for every critical pair Innocuous Constructor-Sharing Combinations
We investigate conditions under which confluence and/or termination are preserved for constructor-sharing and hierarchical combinations of rewrite systems, one of which is left-linear and convergent.
Scott's Conjecture is True, Position Sensitive Weights
The classification of total reduction orderings for strings over a 2-letter alphabet w.r.t. monoid presentations with 2 generators was published by U. Martin, see [9], and used the hypothetical truth of Scott's conjecture, which was 3 years old in 1996.
A Complete Axiomatisation for the Inclusion of Series-Parallel Partial Orders
Series-parallel orders are defined as the least class of partial orders containing the one-element order and closed by ordinal sum and disjoint union. From this inductive definition, it is almost immediate that any series-parallel order may be represented by an algebraic expression, which is unique up to the associativity of ordinal sum and to the associativivity and commutativity of disjoint union. In this paper, we introduce a rewrite system acting on these algebraic expressions that axiomatises completely the sub-ordering relation for the class of series-parallel orders.
Undecidability of the First Order Theory of One-Step Right Ground Rewriting
The problem of decidability of the first order theory of one-step rewriting was stated in [CCD93]. One can find the problem on the lists of open problems in rewriting in [DJK93] and [DJK95]. In 1995 Ralf Treinen proved that the theory is undecidable. The First-Order Theory of One Step Rewriting in Linear Noetherian Systems is Undecidable
We construct a finite linear finitely terminating rewrite rule system with undecidable theory of one step rewriting.
Solving Linear Diophantine Equations Using the Geometric Structure of the Solution Space
In the development of algorithms for finding the minimal solutions of systems of linear Diophantine equations, little use has been made (to our knowledge) of the results by Stanley using the geometric properties of the solution space. Building upon these results, we present a new algorithm, and we suggest the use of geometric properties of the solution space in finding bounds for searching solutions and in having a qualitative evaluation of the difficulty in solving a given system.
A Criterion for Intractability of E-unification with Free Function Symbols and Its Relevance for Combination Algorithms
All applications of equational unification in the area of term rewriting and theorem proving require algorithms for general E-unification, i.e., E-unification with free function symbols. On this background, the complexity of general E-unification algorithms has been investigated for a large number of equational theories. For most of the relevant cases, the problem of deciding solvability of general E-unification problems was found to be NP-hard. We offer a partial explanation. A criterion is given that characterizes a large class K of equational theories E where general E-unification is always NP-hard. We show that all regular equational theories E that contain a commutative or an associative function symbol belong to K. Other examples of equational theories in K concern non-regular cases as well. Effective Reduction and Conversion Strategies for Combinators
We imagine that we are computing with combinators or lambda terms and that successive terms are related by one-step reduction or expansion. We have a term on our screen and we want to click on a redex to be reduced (or expanded) to obtain the next screenful. The choice of redex is determined by a strategy for achieving our ends. Such a strategy must be effective in the sense of being computable. Memory is a serious constraint, since only one term fits on our screen at a time. Finite Family Developments
Associate to a rewrite system R having rules l → r, its labelled version Rω having rules lm+1° → rm•, for any natural number m ∈ ω. These rules roughly express that a left-hand side l carrying labels all larger than m can be replaced by its right-hand side r carrying labels all smaller than or equal to m. A rewrite system R enjoys finite family developments (FFD) if Rω is terminating. We show that the class of higher order pattern rewrite systems enjoys FFD, extending earlier results for the lambda calculus and first order term rewrite systems.
Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language
The implementation of the general non-deterministic method provides now a convenient and useful ELAN platform to tackle some non-disjoint cases [5] (only one additional non-deterministic step) or to realize other combination algorithms based on the same techniques but in different contexts: satisfiability, the word-problem, matching [6], free amalgamation [1],... Most of them can be viewed as a way to decrease the non-determinism inherent in the general method.
The Invariant Package of MAS
TODO
Opal: A System for Computing Noncommutative Gröbner Bases
TODO
TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems
TODO
Fine-Grained Concurrent Completion
We present a concurrent Completion procedure based on the use of a SOUR graph as data structure. The procedure has the following characteristics. It is asynchronous, there is no need for a global memory or global control, equations are stored in a SOUR graph with maximal structure sharing, and each vertex is a process, representing a term. Therefore, the parallelism is at the term level. Each edge is a communication link, representing a (subterm, ordering, unification or rewrite) relation between terms. Completion is performed on the graph as local graph transformations by cooperation between processes. We show that this concurrent Completion procedure is sound and complete with respect to the sequential one, provided that the information is locally time stamped in order to detect out of date information.
AC-Complete Unification and its Application to Theorem Proving
The inefficiency of AC-completion is mainly due to the doubly exponential number of AC-unifiers and thereby of critical pairs generated. We present AC-complete E-unification, a new technique whose goal is to reduce the number of AC-critical pairs inferred by performing unification in a extension E of AC (e.g. ACU, Abelian groups, Boolean rings, ...) in the process of normalized completion [24, 25]. The idea is to represent complete sets of AC-unifiers by (smaller) sets of E-unifiers. Not only do the theories E used for unification have exponentially fewer most general unifiers than AC, but one can remove from a complete set of E-unifiers those solutions which have no E-instance which is an AC-unifier.
Superposition Theorem Proving for Albelian Groups Represented as Integer Modules
We define a superposition calculus specialized for abelian groups represented as integer modules, and show its refutational completeness. This allows to substantially reduce the number of inferences compared to a standard superposition prover which applies the axioms directly. Specifically, equational literals are simplified, so that only the maximal term of the sums is on the left-hand side. Only certain minimal superpositions need to be considered; other superpositions which a standard prover would consider become redundant. This not only reduces the number of inferences, but also reduces the size of the AC-unification problems which are generated. That is, AC-unification is not necessary at the top of a term, only below some non-AC-symbol. Further, we consider situations where the axioms give rise to variable overlaps and develop techniques to avoid these explosive cases where possible.
Symideal Gröbner Bases
This paper presents a completion technique for a set of polynomials in K[X1,..., Xn] which is closed under addition and under multiplication with symmetric polynomials as well as a solution for the corresponding membership problem. Our algorithmic approach is based on a generalization of a novel rewriting technique for the computation of bases for rings of permutation-invariant polynomials.
Termination of Constructor Systems
We present a method to prove termination of constructor systems automatically. Our approach takes advantage of the special form of these rewrite systems because for constructor systems instead of left- and right-hand sides of rules it is sufficient to compare so-called dependency pairs [Art96]. Unfortunately, standard techniques for the generation of well-founded orderings cannot be directly used for the automation of the dependency pair approach. To solve this problem we have developed a transformation technique which enables the application of known synthesis methods for well-founded orderings to prove that dependency pairs are decreasing. In this way termination of many (also non-simply terminating) constructor systems can be proved fully automatically.
Dummy Elimination in Equational Rewriting
In [5] we introduced the concept of dummy elimination in term rewriting: a transformation on terms which eliminates function symbols simplifying the rewrite rules and making, in general, the task of proving termination easier. Here we consider the more general setting of rewriting modulo an equational theory; we show that, in contrast with most techniques developed for proving termination of rewrite systems, dummy elimination remains valid in the presence of equational theories. Furthermore using the same proof technique, the soundness of a family of transformations (containing dummy elimination) can be shown. This work was motivated by an application in the area of Process Algebra.
On Proving Termination by Innermost Termination
We present a new approach for proving termination of rewrite systems by innermost termination. From the resulting abstract criterion we derive concrete conditions, based on critical peak properties, under which innermost termination implies termination (and confluence). Finally, we show how to apply the main results for providing new sufficient conditions for the modularity of termination.
A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form
This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in η-long β-normal form. This ordering is powerful enough to show termination of several complex examples.
Higher-Order Superposition for Dependent Types
We describe a proof of the Critical Pair Lemma for Plotkin's LF calculus [4]. Our approach basically follows the one used by Nipkow [12] for the simply-typed case, though substantial modifications and some additional theoretical machinery are needed to ensure well-typedness of rewriting in this richer type system. We conclude the paper presenting some significant applications of the theory.
Higher-Order Narrowing with Definitional Trees
Functional logic languages with a sound and complete operational semantics are mainly based on narrowing. Due to the huge search space of simple narrowing, steadily improved narrowing strategies have been developed in the past. Needed narrowing is currently the best narrowing strategy for first-order functional logic programs due to its optimality properties w.r.t. the length of derivations and the number of computed solutions. In this paper, we extend the needed narrowing strategy to higher-order functions and λ-terms as data structures. By the use of definitional trees, our strategy computes only incomparable solutions. Thus, it is the first calculus for higher-order functional logic programming which provides for such an optimality result. Since we allow higher-order logical variables denoting λ-terms, applications go beyond current functional and logic programming languages.
A Compiler for Nondeterministic Term Rewriting Systems
This work presents the design and the implementation of a compiler for the ELAN specification language. The language is based on rewriting logic and permits, in particular, the combination of computations where deterministic evaluations are mixed with a nondeterministic search for solutions. The implementation combines compilation methods of term rewriting systems, functional and logic programming languages, and some new original techniques producing, in summary, an efficient code in an imperative language. The efficiency of the compiler is demonstrated on experimental results.
Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Nomalisation
We generalise the notion of explicit substitution from the λ-calculus to higher order rewriting, realised by combinatory reduction systems (CRSs). For every confluent CRS, R, we construct an explicit substitution variant, Rx, which we prove confluent. Confluence Properties of Extensional and Non-Extensional λ-Calculi with Explicit Substitutions (Extended Abstract)
This paper studies confluence properties of extensional and non-extensional λ-calculi with explicit substitutions, where extensionality is interpreted by η-expansion. For that, we propose a general scheme for explicit substitutions which describes those abstract properties that are sufficient to guarantee confluence. Our general scheme makes it possible to treat at the same time many well-known calculi such as λσ, λσ⇑ and λυ, or some other new calculi that we propose in this paper. We also show for those calculi not fitting in the general scheme that can be translated to another one fining the scheme, such as λs, how to reason about confluence properties of their extensional and non-extensional versions.
On the Power of Simple Diagrams
In this paper we focus on a set of abstract lemmas that are easy to apply and turn out to be quite valuable in order to establish confluence and/or normalization modularly, especially when adding rewriting rules for extensional equalities to various calculi. We show the usefulness of the lemmas by applying them to various systems, ranging from simply typed lambda calculus to higher order lambda calculi, for which we can establish systematically confluence and/or normalization (or decidability of equality) in a simple way. Many result are new, but we also discuss systems for which our technique allows to provide a much simpler proof than what can be found in the literature.
Coherence for Sharing Proof Nets
Sharing graphs are a way of representing linear logic proof-nets in such a way that their reduction never duplicates a redex. In their usual presentations, they present a problem of coherence: if the proof-net N reduces by standard cut-elimination to N', then, by reducing the sharing graph of N we do not obtain the sharing graph of N'. We solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). The rewriting system is confluent and terminating.
Modularity of Termination in Term Graph Rewriting
Term rewriting is generally implemented using graph rewriting for efficiency reasons. Graph rewriting allows sharing of common structures thereby saving both time and space. This implementation is sound in the sense that computation of a normal form of a graph yields a normal form of the corresponding term. In this paper, we study modularity of termination of the graph reduction. Unlike in the case of term rewriting, termination is modular in graph rewriting for a large class of systems. Our results generalize the results of Plump [14] and Kurihara and Ohuchi [10].
Confluence of Terminating Conditional Rewrite Systems Revisited
We present a new and powerful criterion for confluence of terminating (terms in) join conditional term rewriting systems. This criterion is based on a certain joinability property for shared parallel critical peaks and does neither require the systems to be decreasing nor left-linear nor normal, but only terminating.
Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem
This article proposes a compositional semantics for term rewriting systems, i.e. a semantics preserving structuring operations such as the disjoint union. The semantics is based on the categorical construct of a monad, adapting the treatment of universal algebra in category theory to term rewriting systems. The First-Order Theory of One-Step Rewriting is Undecidable
The theory of one-step rewriting for a given rewrite system R and signature Σ is the first-order theory of the following structure: Its universe consists of all Σ-ground terms, and its only predicate is the relation "x rewrites to y in one step by R". The structure contains no function symbols and no equality. We show that there is no algorithm deciding the ∃*∀*-fragment of this theory for an arbitrary rewrite system. The proof uses both non-linear and non-shallow rewrite rules.
An Algorithm for Distributive Unification
The purpose of this paper is to describe a decision algorithm for unifiability of equations w.r.t. the equational theory of two distributive axioms: x*(y+z)=x*y+x*z and (x+y)*z=x*z+y*z. The algorithm is described as a set of non-deterministic transformation rules. The equations given as input are eventually transformed into a conjunction of two further problems: One is an AC1-unification-problem with linear constant restrictions. The other one is a second-order unification problem that can be transformed into a word-unification problem and then can be decided using Makanin's decision algorithm. Since the algorithm terminates, this is a solution for an open problem in the field of unification.
On the Termination Problem for One-Rule Semi-Thue System
We solve the u-termination and the termination problems for the one-rule semi-Thue systems S of the form 0p1q → v, (p,q ∈ N-{0}, v ∈ {0,1}*). We obtain a structure theorem about a monoid that we call the termination-monoid of 5. As a consequence, for every fixed system S of the above form, the termination-problem has a linear time-complexity.
Efficient Second-Order Matching
The standard second-order matching algorithm by Huet may be expansive in matching a flexible-rigid pair. On one hand, many fresh free variables may need to be introduced; on the other hand, attempts are made to match the heading free variable on the flexible side with every "top layer" on the rigid side and every argument of the heading free variable with every subterm covered by the "top layer". We propose a new second-order matching algorithm, which introduces no fresh free variables and just considers some selected "top layers", arguments of the heading free variable and subterms covered by the corresponding "top layers". A first implementation shows that the new algorithm is more efficient both in time and space than the standard one for a great number of matching problems.
Linear Second-Order Unification
We present a new class of second-order unification problems, which we have called linear. We deal with completely general second-order typed unification problems, but we restrict the set of unifiers under consideration: they instantiate free variables by linear terms, i.e. terms where any λ-abstractions bind one and only one occurrence of a bound variable. Linear second-order unification properly extends context unification studied by Comon and Schmidt-Schauß. We describe a sound and complete procedure for this class of unification problems and we prove termination for three different subcases of them. One of these subcases is obtained requiring Comon's condition, another corresponds to Schmidt-Schauß's condition, (both studied previously for the case of context unification, and applied here to a larger class of problems), and the third one is original, namely that free variables occur at most twice.
Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type
We develop a higher-order unification algorithm for a restricted class of simply typed lambda terms with function space and product type constructors. It is based on an inference system manipulating so called higher-order product-patterns which is proven to be sound and complete. Allowing tuple constructors in lambda binders provides elegant notations. We show that our algorithm terminates on each input and produces a most general unifier if one exists. The approach also extends smoothly to a calculus with terminal type.
Decidable Approximations of Term Rewriting Systems
A linear term rewriting system R is growing when, for every rule l→r∈R, each variable which is shared by l and r occurs at depth one in l. We show that the set of ground terms having a normal form w.r.t. a growing rewrite system is recognized by a finite tree automaton. This implies in particular that reachability and sequentiality of growing rewrite systems are decidable. Moreover, the word problem is decidable for related equational theories. We prove that our conditions are actually necessary: relaxing them yields undecidability of reachability. Semantics and Strong Sequentiality of Priority Term Rewriting Systems
This paper gives an operational semantics of priority term rewriting systems (PRS) by using conditional systems, whose reduction is decidable and stable under substitution. We also define the class of strong sequential PRSs and show that this class is decidable. Moreover, we show that the index rewriting of strong sequential PRSs gives a normalizing strategy.
Higher-Order Families
A redex family is a set of redexes which are lsquocreated in the same wayrsquo. Families specify which redexes should be shared in any so-called optimal implementation of a rewriting system. We formalise the notion of family for orthogonal higher-order term rewriting systems (OHRSs). In order to comfort our formalisation of the intuitive concept of family, we actually provide three conceptually different formalisations, via labelling, extraction and zigzag and show them to be equivalent. This generalises the results known from literature and gives a firm theoretical basis for the optimal implementation of OHRSs.
A New Proof Manager and Graphic Interface for Larch Prover
We present PLP, a proof management system and graphic interface for the "Larch Prover" (LP). The system provides additional support for interactive use of LP, by letting the user control the order in which goals are proved. We offer improved ways to investigate, compare and communicate proofs by allowing independent attempts at proving a goal, a better access to the information associated with goals and an additional script mechanism. All the features are accessible through a graphic system that makes the proof structure accessible to the user.
ReDuX 1.5: New Facets of Rewriting
TODO
CiME: Completion Modulo E
TODO
Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover
The Distributed Larch Prover, DLP, is a distributed and parallel version of LP, an interactive prover. DLP helps users find proofs by creating and managing many proof attempts that run in parallel. Parallel attempts may work independently on different subgoals of an inference method, and they may compete by using different inference methods to prove the same goal. DLP runs on a network of workstations.
EPIC: An Equational Language -Abstract Machine Supporting Tools-
TODO
SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories
Automated verification problems often involve Associative-Commutative (AC) operators. But, these operators are hard to handle since they cause combinational explosion. Many provers simply consider AC axioms as additional properties kept in a library, adding a burden to the proof search control. Term rewriting modulo AC is a basic approach to remedy this problem. Based on it, we have developed techniques to treat properly AC operators, that have been integrated in SPIKE, an automatic theorem prover in theories expressed by conditional equations [4]. The system SPIKE-AC obtained, written in Caml Light, have demonstrated that induction proofs become more natural and require less interaction. In contrast with other inductive completion methods [6, 9, 11] needing AC unification to compute critical pairs, our method does not need AC unification which is doubly exponential [10]; only AC matching is required. An other advantage is that our system refutes all false conjectures, under reasonable assumptions on the given theories. Experiments have shown that in presence of AC operators, less input from the user is needed, comparing with related systems such as LP [8], NQTHM [5] and PVS [12].
On Gaining Efficiency in Completion-Based Theorem Proving
Gaining efficiency in completion-based theorem proving requires improvements on three levels: fast inference step execution, careful aggregation into an inference machine, and sophisticated control strategies, all that combined with space saving representation of derived facts. We introduce the new Waldmeister prover which shows an increase in overall system performance of more than one order of magnitude as compared with standard techniques.
Modularity of Completeness Revisited
One of the key results in the field of modularity for Term Rewriting Systems is the modularity of completeness for left-linear TRSs established by Toyama, Klop and Barendregt in [TKB89]. The proof, however, is quite long and involved. In this paper, a new proof of this basic result is given which is both short and easy, employing the powerful technique of lsquopile and deletersquo already used with success in proving the modularity of UN→. Moreover, the same proof is shown to extend the result in [TKB89] proving modularity of termination for left-linear and consistent with respect to reduction TRSs.
Automatic Termination Proofs With Transformation Orderings
Transformation orderings are a powerful tool for proving termination of term rewriting systems. However, it is rather hard to establish their applicability to a given rule system. We introduce an algorithm which automatically generates transformation orderings for many non-trivial systems including Hercules & hydra and sorting algorithms.
A Termination Ordering for Higher Order Rewrite System
We present an extension of the recursive path ordering for the purpose of showing termination of higher order rewrite systems. Keeping close to the general path ordering of Dershowitz and Hoot, we demonstrate sufficient properties of the termination functions for our method to apply. Thereby we describe a class of different orderings. Finally we compare our method to previously published extensions of the recursive path ordering into the higher order setting.
A Complete Characterization of Termination of Op1q → 1rOs
We characterize termination of one-rule string rewriting systems of the form 0p1q → 1r0s for every choice of positive integers p, q, r, and s. For the simply terminating cases, we give the precise complexity of derivation lengths.
On Narrowing, Refutation Proofs and Constraints
We develop a proof technique for dealing with narrowing and refutational theorem proving in a uniform way, clarifying the exact relationship between the existing results in both fields and allowing us to obtain several new results. Refinements of narrowing (basic, LSE, etc.) are instances of the technique, but are also defined here for arbitrary (possibly ordering and/or equality constrained or not yet convergent or saturated) Horn clauses, and shown compatible with simplification and other redundancy notions. By narrowing modulo equational theories like AC, compact representations of solutions, expressed by AC-equality constraints, can be obtained. Computing AC-unifiers is only needed at the end if one wants to "compress" such a constraint into its (doubly exponentially many) concrete substitutions.
Completion for Multiple Reduction Orderings
We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s harr t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.
Towards an Efficient Construction of Test Sets for Deciding Ground Reducability
We propose a method for constructing test sets for deciding whether a term is ground reducible w.r.t. an arbitrary, many-sorted, unconditional term rewriting system. Our approach is based on a suitable characterization of such test sets using a certain notion of transnormality. It generates very small test sets and shows some promise to be an important step towards a practicable implementation.
δo!ε = 1 - Optimizing Optimal λ-Calculus Implementations
In [As94], a correspondence between Lamping-Gonthier's operators for Optimal Reduction of the lambda-calculus [Lam90, GAL92a] and the operations associated with the comonad "!" of Linear Logic was established. In this paper, we put this analogy at work, adding new rewriting rules directly suggested by the categorical equations of the comonad. These rules produce an impressive improvement of the performance of the reduction system, and provide a first step towards the solution of the well known and crucial problem of accumulation of control operators.
Substitution Tree Indexing
Sophisticated maintenance and retrieval of first-order predicate calculus terms is a major key to efficient automated reasoning. We present a new indexing technique, which accelerates the speed of the basic retrieval operations such as finding complementary literals in resolution theorem proving or finding critical pairs during completion. Subsumption and reduction are also supported. Moreover, the new technique not only provides maintenance and efficient retrieval of terms but also of idem-potent substitutions. Substitution trees achieve maximal search speed paired with minimal memory requirements in various experiments and outperform traditional techniques such as path indexing, discrimination tree indexing, and abstraction trees by combining their advantages and adding some new features.
Concurrent Garbage Collection for Concurrent Rewriting
We describe an algorithm that achieves garbage collection when performing concurrent rewriting. We show how this algorithm follows the implementation model of concurrent graph rewriting. This model has been studied and directly implemented on MIMD machines where nodes of the graph are distributed over a set of processors. A distinguishing feature of our algorithm is that it collects garbage concurrently with the rewriting process. Furthermore, our garbage collection algorithm never blocks the process of rewriting; in particular it does not involve synchronisation primitives. In contrast to a classical garbage collection algorithm reclaiming unused blocks of memory, the presented algorithm collects active nodes of the graph (i.e. nodes are viewed as processes). Finally, we present different results of experimentations based on our implementation (RECO) of concurrent rewriting using the concurrent garbage collection algorithm and show that significant speed-ups can be obtained when computing normal forms of terms. Keywords: Concurrent rewriting, Graph rewriting, MIMD architectures, Concurrent garbage collection algorithms.
Lazy Rewriting and Eager Machinery
We define Lazy Term Rewriting Systems and show that they can be realized by local adaptations of an eager implementation of conventional term rewriting systems. The overhead of lazy evaluation is only incurred when lazy evaluation is actually performed. A Rewrite Mechanism for Logic Programs with Negation
Pure logic programs can be interpreted as rewrite programs, executable with a version of the Knuth-Bendix completion procedure called linear completion. The main advantage here is in avoiding many of the loops inherent in the resolution approach: for most productive loops, linear completion yields a finite set of answers and a finite set of rewrite rules (involving just one predicate), from which all the remaining answers can be deduced. And this 'program synthesizing' aspect can be easily combined with other loop avoiding techniques using 'marked' literals and substitutions. It is thus natural to ask how much of the rewrite mechanism carries through for deducing negative information from pure programs, and more generally for any normal logic program. In this paper we show that such an extension can be built in a natural way, with ideas from the Clark completion for normal logic programs, and the domain of constrained rewriting. The correction and completeness of this extended mechanism is proved w.r.t. the 3-valued declarative semantics of Künen for normal programs. We also point out how the semantics of a normal program can in a certain sense be 'parametrized', in terms of the 'meta-reduction' rule set of our approach.
Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides
Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rule because it guarantees the completeness of narrowing for such systems. In this paper we present a syntactic condition ensuring level-confluence for orthogonal, not necessarily terminating, conditional term rewriting systems that have extra variables in the right-hand sides of the rewrite rules. To this end we generalize the parallel moves lemma. Our result bears practical significance since the class of systems that fall within its scope can be viewed as a computational model for functional logic programming languages with local definitions, such as let-expressions and where-constructs.
A Polynomial Algorithm Testing Partial Confluence of Basic Semi-Thue Systems
We give a polynomial algorithm solving the problem "is S partially confluent on the rational set R ?" for finite, basic, noetherian semi-Thue systems. The algorithm is obtained by a polynomial reduction of this problem to the equivalence-problem for deterministic 2-tape finite automata, which has been shown to be polynomially decidable in [Fri-Gre82].
Problems in Rewriting Applied to Categorical Concepts by the Example of a Computational Comonad
We present a canonical system for comonads which can be extended to the notion of a computational comonad [BG92] where the crucial point is to find an appropriate representation. These canonical systems are checked with the help of the Larch Prover [GG91] exploiting a method by G. Huet [Hue90a] to represent typing within an untyped rewriting system. The resulting decision procedures are implemented in the programming language Elf [Pfe89] since typing is directly supported by this language. Finally we outline an incomplete attempt to solve the problem which could be used as a benchmark for rewriting tools.
Relating Two Categorial Models of Term Rewriting
In the last years there has been a growing interest towards categorical models for term rewriting systems (trs's). In our opinion, very interesting are those associating to each trs's a cat-enriched structure: a category whose hom-sets are categories. Interpreting rewriting steps as morphisms in hom-categories, these models provide rewriting systems with a concurrent semantics in a clean algebraic way. In this paper we provide a unified presentation of two models recently proposed in literature by José Meseguer [Mes90, Mes92, MOM93] and John Stell [Ste92, Ste94], respectively, pursuing a critical analysis of both of them. More precisely, we show why they are to a certain extent unsatisfactory in providing a concurrent semantics for rewriting systems. It turns out that the derivation space of Meseguer's Rewriting Logic associated with each term (i.e., the set of coinitial computations) fails in general to form a prime algebraic domain: a condition that is generally considered as expressing a directly implementable model of concurrency for distributed systems (see [Win89]). On the contrary, the resulting derivation space in Stell's model is actually a prime algebraic domain, but too few computations are identified: only disjoint concurrency can be expressed, limiting the degree of parallelism described by the model.
Towards a Domain Theory for Termination Proofs
We present a general framework for termination proofs for Higher-Order Rewrite Systems. The method is tailor-made for having simple proofs showing the termination of enriched λ-calculi.
Infinitary Lambda Calculi and Böhm Models
In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. This results in several new Böhm-like models of the lambda calculus, and new descriptions of existing models.
Proving the Genericity Lemma by Leftmost Reduction is Simple
The Genericity Lemma is one of the most important motivations to take in the untyped lambda calculus the notion of solvability as a formal representation of the informal notion of undefinedness. We generalise solvability towards typed lambda calculi, and we call this generalisation: usability. We then prove the Genericity Lemma for un-usable terms. The technique of the proof is based on leftmost reduction, which strongly simplifies the standard proof.
(Head-) Normalization of Typeable Rewrite Systems
In this paper we study normalization properties of rewrite systems that are typeable using intersection types with ω and with sorts. We prove two normalization properties of typeable systems. On one hand, for all systems that satisfy a variant of the Jouannaud-Okada Recursion Scheme, every term typeable with a type that is not ω is head normalizable. On the other hand, non-Curryfied terms that are typeable with a type that does not contain ω, are normalizable.
Explicit Substitutions with de Bruijn's Levels
TODO
A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics
An algorithm for a restricted form of higher-order matching is described. The intended usage is for rewrite rules that use function-valued variables in place of some unknown term structure. The matching algorithm instantiates these variables with suitable λ-abstractions when given the term to be rewritten. Each argument of one of the variables is expected to match some unique substructure. Multiple solutions are avoided by making fixed choices when alternative ways to match arise. The algorithm was motivated by correctness proofs of designs written in a hardware description language. The feature of the language's semantics that necessitates the higher-order rewriting is described.
Rewrite Systems for Integer Arithmetic
We present three term rewrite systems for integer arithmetic with addition, multiplication, and, in two cases, subtraction. All systems are ground confluent and terminating; termination is proved by semantic labelling and recursive path order. General Solution of Systems of Linear Diophantine Equations and Inequations
Given a system gs of linear diophantine equations and inequations of the form Li #i Mi, i=1,...,n, where #i ∈ {=,<,>,≠,≥,≤} we compute a finite set S of numerical and parametric solutions describing the set of all the solutions of gs (i.e. its general solution). Our representation of the general solution gives direct and simple functions generating the set of all the solutions: this is obtained by giving all the nonnegative natural values to the integer variables of the right hand-side of the parametric solutions, without any linear combination. In particular, unlike the usual representation based on minimal solutions, our representation of the general solution is nonambiguous: given any solution s of gs, it can be deduced from a unique numerical or parametric solution of S.
Combination of Constraint Solving Techniques: An Algebraic POint of View
In a previous paper we have introduced a method that allows one to combine decision procedures for unifiability in disjoint equational theories. Lately, it has turned out that the prerequisite for this method to apply - namely that unification with so-called linear constant restrictions is decidable in the single theories - is equivalent to requiring decidability of the positive fragment of the first order theory of the equational theories. Thus, the combination method can also be seen as a tool for combining decision procedures for positive theories of free algebras defined by equational theories. Complementing this logical point of view, the present paper isolates an abstract algebraic property of free algebras - called combinability - that clarifies why our combination method applies to such algebras. We use this algebraic point of view to introduce a new proof method that depends on abstract notions and results from universal algebra, as opposed to technical manipulations of terms (such as ordered rewriting, abstraction functions, etc.) With this proof method, the previous combination results for unification can easily be extended to the case of constraint solvers that also take relational constraints (such as ordering constraints) into account. Background information from universal algebra about free structures is given to clarify the algebraic meaning of our results.
Some Independent Results for Equational Unification
For finite convergent term-rewriting systems the equational unification problem is shown to be recursively independent of the equational matching problem, the word matching problem, and the (simultaneous) 2nd-order equational matching problem. We also present some new decidability results for simultaneous equational unification and 2nd-order equational matching.
Regular Substitution Sets: A Means of Controlling E-Unification
A method for selecting solution constructors in narrowing is presented. The method is based on a sort discipline that describes regular sets of ground constructor terms as sorts. It is extended to cope with regular sets of ground substitutions, thus allowing different sorts to be computed for terms with different variable bindings. An algorithm for computing signatures of equationally defined functions is given that allows potentially infinite overloading. Applications to formal program development are sketched.
DISCOUNT: A SYstem for Distributed Equational Deduction
TODO
ASTRE: Towards a Fully Automated Program Transformation System
Astre has achieved its initial goal: it is fully automatic for deforestation and two-loops fusion of functional programs. Other fully automatic algorithms for deforestation does not include two-loops fusion. They reject all deforestations that necessitate laws but Astre can perform most of them using additional synthesis. Moreover they do not extend easily to include laws or other strategies. The limitation of Astre is the termination obligation of the input rewrite system. Also Astre does not process easily a large amount of rules. The present prototype has been used so far up-to 500 rules input. At this size, it becomes intractable to perform all the syntheses. We plan to automatize derecursion tactical and automatic insertion of laws [3] in a near future.
Parallel ReDuX → PaReDuX
TODO
STORM: A Many-to-One Associative-Commutative Matcher
TODO
LEMMA: A System for Automated Synthesis of Recursive Programs in Equational Theories
TODO
Generating Polynomial Orderings for Termination Proofs
Most systems for the automation of termination proofs using polynomial orderings are only semi-automatic, i.e. the "right" polynomial ordering has to be given by the user. We show that a variation of Lank-ford's partial derivative technique leads to an easier and slightly more powerful method than most other semi-automatic approaches. Based on this technique we develop a method for the automated synthesis of a suited polynomial ordering.
Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2
TODO
Prototyping Completion with Constraints Using Computational Systems
We use computational systems to express a completion with constraints procedure that gives priority to simplifications. Computational systems are rewrite theories enriched by strategies. The implementation of completion in ELAN, an interpretor of computational systems, is especially convenient for experimenting with different simplification strategies, thanks to the powerful strategy language of ELAN.
Guiding Term Reduction Through a Neural Network: Some Prelimanary Results for the Group Theory
Some experiments have been carried out in order to build Neural Networks which, given a term belonging to an Equational Theory, could suggest which rewrite rules belonging to the Completed TRS for that theory represent the best choice at each reduction step in order to minimize the number of reductions needed to reach the normal form. For the Groups Theory a net was built which had an accuracy of 61%. Moreover the same net in the 71% of the cases could correctly suggest a rule applicable to the term.
Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results
Finite quasigroups in the form of Latin squares have been extensively studied in design theory. Some quasigroups satisfy constraints in the form of equations, called quasigroup identities. In this note, we propose some questions concerning quasigroup identities that can sometimes be answered by the rewriting techniques.
Problems in Rewriting III
We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [36; 37]. We continue with that tradition this year. We give references to solutions to eleven problems from the previous lists, report on progress on several others, provide a few reformulations of old problems, and include ten new problems.
Redundancy Criteria for Constrained Completion
We study the problem of completion in the case of equations with constraints consisting of first-order formulae over equations, disequations, and an irreducibility predicate. We present several inference systems which show in a very precise way how to take advantage of redundancy notions in the context of constrained equational reasoning. A notable feature of these systems is the variety of tradeoffs they present for removing redundant instances of the equations involved in an inference. This combines in one consistent framework almost all practical critical pair criteria, including the notion of Basic Completion. In addition strict improvements of currently known criteria are developed.
Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations
We propose an extension of rewriting techniques to derive inclusion relations a⊆b between terms built from monotonic operators. Instead of using only a rewriting relation →⊆ and rewriting a to b, we use another rewriting relation →⊇ as well and seek a common expression c such that a→⊆*c and b→⊇*c. Each component of the bi-rewriting system (→⊆,→⊇) is allowed to be a subset of the corresponding inclusion ⊆ or ⊇. In order to assure the decidability and completeness of the proof procedure we study the commutativity of →⊆ and →⊇. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. We present the canonical bi-rewriting system corresponding to the theory of non-distributive lattices.
A Case Study of Completion Modulo Distributivity and Abelian Groups
We propose an approach for building equational theories with the objective of improving the performance of the completion procedure, even though there exist canonical rewrite systems for these theories. As a test case of our approach, we show how to build the free Abelian groups and distributivity laws in the completion procedure. The empirical results of our experiment on proving many identities in alternative rings show clearly that the gain of this approach is substantial. More than 30 identities which are valid in any alternative ring are taken from the book "Rings that are nearly associative" by K. A. Zhevlakov et al., and include the Moufang identities and the skew-symmetry of the Kleinfeld function. The proofs of these identities are obtained by Herky, a descendent of RRL and a high-performance rewriting-based theorem prover.
A Semantic Approach to Order-Sorted Rewriting
Order-sorted rewriting builds a nice framework to handle partially defined functions and subtypes (see [Smolka & al 87]). In the previous works about order-sorted rewriting the term rewriting system needs to be sort decreasing in order to be able to prove a critical pair lemma and Birkhoff's completeness theorem. However, this approach is too restrictive. Distributing Equational Theorem Proving
In this paper we show that distributing the theorem proving task to several experts is a promising idea. We describe the team work method which allows the experts to compete for a while and then to cooperate. In the cooperation phase the best results derived in the competition phase are collected and the less important results are forgotten. We describe some useful experts and explain in detail how they work together. We establish fairness criteria and so prove the distributed system to be both complete and correct. We have implemented our system and show by non-trivial examples that drastical time speed-ups are possible for a cooperating team of experts compared to the time needed by the best expert in the team.
On the Correctness of a Distributed Memory Gröbner basis Algorithm
We present an asynchronous MIMD algorithm for Gröbner basis computation. The algorithm is based on the well-known sequential algorithm of Buchberger. Two factors make the correctness of our algorithm nontrivial: the nondeterminism that is inherent with asynchronous parallelism, and the distribution of data structures which leads to inconsistent views of the global state of the system. We demonstrate that by describing the algorithm as a nondeterministic sequential algorithm, and presenting the optimized parallel algorithm through a series of refinements to that algorithm, the algorithm is easier to understand and the correctness proof becomes manageable. The proof does, however, rely on algebraic properties of the polynomials in the computation, and does not follow directly from the proof of Buchberger's algorithm.
Improving Transformation Systems for General E-Unification
In this paper we motivate and present a new and improved transformation system for general E-unification. It can be seen as a modification of the original transformation system by Gallier and Snyder refined by ordinary unification and basic paramodulation. We present a short proof of completeness. Besides completeness we can also show an important property of the transformation system which is not known for the original system: independence of the selection rule. This motivates the abstraction of transformation sequences to equational proof trees thus obtaining static proof objects which facilitates finding further refinements of the procedure.
Equational and Membership Constraints for Finite Trees
We present a new constraint system with equational and membership constraints over infinite trees. It provides for complete and correct satisfiability and entailment tests and is therefore suitable for the use in concurrent constraint programming systems which are based on cyclic data structures. Regular Path Expression in Feature Logic
We examine the existential fragment of a feature logic, which is extended by regular path expressions. A regular path expression is a subterm relation, where the allowed paths for the subterms are restricted by a regular language. We will prove that satisfiability is decidable. This is achieved by setting up a quasi-terminating rewrite system.
Some Lambda Calculi with Categorial Sums and Products
We consider the simply typed λ-calculus with primitive recursion operators and types corresponding to categorical products and coproducts.. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.
Paths, Computations and Labels in the Lambda-Calculus
We provide a new characterization of Lévy's redex-families in the λ-calculus [11] as suitable paths in the initial term of the derivation. The idea is that redexes in a same family are created by "contraction" (via β-reduction) of a unique common path in the initial term. This fact gives new evidence about the "common nature" of redexes in a same family, and about the possibility of sharing their reduction. From this point of view, our characterization underlies all recent works on optimal graph reduction techniques for the λ-calculus [9,6,7,1], providing an original and intuitive understanding of optimal implementations. Confluence and Superdevelopments
In this paper a short proof is presented for confluence of a quite general class of reduction systems, containing λ-calculus and term rewrite systems: the orthogonal combinatory reduction systems. Combinatory reduction systems (CRSs for short) were introduced by Klop generalizing an idea of Aczel. In CRSs, the usual first-order term rewriting format is extended with binding structures for variables. This permits to express besides first order term rewriting also λ-calculus, extensions of λ-calculus and proof normalizations. Confluence will be proved for orthogonal CRSs, that is, for those CRSs having left-linear rules and no critical pairs. The proof proceeds along the lines of the proof of Tait and Martin-Löf for confluence of λ-calculus, but uses a different notion of 'parallel reduction' as employed by Aczel. It gives rise to an extended notion of development, called 'superdevelopment'. A superdevelopment is a reduction sequence in which besides redexes that descend from the initial term also some redexes that are created during reduction may be contracted. For the case of λ-calculus, all superdevelopments are proved to be finite. A link with the confluence proof is provided by proving that superdevelopments characterize exactly the Aczel's notion of 'parallel reduction' used in order to obtain confluence.
Relating Graph and Term Rewriting via Böhm Models
Dealing properly with sharing is important for expressing some of the common compiler optimizations, such as common subexpressions elimination, lifting of free expressions and removal of invariants from a loop, as source-to-source transformations. Graph rewriting is a suitable vehicle to accommodate these concerns. In [4] we have presented a term model for graph rewriting systems (GRSs) without interfering rules, and shown the partial correctness of the aforementioned optimizations. In this paper we define a different model for GRSs, which allows us to prove total correctness of those optimizations. Differently from [4] we will discard sharing from our observations and introduce more restrictions on the rules. We will introduce the notion of Böhm tree for GRSs, and show that in a system without interfering and non-left linear rules (orthogonal GRSs), Böhm tree equivalence defines a congruence. Total correctness then follows in a straightforward way from showing that if a program M contains less sharing than a program N, then both M and N have the same Böhm tree. Topics in Termination
We generalize the various path orderings and the conditions under which they work, and describe an implementation of this general ordering. We look at methods for proving termination of orthogonal systems and give a new solution to a problem of Zantema's.
Total Termination of Term Rewriting
We investigate proving termination of term rewriting systems by interpretation of terms in a compositional way in a total wellfounded order. This kind of termination is called total termination. On one hand it is more restrictive than simple termination, on the other it generalizes most of the usual techniques for proving termination. For total termination it turns out that below ε0 the only orders of interest are built from the natural numbers by lexicographic product and the multiset construction. By examples we show that both constructions are essential. For a wide class of term rewriting systems we prove that total termination is a modular property. Most of our techniques are based on ordinal arithmetic.
Simple Termination is Difficult
A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than its proper subterms. Almost all methods for proving termination yield, when applicable, simple termination. We show that simple termination is an undecidable property, even for one-rule systems. This contradicts a result by Jouannaud and Kirchner. The proof is based on the ingenious construction of Dauchet who showed the undecidability of termination for one-rule systems.
Optimal Normalization in Orthogonal Term Rewriting Systems
We design a normalizing strategy for orthogonal term rewriting systems (OTRSs), which is a generalization of the call-by-need strategy of Huet-Lévy [4]. The redexes contracted in our strategy are essential in the sense that they have "descendants" under any reduction of a given term. There is an essential redex in any term not in normal form. We further show that contraction of the innermost essential redexes gives an optimal reduction to normal form, if it exists. We classify OTRSs depending on possible kinds of redex creation as non-creating, persistent, inside-creating, non-left-absorbing, etc. All these classes are decidable. TRSs in these classes are sequential, but they do not need to be strongly sequential. For non-creating and persistent OTRSs, we show that our optimal strategy is efficient as well.
A Graph Reduction Approach to Incremental Term Rewriting (Preliminary Report)
Our concern is incremental term rewriting: efficient normalization of a sequence of terms that are related to one another by some set of disjoint subterm replacements. Such sequences of similar terms arise frequently in practical applications of term rewriting systems. Previous approaches to this problem [9, 10], have applied only to a limited class of reduction systems and rewriting strategies. In this paper, we present a new algorithm, INCfR, for carrying out incremental term rewriting in an arbitrary left-linear term rewriting system possessing a non-parallel normalizing rewriting strategy fR. This algorithm is based on a novel variant of graph rewriting.
Generating Tables for Bottom-Up Matching
Matching forms a bottle-neck in most implementations of rewrite systems. Bottom-up matching is a very fast form of matching. This paper presents a new approach to bottom-up matching that replaces match-sets by their unifiers. In this way it is possible to define a subsumption ordering on the states. A new algorithm is presented that uses the subsumption graph to compute the bottom-up tables. Its time complexity per table entry is O(rank × wd) where rank is the maximum arity of a function symbol and wd is the maximum number of immediate predecessors in the subsumption graph.
Combination Techniques and Decision Problems for Disunification
Former work on combination techniques was concerned with combining unification algorithms for disjoint equational theories E1,..., En in order to obtain a unification algorithm for the union E1, ∪ ... ∪ En of the theories. Here we show that variants of this method may be applied to disunification as well. Solvability of disunification problems in the free algebra of the combined theory E1 ∪ ... ∪ En is shown to be decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories Ei is decidable. In order to decide ground solvability (i.e., solvability in the initial algebra) of disunification problems in E1 ∪ ... ∪ En we have to consider a new kind of subproblem for the particular theories Ei, namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not Ei -equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, (1) if one theory Ei is the free theory with at least one function symbol and one constant, or (2) if the initial algebras of all theories Ei are infinite. Our results can be used to show that the existential fragment of the theory of the (ground) term algebra modulo associativity of a finite number of function symbols is decidable; the same result follows for function symbols which are associative and commutative, or associative, commutative and idempotent.
The Negation Elimination from Syntactic Equational Formula is Decidable
In this paper we introduce the property of finitely generated sets in an algebra. This property generalizes several notions of rewriting and logical programming; for example unification and disunification are specific cases of this notion. We use this property to formalize the problem of negation elimination in a syntactic equational formulae (i.e first order formulae whose only predicate is syntactic equality) and we prove that this problem is decidable.
Encompassment Properties and Automata with Constraints
We introduce a class of tree automata with constraints which gives an algebraic and algorithmic framework in order to extend the theorem of decidability of inductive reducibility. We use automata with equality constraints in order to solve encompassment constraints and we combine such automata in order to solve every first order formulas built up with unary predicates "x encompasses t" denoted by encompt(x).
Recursively Defined Tree Transductions
we give an equational definition for relations over trees, show that they can be described by rational expressions and give sufficient restrictions on the generated relations to ensure the rationality of their domain and range, and their stability under inverse, composition and substitution. We get in this way "rational tree transductions" extending to the case of trees the well known rational transductions over words.
AC Complement Problems: Satisfiability and Negation Elimination
We show that negation elimination is decidable for linear complement problems interpreted in, where AC is a set of associative and commutative axioms. For this, we present a system of rewrite rules that transforms any linear complement problem into a simple formula, and we give a test for deciding whether a simple formula is satisfiable in or not. This test serves as a basis for the development of a negation elimination algorithm.
A Precedence-Based Total AC-Compatible Ordering
TODO Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols
In this paper, we give a generalization of the associative path ordering. This ordering has been introduced by Bachmair and Plaisted [5] and is a restricted variant of the recursive path ordering which can be used for proving the termination of associative-commutative term rewriting systems. This ordering requires strong conditions on the precedence on the alphabet. In this article, we treat the case of a precedence which contains a chain of AC symbols. We also introduce some unary symbols comparable with AC symbols.
Polynomial Time Termination and Constraint Satisfaction Tests
We show that the termination of ground term-rewriting systems is decidable in polynomial time. This result is extended to ground rational term-rewriting systems. We apply this result to show that the problem of determining whether there exists a simplification ordering over a possibly extended signature, satisfying a set of stict inequalities between terms, is decidable in polynomial time. As a simple consequence, it is decidable in polynomial time whether there exists a simplification ordering which shows that a ground term rewriting system terminates.
Linear Interpretations by Counting Patterns
We introduce a new family of well-founded monotonic orderings on terms, constructed bu counting certain patterns in terms called zig-zags. These extend the familiar Knuth Bendix orderings, providing in general continuum many distinct new orderings with a given choice of Knuth-Bendix weight.
Some Undecidable Termination Problems for Semi-Thue Systems (Abstract)
We show that the uniform termination problem is undecidable for length-preserving semi-Thue systems having 10 rules. We then give an explicit uniformly-terminating semi-Thue system having 9 rules which is "universal with respect to termination problems" in some sense. It follows that there exists a fixed rule (u0,v0) such that T ∪ {(u0, v0)} has 10 rules and undecidable termination problem.
Saturation of First-Order (Constrained) Clauses with the Saturate System
TODO
MERILL: An Equational Reasoning System in Standard ML
TODO
Reduce the Redex → ReDuX
The ReDuX-system is a work-bench for programming and experimenting with term rewriting systems. It is focused towards the implementation of completion procedures with special emphasis on inductive completion. From the programmer's point of view ReDuX provides a large library of data types and algorithms (over 450) which allows for high level programming. The experimentalist also finds a collection of ready-to-run programs (see Table 1, and [WB91]). geDuX has been developed as an extension of the TC- and IC-systems [Kiic82a, B/in87] and has been used as a research tool over the last years. For the last two years it has also been employed as a tutorial system for courses on term rewriting systems at the University of Tiibingen.
AGG - An Implementation of Algebraic Graph Rewriting
TODO
Smaran: A Congruence-Closure Based System for Equational Computations
TODO
LAMBDALG: Higher Order Algebraic Specification Language
TODO
More Problems in Rewriting
Two years ago, in the proceedings of the previous conference, we presented a list of open problems in the theory of rewriting [Dershowitz et al., 1991a]. This time, we report on progress made during the intervening time, and then list some new problems. (A few additional questions on the subject appear in the back of [Diekert, 1990].) We also mention a couple of long-standing open problems which have recently been answered. The last section contains a partisan list of interesting areas for future research. A new, comprehensive survey of the field is [Klop, 1992]. Transfinite Reductions in Orthogonal Term Rewriting Systems (Extended Abstract)
Strongly convergent reduction is the fundamental notion of reduction in infinitary orthogonal term rewriting systems (OTRSs). For these we prove the Transfinite Parallel Moves Lemma and the Compressing Lemma. Strongness is necessary as shown by counterexamples. Normal forms, which we allow to be infinite, are unique, in contrast to ω-normal forms. Strongly converging fair reductions result in normal forms. Redex Capturing in Term Graph Rewriting (Concise Version)
Term graphs are a natural generalization of terms in which structure sharing is allowed. Structure sharing makes term graph rewriting a time- and space-efficient method for implementing term rewrite systems. Certain structure sharing schemes can lead to a situation in which a term graph component is rewritten to another component that contains the original. This phenomenon, called redex capturing, introduces cycles into the term graph which is being rewritten - even when the graph and the rule themselves do not contain cycles. In some applications, redex capturing is undesirable, such as in contexts where garbage collectors require that graphs be acyclic. In other applications, for example in the use of the fixed-point combinator Y, redex capturing acts as a rewriting optimization. We show, using results about infinite rewritings of trees, that term graph rewriting with arbitrary structure sharing (including redex capturing) is sound for left-linear term rewrite systems.
Rewriting, and Equational Unification: the Higher-Order Cases
We give here a general definition of term rewriting in the simply typed lambda-calculus, and use it to define higher-order forms of term rewriting systems, and equational unification and their properties. This provides a basis for generalizing the first- and restricted higher-order results for these concepts. As examples, we generalize Plotkin's criteria for building-in equational theories, and show that pure third-order equational matching is undecidable. This approach simplifies computations in applications involving lexical scoping, and equations. We discuss open problems and summarize future research directions.
Adding Algebraic Rewriting to the Untyped Lambda Calculus (Extended Abstract)
We investigate the system obtained by adding an algebraic rewriting system R to the untyped lambda calculus. On certain classes of terms, called here "stable", we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result yields a general method for proving confluence of typed β reduction plus rewriting; we sketch the application to the polymorphic calculus Fω.
Incremental Termination Proofs and the Length of Derivations
Incremental termination proofs, a concept similar to termination proofs by quasi-commuting orderings, are investigated. In particular, we show how an incremental termination proof for a term rewriting system T can be used to derive upper bounds on the length of derivations in T. A number of examples show that our results can be applied to yield (sharp) low-degree polynomial complexity bounds.
Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding
It is shown that term rewriting systems with primitive recursively bounded derivation heights can be simulated by rewriting systems that have termination proofs using generalized embedding, a very restricted class of simplification orderings. As a corollary we obtain a characterization of the class of relations computable by rewrite systems having primitive recursively bounded derivation heights using recent results on termination proofs by multiset path orderings.
Detecting Redundant Narrowing Derivations by the LSE-SL Reducability Test
Rewriting and narrowing provide a nice theoretical framework for the integration of logic and functional programming. For practical applications however, narrowing is still much too inefficient. In this paper we show how reducibility tests can be used to detect redundant narrowing derivations. We introduce a new narrowing strategy, LSE-SL left-to-right basic normal narrowing, prove its completeness for arbitrary canonical term rewriting systems, and demonstrate how it increases the efficiency of the narrowing process.
Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems
We introduce E-unification, weak E-unification, E-upper bound, E-lower bound, and E-generalization problems, and the corresponding notions of unification, weak unification, upper bound, lower bound, and generalization type of an equational theory. When defining instantiation preorders on solutions of these problems, one can compared substitutions w.r.t. their behaviour on all variables or on finite sets of variables. We shall study the effect which these different instantiation preorders have on the existence of most general or most specific solutions of E-unification, weak E-unification, and E-generalization problems. In addition, we shall elucidate the subtle difference between most general unifiers and coequalizers, and we shall consider generalization in the class of commutative theories.
AC Unification Through Order-Sorted AC1 Unification
We design in this paper a new algorithm to perform unification modulo Associativity and Commutativity. This problem is known to be NP-Complete, and none of the solutions proposed until now is very satisfying because of the huge amount of minimal unifiers of some equations. Unlike many authors, we did not try to speed up computations by optimizing some parts of the algorithm, but we tried to design an extension of the algebra in which unification would be less complex. This goal is achieved by adding axioms expressing the existence of an identity for every AC-operator and working in the AC1 theory. In order to get a conservative extension of the quotient algebra, we work in an order-sorted framework, and thus have to deal with order-sorted unification in a collapsing theory.
Narrowing Directed by a Graph of Terms
Narrowing provides a complete procedure to solve equations modulo confluent and terminating rewriting systems. But it seldom terminates. This paper presents a method to improve the termination. The idea consists in using a finite graph of terms built from the rewriting system and the equation to be solved, which helps one to know the narrowing derivations possibly leading to solutions. Thus, the other derivations are not computed. This method is proved complete. An example is given and some improvements are proposed.
Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification
In this paper we consider the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. This class has been introduced by the authors independently of each other as commutative theories (Baader) and monoidal theories (Nutt). The class encompasses important examples like the theories of abelian monoids, idempotent abelian monoids, and abelian groups. Undecidable Properties of Syntactic Theories
Since we are looking for unification algorithms for a large enough class of equational theories, we are interested in syntactic theories because they have a nice decomposition property which provides a very simple unification procedure. A presentation is said resolvent if any equational theorem can be proved using at most one equality step at the top position. A theory which has a finite and resolvent presentation is called syntactic. In this paper we give decidability results about open problems in syntactic theories: unifiability in syntactic theories is not decidable, resolventness of a presentation and syntacticness of a theory are even not semidecidable. Therefore we claim that the condition of syntacticness is too weak to get unification algorithms directly.
Goal Directed Strategies for Paramodulation
It is well-known that the set of support strategy is incomplete in paramodulation theorem provers if paramodulation into variables is forbidden. In this paper, we present a paramodulation calculus for which the combination of these two restrictions is complete, based on a lazy form of the paramodulation rule which delays parts of the unification step. The refutational completeness of this method is proved by transforming proofs given by other paramodulation strategies into set of support proofs using this new inference rule. Finally, we consider the completeness of various refinements of the method, and conclude by discussing related work and future directions.
Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms
We give new bounds and algorithms for minimal solutions of linear diophantine systems. These bounds are simply exponential, while previous known bounds were, at least until recently, doubly exponential.
Proofs in Parameterized Specification
Theorem proving in parameterized specifications has strong connections with inductive theorem proving. An equational theorem holds in the generic theory of the parameterized specification if and only if it holds in the so-called generic algebra. Provided persistency, for any specification morphism, the translated equality holds in the initial algebra of the instantiated specification. Using a notion of generic ground reducibility, a persistency proof can be reduced to a proof of a protected enrichment. Effective tools for these proofs are studied in this paper.
Completeness of Combinations of Constructor Systems
A term rewriting system is called complete if it is both confluent and strongly normalizing. Barendregt and Klop showed that the disjoint union of complete term rewriting systems does not need to be complete. In other words, completeness is not a modular property of term rewriting systems. Toyama, Klop and Barendregt showed that completeness is a modular property of left-linear TRS's. In this paper we show that it is sufficient to impose the constructor discipline for obtaining the modularity of completeness. This result is a simple consequence of a quite powerful divide and conquer technique for establishing completeness of such constructor systems. Our approach is not limited to systems which are composed of disjoint parts. The importance of our method is that we may decompose a given constructor system into parts which possibly share function symbols and rewrite rules in order to infer completeness. We obtain a similar technique for semi-completeness, i.e. the combination of confluence and weak normalization.
Modular Higher-Order E-Unification
The combination of higher-order and first-order unification algorithms is studied. We present algorithms to compute a complete set of unifiers of two simply typed λ-terms w.r.t. the union of α, β and η conversion and a first-order equational theory E. The algorithms are extensions of Huet's work and assume that a complete unification algorithm for E is given. Our completeness proofs require E to be at least regular.
On Confluence for Weakly Normalizing Systems
We present a general, abstract method to show confluence of weakly normalizing systems. The technique consists in constructing an interpretation of the source system into a target system which is already confluent. If the interpretation satisfies certain simple conditions, then the source system is confluent. The method has been used implicitly in a number of applications, but does not seem to have been presented so far in its generality. We present, as digressions, two other methods for proving confluence.
Program Transformation and Rewriting
We present a basis for program transformation using term rewriting tools. A specification is expressed hierarchically by successive enrichments as a signature and a set of equations. A term can be computed by rewriting. Transformations come from applying a partial unfailing completion procedure to the original set of equations augmented by inductive theorems and a definition of a new function symbol following diverse heuristics. Moreover, the system must provide tools to prove inductive properties; to verify that enrichment produces neither junk nor confusion; and to check for ground confluence and termination. These properties are related to the correctness of the transformation.
An Efficient Representation of Arithmetic for Term Rewriting
We give a locally confluent set of rewrite rules for integer (positive and negative) arithmetic using the familiar system of place notation. We are unable to prove its termination at present, but we strongly conjecture that rewriting with this system terminates and give our reasons. We show that every term has a normal form and so the rewrite system is normalising. Query Optimization Using Rewrite Rules
In literature on query optimization the normal form for relational algebra expressions consisting of Projection, Selection and Join, is well known. In this paper we extend this normal form with Calculation and Union and define a corresponding language UPCSJL. In addition we show how the normal form can be used for query optimization.
Boolean Algebra Admits No Convergent Term Rewriting System
Although there exists a normal form for the theory of Boolean Algebra w.r.t. associativity and commutativity, the so called set of prime implicants, there does not exist a convergent equational term rewriting system for the theory of boolean algebra modulo AC. The result seems well-known, but no formal proof exists as yet. In this paper a formal proof of this fact is given.
Decidability of Confluence and Termination of Monadic Term Rewriting Systems
Term rewriting systems where the right-hand sides of rewrite rules have height at most one are said to be monadic. These systems are a generalization of the well known monadic Thue systems. We show that termination is decidable for right-linear monadic systems but undecidable if the rules are only assumed to be left-linear. Using the Peterson-Stickel algorithm we show that confluence is decidable for right-linear monadic term rewriting systems. It is known that ground confluence is undecidable for both left-linear and right-linear monadic systems. We consider partial results for deciding ground confluence of linear monadic systems.
Bottom-Up Tree Pushdown Automata and Rewrite Systems
Studying connections between term rewrite systems and bottom-up tree pushdown automata (tpda), we complete and generalize results of Gallier, Book and K. Salomaa. We define the notion of tail reduction free rewrite systems (trf rewrite systems). Using the decidability of inductive reducibility (Plaisted), we prove the decidability of the trf property. Monadic rewrite systems of Book, Gallier and K. Salomaa become an obvious particular case of trf rewrite systems. We define also semi-monadic rewrite systems which generalize monadic systems but keep their fair properties. We discuss different notions of bottom-up tree pushdown automata, that can be seen as the algorithmic aspect of classes of problems specified by trf rewrite systems. Especially, we associate a deterministic tpda with any left-linear trf rewrite system.
On Relationship Between Term Rewriting Systems and Regular Tree Languages
The paper presents a new result on the relationship between term rewriting systems (TRSs) and regular tree languages. Important consequences (concerning, in particular, a problem of ground-reducibility) are discussed.
The Equivalence of Boundary and Confluent Graph Grammars on Graph Languages of Bounded Degree
Let B-edNCE and C-edNCE denote the families of graph languages generated by boundary and by confluent edNCE graph grammars, respectively. Boundary means that two nonterminals are never adjacent, and confluent means that rewriting steps are order independent. By definition, boundary graph grammars are confluent, so that B-edNCE ⊆ C-edNCE. Engelfriet et. al. [8] have shown that this inclusion is proper, in general, using certain graph languages of unbounded degree as a witness. We prove that equality holds on graph languages of bounded degree, i.e., B-edNCEdeg=C-edNCEdeg, where the subscript "deg" refers to graph languages of bounded degree. Thus, for bounded degree, boundary graph grammars are the operator normal form of confluent graph grammars and e.g., the characterization results obtained independently for B-edNCE and C-edNCE can be merged. Our result confirms boundary and confluent graph grammars as notions for context-free graph grammars.
Left-to-Right Tree Pattern Matching
We propose a new technique to construct left-to-right matching automata for trees. Our method is based on the novel concept of prefix unifcation which is used to compute a certain closure of the pattern set. From the closure a kind of deterministic matching automaton can be derived immediately. We also point out how to perform the construction incrementally which makes our approach suitable for applications in which pattern sets change dynamically, such as in the Knuth-Bendix completion algorithm. Incremental Techniques for Efficient Normalization of Nonlinear Rewrite Systems
In [8] we described a nonlinear pattern-matching algorithm with the best known worst-case and optimal average-case time complexity. In this paper we first report on some experiments conducted on our algorithm. Based on these experiments we believe that our algorithm is useful in speeding up normalization of nonlinear rewrite systems even when it has a small number (≥5) of rewrite rules. On Fairness of Completion-Based Theorem Proving Strategies
Fairness is an important concept emerged in theorem proving recently, in particular in the area of completion-based theorem proving. Fairness is a required property for the search plan of the given strategy. Intuitively, fairness of a search plan guarantees the generation of a successful derivation if the inference mechanism of the strategy indicates that there is one. Thus, the completeness of the inference rules and the fairness of the search plan form the completeness of a theorem proving strategy. A search plan which exhausts the entire search space is obviously fair, albeit grossly inefficient. Therefore, the problem is to reconciliate fairness and efficiency. This problem becomes even more intricate in the presence of contraction inference rules - rules that remove data from the data set. Proving Equational and Inductive Theorems by Completion and Embedding Techniques
The Knuth-Bendix completion procedure can be used to transform an equational system into a convergent rewrite system. This allows to prove equational and inductive theorems. The main draw back of this technique is that in many cases the completion diverges and so produces an infinite rewrite system. We discuss a method to embed the given specification into a bigger one such that the extended specification allows a finite "parameterized" description of an infinite rewrite system of the base specification. The main emphasis is in proving the correctness of the approach. Examples show that in many cases the Knuth-Bendix completion in the extended specification stops with a finite rewrite system though it diverges in the base specification. This indeed allows to prove equational and inductive theorems in the base specification.
Divergence Phenomena during Completion
We will show how any primitive recursive function may be encoded in a finite canonical string rewriting system. Using these encodings for every primitive recursive function f (and even for every recursively enumerable set C) a finite string rewriting system R and a noetherian ordering > may be constructed such that completion of R with respect to > will generate a divergence sequence that encodes explicitly the input/output behaviour of f (or the set C, respectively). Furthermore, we will show by an example that if completion of a set R with respect to a noetherian ordering > diverges, then there need not exist any rule that causes infinitely many other ones by overlapping.
Simulation Buchberger's Algorithm by Knuth-Bendix Completion
We present a canonical term rewriting system whose initial model is isomorphic to GF(q)[x1,...,xn]. Using this set of rewrite rules and additional ground equations specifying an ideal we can simulate Buchberger's algorithm for polynomials over finite fields using Knuth-Bendix term completion modulo AC. In order to simplify our proofs we exhibit a critical pair criterion which transforms critical pairs into simpler ones.
On Proving Properties of Completion Strategies
We develop methods for proving the fairness and correctness properties of rule based completion strategies by means of process logic. The concepts of these properties are formulated generally within process logic and then concretized to rewrite system theory based on transition rules. We develop in parallel the notions of success and failure of a completion strategy, necessary to support the proves of the cited properties. Finally we show the necessity of another property, called justice, in the analysis of completion strategies.
On Ground AC-Completion
We prove that a canonical set of rules for an equational theory defined by a finite set of ground axioms plus the associativity and commutativity of any number of operators must be finite. Any Gound Associative-Commutative Theory Has a Finite Canonical System
We show that theories presented by a set of ground equations with several associative-commutative (AC) symbols always admit a finite canonical system. This result is obtained through the construction of a reduction ordering which is AC-compatible and total on the set of congruence classes generated by the associativity and commutativity axioms. As far as we know, this is the first ordering with such properties, when several AC function symbols and free function symbols are allowed. Such an ordering is also a fundamental tool for deriving complete theorem proving strategies with built-in associative commutative unification.
A Narrowing-Based Theorem Prover
This work presents a theorem prover for inductive proofs within an equational theory which supports the verification of universally quantified equations. This system, called TIP, is based on a modification of the well-known narrowing algorithm. Particulars of the implementation are stated and practical experiences are summarized.
ANIGRAF: An Interactive System for the Animation of Graph Rewriting Systems with Priorities
TODO
EMMY: A Refutational Theorem Prover for First-Order Logic with Equation
Emmy is an implementation in Quintus Prolog of a refutational theorem prover for first-order logic with equations based on a superposition calculus. This paper describes the structure and the functionalities of this theorem prover.
The Tecton Proof System
TODO
Open Problems in Rewriting
TODO
Characterization of Unification Type Zero
In the literature several methods have hitherto been used to show that an equational theory has unification type zero. These methods depend on conditions which are candidates for alternative characterizations of unification type zero. In this paper we consider the logical connection between these conditions on the abstract level of partially ordered sets. Not all of them are really equivalent to type zero. Proof Normalization for Resolution and Paramodulation
We prove the refutation completeness of restricted versions of resolution and paramodulation for first-order predicate logic with equality. Furthermore, we show that these inference rules can be combined with various deletion and simplification rules, such as rewriting, without compromising refutation completeness. The techniques employed in the completeness proofs are based on proof normalization and proof orderings.
Complete Sets of Reductions Modulo Associativity, Commutativity and Identity
We describe the theory and implementation of a process which finds complete sets of reductions modulo equational theories which contain one or more associative and commutative operators with identity (ACI theories). We emphasize those features which distinguish this process from the similar one which works modulo associativity and commutativity. A primary difference is that for some rules in ACI complete sets, restrictions are required on the substitutions allowed when the rules are applied. Without these restrictions, termination cannot be guaranteed. We exhibit six examples of ACI complete sets that were generated by an implementation.
Completion-Time Optimization of Rewrite-Time Goal Solving
Completion can be seen as a process that transforms proofs in an initially given equational theory to rewrite proofs in final rewrite rules. Rewrite proofs are the normal forms of proofs under these proof transformations. The purpose of this paper is to provide a framework in which one may further restrict the normal forms of proofs which completion is required to construct, thereby further decreasing the complexity of reduction and goal solving in completed systems.
Computing Ground Reducability and Inductively Complete Positions
We provide the extended ground-reducibility test which is essential for induction with term-rewriting systems based on [Küc89]: Given a term, determine at which sets of positions it is ground-reducible by which subsets of rules. The core of our method is a new parallel cover algorithm based on recursive decomposition. From this we obtain a separation algorithm which determines constructors and defined function symbols in a term-algebra presented by a rewrite system. We then reduce our main problem of extended ground-reducibility to separation and cover. Furthermore, using the knowledge of algebra separation, we refine the bounds of [JK86] for the size of ground reduction test-sets. Both our cover algorithm and our extended ground-reducibility test are engineered to be adaptive to actual problem structure, i.e., to allow for lower than the worst case bounds for test-sets on well conditioned problems, including well conditioned subproblems of difficult cases.
Inductive Proofs by Specification Transformation
We show how to transform equational specifications with relations between constructors (or without constructors) into order-sorted equational specifications where every function symbol is either a free constructor or a completely defined function. Narrowing and Unification in Functional Programming - An Evaluation Mechanism for Absolute Set Abstraction
The expressive power of logic programming may be achieved within a functional programming framework by extending the functional language with the ability to evaluate absolute set abstractions. By absolute set abstraction, logical variables are introduced into functional languages as first class objects. Their set-valued interpretations are implicitly defined by the constraining equations. Narrowing and unification can be used to solve these constraining equations to produce the satisfying instantiations of the logic variables. In this paper, we study an execution mechanism for evaluating absolute set abstraction in a first order (non-strict) functional programming setting. First, we investigate the semantics of absolute set abstraction. It is shown that absolute set abstraction is no more than a setvalued expression involving the evaluation of function inversion. Functional equality is defined coinciding with the semantics of the continuous and strict equality function in functional programming. This new equality means that the well known techniques for equation solving can be adopted as a proper mechanism for solving the constraining equations which are the key to the evaluation of absolute set abstraction. The main result of this paper lies in the study of a particular narrowing strategy, called lazy pattern driven narrowing, which is proved to be complete and optimal for evaluating absolute set abstraction in the sense that a complete set of minimal solutions of the constraining equations can be generated by a semantic unification procedure based on this narrowing strategy. This indicates that a mechanism for equation solving can be developed within a functional programming context, producing a more expressive language.
Simulation of Turning Machines by a Left-Linear Rewrite Rule
We prove in this paper that for every Turing machine there exists a left-linear, variable preserving and non-overlapping rewrite rule that simulates its behaviour. The main corollary is the undecidability of the termination for such a rule. If we suppose that the left-hand side can be unified with an only subterm of the right-hand side, then termination is decidable.
Higher-order Unification with Dependent Function Types
Roughly fifteen years ago, Huet developed a complete semidecision algorithm for unification in the simply typed λ-calculus (λ→). In spite of the undecidability of this problem, his algorithm is quite usable in practice. Since then, many important applications have come about in such areas as theorem proving, type inference, program transformation, and machine learning. An Overview of LP, The Larch Power
TODO
Graph Grammars, A New Paradigma for Implementing Visual Languages
This paper is a report on an ongoing work which started in 1981 and is aiming at a general method which would help to considerably reduce the time necessary to develop a syntax-directed editor for any given diagram technique. The main idea behind the approach is to represent diagrams by (formal) graphs whose nodes are enriched with attributes. Then, any manipulation of a diagram (typically the insertion of an arrow, a box, text, coloring, etc.) can be expressed in terms of the manipulation of its underlying attributed representation graph. The formal description of the manipulation is done by programmed attributed graph grammars.
Termination Proofs and the Length of Derivations (Preliminary Version)
The derivation height of a term t, relative to a set R of rewrite rules, dhR(t), is the length of a longest derivation from t. We investigate in which way certain termination proof methods impose bounds on dhR. In particular we show that, if termination of R can be proved by polynomial interpretation then dhRis bounded from above by a doubly exponential function, whereas termination proofs by Knuth-Bendix ordering are possible even for systems where dhRcannot be bounded by any primitive recursive functions. For both methods, conditions are given which guarantee a singly exponential upper bound on dhR. Moreover, all upper bounds are tight.
Abstract Rewriting with Concrete Operations
TODO
On How To Move Mountains 'Associatively and Commutatively'
In this paper we give another characterization of a set of rules which defines a Church-Rosser reduction on the term algebra specified by some associative and commutative equations. This characterization requires fewer conditions to be satisfied than those previously given in the literature do. As a result, when the required conditions are satisfied, the word problem in the term algebra defined by the set of rules and the set of associative and commutative equations can be solved by successive applications of rewriting to the elements in question. Generalized Gröbner Bases: Theory and Applications. A Condensation
Zacharias and Trinks proved that it can be constructively determined whether a finite generating set is a generalized Gröbner basis provided ideals are detachable and syzygies are solvable in the coefficient ring. We develop an abstract rewriting characterization of generalized Gröbner bases and use it to give new proofs of the Spear-Zacharias and Trinks theorems for testing and constructing generalized Gröbner bases. In addition, we use the abstract rewriting characterization to generalize Ayoub's binary approach for testing and constructing Gröbner bases over polynomial rings with Euclidean coefficient rings to arbitrary principal ideal coefficient domains. This also shows that Spear-Zacharias' and Trinks' approach specializes to Ayoub's approach, which was not known before.
A Local Termination Property for Term Rewriting Systems
We describe a desirable property, local termination, of rewrite systems which provide an operational semantics for formal functional programming (FFP) languages, and we give a multiset ordering which can be used to show that the property holds.
An Equational Logic Sampler
TODO
Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms
In this paper we prove that the property of having unique normal forms is preserved under disjoint union. We show that two related properties do not exhibit this kind of modularity.
Priority Rewriting: Semantics, Confluence, and Conditional
Priority rewrite systems (PRS) are partially ordered finite sets of rewrite rules; in this paper, two possible alternative definitions for rewriting with PRS are examined. A logical semantics for priority rewriting is described, using equational formulas obtained from the rules, and inequations which must be assumed to permit rewriting with rules of lower priority. Towards the goal of using PRS to define data type and function specifications, restrictions are given that ensure confluence and encourage modularity. Finally, the relation between priority and conditional rewriting is studied, and a natural combination of these mechanisms is proposed.
Negation with Logical Variables in Conditional Rewriting
We give a general formalism for conditional rewriting, with systems containing conditional rules whose antecedents contain literals to be shown satisfiable and/or unsatisfiable. We explore semantic issues, addressing when the associated operational rewriting mechanism is sound and complete. We then give restrictions on the formalism which enable us to construct useful and meaningful specifications using the proposed operational mechanism.
Algebraic Semantics and Complexity of Term Rewriting Systems
The present paper studies the semantics of linear and non-overlapping TRSs. To treat possibly non-terminating reduction, the limit of such a reduction is formalized using Scott's order-theoretic approach. An interpretation of the function symbols of a TRS as a continuous algebra, namely, continuous functions on a cpo, is given, and universality properties of this interpretation are discussed. Also a measure for computational complexity of possibly non-terminating reduction is proposed. The space of complexity forms a cpo and function symbols can be interpreted as monotone functions on it.
Optimization by Non-Deterministic, Lazy Rewriting
Given a set S and a condition C we address the problem of determining which members of S satisfy C. One useful approach is to set up the generation of S as a tree, where each node represents a subset of S. If from the information available at a node, we can determine that no members of the subset it represents satisfy C, then the subtree rooted at it can be pruned, i.e. its generation suppressed. Thus, large subsets of S can be quickly eliminated from consideration. We show how such a tree can be simulated by interpretation of non-deterministic rewrite rules, and its pruning simulated by lazy evaluation.
Combining Matching Algorithms: The Rectangular Case
The problem of combining matching algorithms for equational theories with disjoint signatures is studied. It is shown that the combined matching problem is in general undecidable but that it becomes decidable if all theories are regular. For the case of regular theories an efficient combination algorithm is developed. As part of that development we present a simple algorithm for solving the word problem in the combination of arbitrary equational theories with disjoint signatures.
Restrictions of Congruence Generated by Finite Canonical String-Rewriting Systems
Let Σ1 be a subalphabet of Σ2, and let R1 and R2 be finite string-rewriting systems on Σ1 and Σ2, respectively. If the congruence ↔*R1 generated by R1 and the congruence ↔*R2 generated by R2 coincide on Σ1*, then R1 can be seen as representing the restriction of the system R2 to the subalphabet Σ1. Is this property decidable ? This question is investigated for several classes of finite canonical string-rewriting systems.
Embedding with Patterns and Associated Recursive Path Ordering
TODO
Rewriting Techniques for Program Synthesis
We present here a completion-like procedure for program synthesis from specifications. A specification is expressed as a set of equations and the program is a Noetherian set of rewrite rules that is efficient for computation. We show that the optimizations applicable for proving inductive theorems are useful for program synthesis. This improves on the use of general completion procedure for program synthesis, reported by Dershowitz, in that it generates fewer rules and terminates more often. However, there is a qualitative difference between this procedure and completion, as superposition is used not for eliminating critical overlaps but to find a complete set of cases for an inductive theorem.
Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient parallel Execution
Strongly sequential systems, developed by Huet and Levy [2], has formed the basis of equational programming languages. Experience with such languages so far suggests that even complex equational programs are based only on strongly sequential systems with constructors. However, these programs are not readily amenable for efficient parallel execution. This paper introduces a class of strongly sequential systems called path sequential systems. Equational programs based on path sequential systems are more natural for parallel evaluation. An algorithm for transforming any strongly sequential system with constructors into an equivalent path sequential system is described.
We give a fast method for generating reduced sets of rewrite rules equivalent to a given set of ground equations. Since, as we show, reduced ground rewrite systems are in fact canonical, this is essentially an efficient Knuth-Bendix procedure for the ground case. The method runs in O(n log n), where n is the number of occurrences of symbols in E. We also show how our method provides a precise characterization of the (finite) collection of all reduced sets of rewrite rules equivalent to a given ground set of equations E, and prove that our algorithm is complete in that it can enumerate every member of this collection. Finally, we show how to modify the method so that it takes as input E and a total precedence ordering on the symbols in E, and returns a reduced rewrite system contained in the lexicographic path ordering generated by the precedence.
Extensions and Comparison of Simplification Orderings
The effective calculation with term rewriting systems presumes termination. Orderings on terms are able to guarantee termination. This report deals with some of those term orderings: Several path and decomposition orderings and the Knuth-Bendix ordering. We pursue three aims:
Classes of Equational Programs that Compile into Efficient Machine Code
Huet and Lévy [HL79] showed that, if an equational program E is strongly sequential, there exists an automaton that, given a term in the language L(E), finds a redex in that term. Fair Termination is Decidable for Ground Systems
By summing up, we have reduced the problem of fair termination to the emptiness of the intersection of two constructible and recognizable forests. Since the family of recognizable forests is closed under intersection and since emptiness is decidable in this family, fair termination is decidable.
Termination for the Direct Sum of left-Linear Term Rewriting Systems -Preliminary Draft-
The direct sum of two term rewriting systems is the union of systems having disjoint sets of function symbols. It is shown that two term rewriting systems both are left-linear and complete if and only if the direct sum of these systems is so.
Conditional Rewrite Rule Systems with Built-In Arithmetic and Induction
Conditional rewriting systems, conditions being the formulae of decidable theories, are investigated. A practical search space-free decision procedure for the related class of unquantified logical theories is described. The procedure is based on cooperating conditional reductions, case splittings and decision algorithms, and is able to perform certain forms of inductive inferences. Completeness and termination of the procedure are proved.
Consider Only General Superpositions in Completion Procedures
Superposition or critical pair computation is one of the key operations in the Knuth-Bendix completion procedure and its extensions. We propose a practical technique which can save computation of some critical pairs where the most general unifiers used to generate these critical pairs are less general than the most general unifiers used to generate other joinable critical pairs. Consequently, there is no need to superpose identical subterms at different positions in a rule more than once and there is also no need to superpose symmetric subterms in a rule more than once. The combination of this technique with other critical pair criteria proposed in the literature is also discussed. The technique has been integrated in the completion procedures for ordinary term rewriting systems as well as term rewriting systems with associative-commutative operators implemented in RRL, Rewrite Rule Laboratory. Performance of the completion procedures with and without this technique is compared on a number of examples.
Solving Systems of Linear Diophantine Equations and Word Equations
TODO
SbReve2: A Term Rewriting Laboratory with (AC-) Unfailing Completion
TODO
THEOPOGLES - An efficient Theorem Prover based on Rewrite-Techniques
TODO
COMTES - An Experimental Environment for the Completion of Term Rewriting Systems
TODO
ASSPEGIQUE: An Integrated Specification Environment
TODO
KBlab: An Equational Theorem Prover for the Macintosh
TODO
Fast Knuth-Bendix Completion: Summary
TODO
Compilation of Ground Term Rewriting Systems and Applications (DEMO)
We get an algorithm (based on tree automata technics) which "compiles" ground term rewriting systems to solve reachability problem in linear time relatively to the terms. The name of the software is VALERIAAN: V=Verification, A= Algebraic, L=Logic, E=Equation, R=Rewrite, I=Inference, A = (tree) Automata, N=Normal (form). VALERIAN is a comics character who travels across time and space.
An Overview of Rewrite Rule Laboratory (RRL)
TODO
InvX: An Automatic Function Inverter
We have implemented InvX, a system that will mechanically generate inverses for a substantial class of functions. By applying an extended set of function-level axioms at compile-time, expressions for the inverses are transformed so that no unification is required at run-time in many cases. This makes the cost of their execution comparable with that of reduction-based semantics. We have also described the incorporation of InvX in the FLAGSHIP programming environment. InvX has been used successfully on a wide range of examples.
A Parallel Implementation of Rewriting and Narrowing
A parallel implementation of rewriting and narrowing is described. This implementation is written in Flat Concurrent Prolog, but the ideas involved are applicable to any system where processes are capable of creating other processes and communicating with each other. Using FCP enables one to write very short programs, virtually no longer than the verbal description of the algorithms. Running programs under the FCP interpreter and using facilities provided by it, one can compare the efficiencies of various strategies. Theoretical results about the efficiency of strategies in certain cases are also mentioned.
Morphocompletion for One-Relation Monoids
TODO
Optimizing Equational Programs
Equational programming [HO82b] involves replacing subterms in a term according to a set of equations or rewrite rules. Each time an equation is applied to the term, the subterm that matches the left hand side of the equation is replaced by the corresponding right hand side. In that process several nodes of the term tree are created. Some of these nodes may later turn out to be useless, and will be reclaimed. A Compiler for Conditional Term Rewriting Systems
In this paper, we present a compiler for conditional term rewriting systems. With respect to traditional interpreters, the gain in execution time that we obtain is of several orders of magnitude. We discuss several optimizations, among which a method to share code in the premises of the conditional rules, well-adapted to algebraic specifications.
How to Choose Weights in the Knuth Bendix Ordering
Knuth and Bendix proposed a very versatile technique for ordering terms, based upon assigning weights to operators and then to terms by adding up the weights of the operators they contain. Our purpose in this paper is twofold. First we give some examples to indicate the flexibility of the method. Then we give a simple and practical algorithm, based on the simplex algorithm, for determining whether or not a set of rules can be ordered by a Knuth Bendix ordering.
Detecting Looping Simplifications
A generalization of tree matching and unification algorithms is presented. Given the equation s=t, this algorithm can often quickly determine that the rewrite rule s→t leads to an infinite sequence of "simplifications". The rule t→s can be tested in the same way. Rules leading to infinite simplifications should not be included in a rewrite system. In general, the problem of deciding whether a set of rewrite rules leads to infinite simplifications is undecidable. The algorithm that is used for this problem is a cross between a unification algorithm for terms with overlapping variables and a matching algorithm. In the simplest case it attempts to find a, σM and σU such that σMσUs = σUt/a. In other words, is there a substitution σ U such that in the rule σUs → σUt the left side matches a subpart of the right side. The same basic algorithm can be used to test more complex cases of looping involving the interaction of several rules, but it is limited to those cases where each application of a rule occurs inside of the previous rule application. Experiments suggest that the simplest form of the algorithm is about 80 percent effective in eliminating bad orientations of rules. The algorithm never rules out a good orientation of a rule, and so it is most useful when one wants to consider all possible rule orientations.
Combinatorial Hypermap Rewriting
Combinatorial hypermaps may be viewed as topological representations of hypergraphs. In this paper, we introduce a hypermap rewriting model, based on a purely combinatorial formulation of the rewriting mechanism. We illustrate this definition by providing a hypermap grammar which generates the set of all connected planar maps. We also investigate a special kind of hypermap grammars, the H-grammars, for which we give a Pumping Theorem enlightening the combinatorial structure of the generated hypermap languages.
Th Word Problem for Finitely Presented Monoids and Finite Canonical Rewriting Systems
The main purpose of this paper is to describe a negative answer to the following question: Term Rewriting Systems with Priorities
Term rewriting systems with rules of different priority are introduced. The semantics are explained in detail and several examples are discussed.
A Gap Between Linear and Non Linear Term-Rewriting Systems (1)
We prove that every recursively enumerable set of terms is generated by a non linear t.r.s in 2 passes. Conversely, every set of terms which is generated by a linear t.r.s in a finite number of passes is recognizable.
Code Generator Generation Based on Template-Driven Target Term Rewriting
A major problem in deriving a compiler from a formal definition is the production of efficient object code. In this context, we propose a solution to the problem of code generator generation. Recent works on public key encryption for secure network communication [7] have brought back the following problem : given a regular set R on A*, defined by a non deterministic finite automaton with n states and a rewriting system T, how can we construct an automaton that recognizes the set of descendants of R : Δ*(R) when this language is regular [1]. Some algorithms are found by Book and Otto [6] or Sakarovitch and me [3],in very particular cases of systems and gave complexity in O(n4) in [6] and O(n3) in [3]. Here we give a strong extension of these algorithms in a large class of systems however the complexity of our algorithm does not depend on the lenght of the words of T and is at most in O(n6).
Groups Presented by Certain Classes of Finite Length-Reducing String-Rewriting Systems
TODO
Some Results about Confluence on a Given Congruence Class
It is undecidable in general whether or not a term-rewriting system is confluent on a given congruence class. This result is shown to hold even when the term-rewriting systems under consideration contain unary function symbols only, and all their rules are length-reducing. On the other hand, for certain subclasses of these systems confluence on a given congruence class is decidable.
Ground Confluence
TODO
Structured Contextual Rewriting
In this paper, we develop a mechanism, which we call structured contextual system, (SCS for short,) to deal with some non-finitely-based algebraic specifications. The sufficient condition for confluence and termination of this kind of systems is also considered, based on a generalization of the approach by O'Donell.
Schematization of Infinite Sets of Rewrite Rules. Application to the Divergence of Completion Processes
This study was originally motivated by the divergence problem of the completion procedure for term rewriting systems [17,18,11]. The practical interest of a completion procedure is limited by the fact that it can generate infinite sets of rewrite rules. Moreover the uniqueness of the result of the completion procedure, given a fixed ordering for orienting equations, implies that it cannot be expected to find another completion strategy for which the completion terminates. [...] Completion for Rewriting Modulo a Congruence
We present completion methods for rewriting modulo a congruence, generalizing previous methods by Peterson and Stickel (1981) and Jouannaud and Kirchner (1986). We formalize our methods as equational inference systems and describe techniques for reasoning about such systems.
On Equational Theories, Unification and Decidability
The following classes of equational theories, which are important in unification theory, are presented: permutative, finite, Noetherian, simple, almost collapse free, collapse free, regular, and Ω-free theories. The relationships between the particular theories are shown and the connection between these classes and the unification hierarchy is pointed out. We give an equational theory that always has a minimal set of unifiers for single equations, but there exists a system of two equations which has no minimal set of unifiers. This example suggests that the definition of the unification type of an equational theory has to be changed. Furthermore we study the conditions, under which minimal sets of unifiers always exist. A General Complete E-Unification Procedure
In this paper, a general unification procedure that enumerates a complete set of E-unifiers of two terms for any arbitrary set E of equations is presented. It is more efficient than the brute force approach using paramodulation, because many redundant E-unifiers arising by rewriting at or below variable occurrences are pruned out by our procedure, still retaining a complete set. This procedure can be viewed as a nondeterministic implementation of a generalization of the Maxtelli-Montanari method of transformations on systems of terms [13], which has its roots in Herbrand's thesis [7]. Remarkably, only two new transformations need to be added to the transformations used for standard unification. This approach differs from previous work based on transformations because, rather than sticking rather closely to the Martelli-Montanari approach using multi-equations [13] as in Kirchner [10,11], we introduce transformations dealing directly with rewrite rules. Improving Basic Narrowing Techniques
In this paper, we propose a new and complete method based on narrowing for solving equations in equational theories. It is a combination of basic narrowing and narrowing with eager reduction, which is not obvious, because their naive combination is not a complete method. We show that it is more efficient than the existing methods in many cases, and for that establish commutation properties on the narrowing. It provides an algorithm that has been implemented as an extension of the REVE software.
Strategy-Controlled Reduction and Narrowing
The inference rules "reduction" and "narrowing" are generalized from terms resp equations to arbitrary atomic formulas. Both rules are parameterized by strategies to control the selection of redices. Church-Rosser properties of the underlying Horn clause specification are shown to ensure both completeness and strategy independence of reduction. "Uniformity" turns out as the crucial property of those reduction strategies which serve as complete narrowing strategies. A characterization of uniformity (and hence completeness) of leftmost-outermost narrowing is presented.
Algorithmic Complexity of Term Rewriting Systems
For the class of the regular term rewriting systems, we have provided ways of obtaining asymptotic evaluations of the cost series. The user does not need to actually manipulate formal series, since our results are given under the form of ready-to-use formulae. These results solely depend on physical characteristics of the system, easily obtainable : number of variables and of constructors in the lefthand sides, occurrences of derived operators in the right-hand sides. Then, the average cost is constant, polynomial or exponential, according to the position of the singularity of the expressions Qi(N(z)) closest to the origin.
Optimal Speedups for Parallel Pattern Matching in Trees
Tree pattern matching is a fundamental operation that is used in a number of programming tasks such as code optimization in compilers, symbolic computation, automatic theorem proving and term rewriting. An important special case of this operation is linear tree pattern matching in which an instance of any variable in the pattern occurs at most once. If n and m are the number of nodes in the subject and pattern tree respectively and if no restriction is placed on the structure of the trees, then the fastest known sequential algorithm for linear tree pattern matching requires O(nm) time in the worst case. Contextual Rewriting
TODO
Deciding Algebraic Properties of Monoids Presented by Finite Church-Rosser Thue Systems
TODO
Two Applications of Equational Theories to Database Theory
Databases and equational theorem proving are well developed and seemingly unrelated areas of Computer Science Research. We provide two natural links between these fields and demonstrate how equational theorem proving can provide useful and tools for a variety of database tasks. An Experiment in Partial Evaluation: The Generation of a Compiler Generator
It has been known for several years that in theory the program transformation principle called partial evaluation or mixsd computation can be used for compiling and compiler generation (given an interpreter for the language to be implemented), and even for the generation of a compiler generator. The present paper describes an experimental partial evaluator able to generate stand-alone compilers and compiler generators. As far as we know, such generations had not been done in practice prior to summer 1984. Partial evaluation of a subIect program with respect to some of its input parameters results in a resfdualprogram. By definition, running the residual program on any remaining input yields the same result as running the original subject program on all of its input. Thus a residual program can be considered a specialization of the subject program to known, fixed values of some of its parameters. A partial evaluator is a program that performs partial evaluation given a subject program and fixed values for some of the program's parameters.
NARROWER: A New Algorithm for Unification and Its Application to Logic Programming
TODO
Solving Type Equations by Graph Rewriting
I have described a syntactic calculus of partially ordered structures and its application to computation. A syntax of record-like terms and a "type subsumption" ordering were defined and shown to form a lattice structure. A simple "type-as-set" interpretation of these term structures extends this lattice to a distributive one, and in the case of finitary terms, to a complete Brouwerian lattice. As a result, a method for solving systems of type equations by iterated rewriting of type symbols was proposed which defines an operational semantics for KBL - a Knowledge Base Language. It was shown that a KBL program can be seen as a system of equations. Thanks to the lattice properties of finite structures, a system of equations admits a least fixed-point solution. The particular order of computation of KBL, the "fan-out computation order", which rewrites symbols closer to the root first was formally defined and shown to be maximal. Unfortunately, the complete "correctness" of KBL is not yet established. That is, it is not known at this point whether the normal form of a term is equal to the fixed-point solution. However, as steps in this direction, two technical lemmas were conjectured to which a proof of the correctness is corollary.
Path of Subterms Ordering and Recursive Decomposition Ordering Revisited
The relationship between several simplification orderings is investigated: PSO, RPO, RDO. RDO is improved in order to deal with more pairs of terms, and made more efficient and easy to handle, by removing useless computations.
Associative Path Orderings
In this paper we introduce a new class of orderings - associative path orderings - for proving termination of associative commutative term rewriting systems. These orderings are based on the concept of simplification orderings and extend the well-known recursive path orderings to E-congruence classes, where E is an equational theory consisting of associativity and commutativity axioms. The associative path ordering is similar to another termination ordering for proving AC termination, described in Dershowitz, et al. (83), which is also based on the idea of transforming terms. Our ordering is conceptually simpler, however, since any term is transformed into a single term, whereas in Dershowitz, et al. (83) the transform of a term is a multiset of terms. More important yet, we show how to lift our ordering to non-ground terms, which is essential for applications of the Knuth-Bendix completion method but was not possible with the previous ordering. A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules
TODO
PETRIREVE: Proving Petri Net Properties with Rewriting Systems
We present here an approach using rewriting systems for analysing and proving properties on Petri nets. This approach is implemented in the system PETRIREVE. By establishing a link between the graphic Petri net design and simulation system PETRIPOTE and the term rewriting system generator REVE, PETRIREVE provides an environment for the design and verification of Petri nets. Representing Petri nets by rewriting systems allows easy and direct proofs of the behaviour correctness of the net to be carried out, without having to build the marking graph or to search for net invariants.
Fairness in Term Rewriting Systems
The notion of fair derivation in a term-rewriting system is introduced, whereby every rewrite rule enabled infinitely often along a derivation is infinitely-often applied. A term-rewriting system is fairly-terminating iff all its fair derivations are finite. The paper presents the following question: is it decidable, for an arbitrary ground term rewriting system, whether it fairly terminates or not? A positive answer is given for several subcases. The general case remains open.
Two Results in Term Rewriting Theorem Proving
Two results are presented in this paper. (1) We extend the term rewriting approach to first order theorem proving, as described in [HsD83], to the theory of first order predicate calculus with equality. Consequently, we have showed that the term rewriting method can be as powerful as paramodulation and resolution combined. Possible improvements of efficiency are also discussed. Handling Function Definitions through Innermost Superposition and Rewriting
This paper presents the operating principles of SLOG, a logic interpreter of equational clauses (Horn clauses where the only predicate is '='). SLOG is based on an oriented form of paramodulation called superposition. Superposition is a complete inference rule for first-order logic with equality. SLOG uses only a strong restriction of superposition (innermost superposition) which is still complete for a large class of programs. Besides superposition, SLOG uses rewriting which provides eager evaluation and handling of negative knowledge. Rewriting combined with superposition improves terminability and control of equational logic programs.
An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras
A new approach based on computing the Gröbner basis of polynomial ideals is developed for solving word problems and unification problems for finitely presented commutative algebras. This approach is simpler and more efficient than the approaches based on generalizations of the Knuth-Bendix completion procedure to handle associative and commutative operators. It is shown that (i) the word problem over a finitely presented commutative ring with unity is equivalent to the polynomial equivalence problem modulo a polynomial ideal over the integers, (ii) the unification problem for linear forms is decidable for finitely presented commutative rings with unity, (iii) the word problem and unification problem for finitely presented boolean polynomial rings are co-NP-complete and co-NP-hard respectively, and (iv) the set of all unifiers of two forms over a finitely presented abelian group can be computed in polynomial time. Examples and results of algorithms based on the Gröbner basis computation are also reported.
Combining Unification Algorithms for Confined Regular Equational Theories
This paper presents a method for combining equational unification algorithms to handle terms containing "mixed" sets of function symbols. For example, given one algorithm for unifying associative-commutative operators, and another for unifying commutative operators, our algorithm provides a method for unifying terms containing both kinds of operators. We restrict our attention to a class of equational theories which we call confined regular theories. The algorithms is proven to terminate with a complete and correct set of E-unifiers. An implementation has been done as part of a larger system for reasoning about equational theories.
An Algebraic Approch to Unification Under Assoiativity and Commutativity
TODO
Unification Problems with One-Sided Distributivity
We show that unification in the equational theory defined by the one-sided distributivity law x×(y+z)=x×y+x×z is decidable and that unification is undecidable if the laws of associativity x+(y+z)=(x+y)+z and unit element 1×x=x×1=x are added. Unification under one-sided distributivity with unit element is shown to be as hard as Markov's problem, whereas unification under two-sided distributivity, with or without unit element, is NP-hard. A quadratic time unification algorithm for one-sided distributivity, which may prove interesting since available universal unification procedures fail to provide a decision procedure for this theory, is outlined. The study of these problems is motivated by possible applications in circuit synthesis and by the need for gaining insight in the problem of combining theories with overlapping sets of operator symbols.
Fast Many-to-One Matching Algorithms
Matching is a fundamental operation in any system that uses rewriting. In most applications it is necessary to match a single subject against many patterns, in an attempt to find subexpressions of the subject that are matched by some pattern. In this paper we describe a many-to-one, bottom-up matching algorithm. The algorithm takes advantage of common subexpressions in the patterns to reduce the amount of work needed to match the entire set of patterns against the subject. Complexity of Matching Problems
We show that the associative-commutative matching problem is NP-complete; more precisely, the matching problem for terms in which some function symbols are uninterpreted and others are both associative and commutative, is NP-complete. It turns out that the similar problems of associative-matching and commutative-matching are also NP-complete. However, if every variable appears at most once in a term being matched, then the associative-commutative matching problem is shown to have an upper-bound of O(|s|*|t|3), where |s| and |t| are respectively the sizes of the pattern s and the subject t.
The Set of Unifiers in Typed Lambda-Calculus as Regular Expression
The main problem for mechanization of the theorem proving in the typed λ-calculus is the problem of determining whether two terms of a fixed type with free variables have the common instance. This unification problem is undecidable for orders ≥2 (see Huet (1973) and Goldfarb (1981)). The Huet (1975) paper contains the description of semi-decision algorithm which in the case of success, returns a substitution called the most general unifier. This algorithm produces the matching tree, in which the most general unifiers are represented by the final branches. The most interesting is the case when the matching tree is infinite and consists of infinite number of most general unifiers. I have noticed that some infinite matching trees have an interesting property: for every infinite branch there is a node which occurs earlier in this tree. It means that there are some fragments which repeated in this tree. In this paper I consider some class of unification problems. For the fixed problem from this class the set of unifiers can be represented by the regular expression built up on the basis of finite alphabet. This alphabet consists of symbols called elementary substitutions. Every word is interpreted as a composition of the elementary substitutions.
As a corollary, any left-linear TRS is CR if P = Q, P -|→W Q or Q -|→W P for every critical pair
Nachum Dershowitz
Samuel M. H. W. Perlo-Freeman, Péter Pröhle
Denis Béchet, Philippe de Groote, Christian Retoré
Jerzy Marcinkowski
In this paper we show that the theorem of Treinen is an easy consequence of a powerful tool first used to establish undecidability results in the theory of logic programming [MP92]. Then we use the tool to give strong refinements of the result of Treinen:
We show that (the ∃*∀* part of) the first order theory of one-step rewriting is undecidable for linear Noetherian rewriting systems.
Then we prove, what we consider to be quite a striking result, that (the ∃*∀* part of) the first order theory of one-step rewriting is undecidable even if the rewriting system is Noetherian and right-ground. Up to our knowledge it is the first known undecidable property of right-ground systems.
Sergei G. Vorobyov
Ana Paula Tomás, Miguel Filgueiras
Klaus U. Schulz
The combination algorithm described in [BS92] can be used to reduce solvability of general E-unification algorithms to solvability of E- and free (Robinson) unification problems with linear constant restrictions. We show that for E ∈ K there exists no polynomial optimization of this combination algorithm for deciding solvability of general E-unification problems, unless P=NP. This supports the conjecture that for E ∈ K there is no polynomial algorithm for combining E-unification with constants with free unification.
Richard Statman
We shall prove the following results concerning effective reduction and conversion strategies for combinators. These results constitute answers to certain questions which have appeared in the literature (with one exception). We believe that these questions are interesting because they get right to the heart of the memory problems inherent in one-step reduction and expansion. These questions appear to be even more subtle for lambda terms where each one-step reduction can create a much more radical change of structure than for combinators.
(1) There is an effective one-step cofinal reduction strategy (answering a question of Barendregt [2] 13.6.6). This is in Section 2.
(2) There is no effective confluence function but there is an effective one-step confluence strategy (answering'a question of Isles reported in [1]). This is in Section 3.
(3) There is an effective one-step enumeration strategy (answering an obvious question). This is in Section 4.
(4) There is an effective one-step Church-Rosser conversion strategy (ldquoalmostrdquo answering a question of Bergstra and Klop [3]). This is in Section 5.
Vincent van Oostrom
Christophe Ringeissen
Manfred Göbel
Edward L. Green, Lenwood S. Heath, Benjamin J. Keller
Kazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi
1996
Claude Kirchner, Christopher Lynch, Christelle Scharff
Alexandre Boudet, Évelyne Contejean, Claude Marché
Jürgen Stuber
Manfred Göbel
Thomas Arts, Jürgen Giesl
Maria C. F. Ferreira
Bernhard Gramlich
Jean-Pierre Jouannaud, Albert Rubio
Roberto Virga
Michael Hanus, Christian Prehofer
Marian Vittek
Roel Bloo, Kristoffer Høgsbro Rose
We identify a large subset of the CRSs, the structure-preserving CRSs, and show for any structure-preserving CRS R that Rx preserves strong normalisation of R.
We believe that this is a significant first step towards providing a methodology for reasoning about the operational properties of higher-order rewriting in general, and higher-order program transformations in particular, since confluence ensures correctness of such transformations and preservation of strong normalisation ensures that the transformations are always safe, in both cases independently of the used reduction strategy.
Delia Kesner
Roberto Di Cosmo
Stefano Guerrini, Simone Martini, Andrea Masini
M. R. K. Krishna Rao
Bernhard Gramlich, Claus-Peter Wirth
Christoph Lüth
As an example, the preservation of confluence under the disjoint union of two term rewriting systems is shown, obtaining an algebraic proof of Toyama's theorem, generalised slightly to term rewriting systems introducing variables on the right-hand side of the rules.
Ralf Treinen
Manfred Schmidt-Schauß
Géraud Sénizergues
Régis Curien, Zhenyu Qian, Hui Shi
Jordi Levy
Roland Fettig, Bernd Löchner
Florent Jacquemard
Concerning sequentiality, the result may be restated in terms of approximations of term rewriting systems. An approximation of a system R is a renaming of the variables in the right hand sides which yields a growing rewrite system. This gives the decidability of a new sufficient condition for sequentiality of left-linear rewrite systems, which encompasses known decidable properties such as strong, NV and NVNF sequentiality.
Masahiko Sakai, Yoshihito Toyama
Vincent van Oostrom
Frédéric Voisin
Reinhard Bündgen, Carsten Sinz, Jochen Walter
Évelyne Contejean, Claude Marché
Mark T. Vandevoorde, Deepak Kapur
H. R. Walters, J. F. Th. Kamperman
Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch
Thomas Hillenbrand, Arnim Buch, Roland Fettig
1995
Massimo Marchiori
Joachim Steinbach
Olav Lysne, Javier Piris
Hans Zantema, Alfons Geser
Robert Nieuwenhuis
Masahito Kurihara, Hisashi Kondo, Azuma Ohuchi
Klaus Schmid, Roland Fettig
Andrea Asperti
Peter Graf
Ilies Alouini
J. F. Th. Kamperman, H. R. Walters
Our method is modelled by a transformation of term rewriting systems, which concisely expresses the intricate interaction between pattern matching and lazy evaluation. The method easily extends to term graph rewriting. We consider only left-linear, confluent term rewriting systems, but we do not require orthogonality.
Siva Anantharaman, Gilles Richard
Taro Suzuki, Aart Middeldorp, Tetsuo Ida
Géraud Sénizergues
Wolfgang Gehrke
Andrea Corradini, Fabio Gadducci, Ugo Montanari
Stefan Kahrs
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, Fer-Jan de Vries
Jan Kuper
Steffen van Bakel, Maribel Fernández
Pierre Lescanne, Jocelyne Rouyer-Degli
Richard J. Boulton
H. R. Walters, Hans Zantema
The first system represents numbers by successor and predecessor. In the second, which defines non-negative integers only, digits are represented as unary operators. In the third, digits are represented as constants. The first and the second system are complete; the second and the third system have logarithmic space and time complexity, and are parameterized for an arbitrary radix (binary, decimal, or other radices). Choosing the largest machine representable single precision integer as radix, results in unbounded arithmetic with machine efficiency.
Habib Abdulrab, Marianne Maksimenko
Franz Baader, Klaus U. Schulz
Friedrich Otto, Paliath Narendran, Daniel J. Dougherty
Jochen Burghardt
Jürgen Avenhaus, Jörg Denzinger, Matthias Fuchs
Françoise Bellegarde
Reinhard Bündgen, Manfred Göbel, Wolfgang Küchlin
Ta Chen, Siva Anantharaman
Jacques Chazarain, Serge Muller
Jürgen Giesl
M. Randall Holmes
Hélène Kirchner, Pierre-Étienne Moreau
Alberto Paccanaro
Mark E. Stickel, Hantao Zhang
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
1993
Christopher Lynch, Wayne Snyder
Jordi Levy, Jaume Agustí-Cullell
Hantao Zhang
Andreas Werner
Therefore, we generalize well-sorted terms to semantically well-sorted terms and well-sorted substitutions to some kind of semantically wellsorted substitutions. Semantically well-sorted terms with respect to a set of equations E are terms that denote well-defined elements in every algebra satisfying E.
We prove a critical pair lemma and Birkhoff's completeness theorem for so-called range unique signatures and arbitrary order-sorted rewriting systems. A transformation is given which allows to obtain an equivalent range unique signature from each non-range-unique one. We also show some decidability results.
Jürgen Avenhaus, Jörg Denzinger
Soumen Chakrabarti, Katherine A. Yelick
Max Moser
Joachim Niehren, Andreas Podelski, Ralf Treinen
Our set defining devices are greatest fixpoint solutions of regular systems of equations with a deterministic form of union. As the main technical particularity of the algorithms we present a novel memorization technique. We believe that both satisfiability and entailment tests can be implemented in an efficient and incremental manner.
Rolf Backofen
Daniel J. Dougherty
Andrea Asperti, Cosimo Laneve
As an easy by-product, we prove that neither overlining nor underlining are required in Lévy's labelling.
Femke van Raamsdonk
Zena M. Ariola
We will also show that orthogonal GRSs are a correct implementation of orthogonal TRSs. The basic idea of the proof is to show that the behavior of a graph can be deduced from its finite approximations, that is, graph rewriting is a continuous operation. Our approach differs from that of other researchers [6, 9], which is based on infinite rewriting.
Nachum Dershowitz, Charles Hoot
Maria C. F. Ferreira, Hans Zantema
Aart Middeldorp, Bernhard Gramlich
Zurab Khasidashvili
John Field
Ernst Lippe
Franz Baader, Klaus U. Schulz
Mohamed Tajine
Anne-Cécile Caron, Jean-Luc Coquidé, Max Dauchet
Jean-Claude Raoult
Maribel Fernández
Albert Rubio, Robert Nieuwenhuis
An important difference w.r.t. their work is that our ordering is not based on polynomial interpretations, but on a total (arbitrary) precedence on the function symbols, like in LPO or RPO (this solves an open question posed e.g. by Bachmair [Bac91]).
A second difference is that we define an extension to terms with variables, which makes the ordering applicable in practice for complete theorem proving strategies with built-in AC-unification and for orienting non-ground rewrite systems.
Our ordering is defined in a simple way by means of rewrite rules, and can be easily (and efficiently) implemented, since its main component is RPO.
Catherine Delor, Laurence Puel
David A. Plaisted
Ursula Martin
Géraud Sénizergues
Pilar Nivela, Robert Nieuwenhuis
Brian Matthews
Reinhard Bündgen
Michael Löwe, Martin Beyer
Rakesh M. Verma
Yexuan Gui, Mitsuhiro Okada
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
Please send any contributions by electronic or ordinary mail to any of us. We hope to continue periodically publicizing new problems and solutions to old ones. We thank all the individuals who contributed questions, updates and solutions
1991
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, Fer-Jan de Vries
In general OTRSs the infinite Church-Rosser Property fails for strongly converging reductions. However for Böhm reduction (as in Lambda Calculus, subterms without head normal forms may be replaced by ⊥) the infinite Church-Rosser property does hold. The infinite Church-Rosser Property for non-unifiable OTRSs follows. The top-terminating OTRSs of Dershowitz c.s. are examples of non-unifiable OTRSs.
William M. Farmer, Ronald J. Watro
David A. Wolfram
Daniel J. Dougherty
Frank Drewes, Clemens Lautemann
Dieter Hofbauer
Stefan Krischer, Alexander Bockmayr
Franz Baader
Eric Domenjoud
Jacques Chabin, Pierre Réty
Franz Baader, Werner Nutt
We identify a large subclass of commutative/monoidal theories that are of unification type zero by studying equations over the corresponding semiring. As a second result, we show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of homomorphisms, and how algorithms for the extended theory can be obtained from algorithms for the basic theory. The two results illustrate how using algebraic machinery can lead to general results and elegant proofs in unification theory.
Francis Klay
Wayne Snyder, Christopher Lynch
Loic Pottier
Hélène Kirchner
Aart Middeldorp, Yoshihito Toyama
Tobias Nipkow, Zhenyu Qian
Pierre-Louis Curien, Giorgio Ghelli
Françoise Bellegarde
Dave Cohen, Phil Watson
We justify our choice of representation in terms of both space efficiency and speed of rewriting.
Finally we give several examples of the use of our system.
Sieger van Denneheuvel, Karen L. Kwast, Gerard R. Renardel de Lavalette, Edith Spaan
Rolf Socher-Ambrosius
Kai Salomaa
Jean-Luc Coquidé, Max Dauchet, Rémi Gilleron, Sándor Vágvölgyi
Gregory Kucherov
Franz-Josef Brandenburg
Albert Gräf
Our method, like most others, is restricted to linear patterns (the case of non-linear matching can be handled as usual by checking the consistency of variable bindings in a separate pass following the matching phase).
R. Ramesh, I. V. Ramakrishnan
In order to find matches quickly our algorithm operates in two phases. In the first phase it scans the subject tree to collect some "information" which is then used to find matches quickly in the second phase. Scanning can become very expensive especially for large subject trees. However the normalization process is "incremental" in nature. After each reduction step the subject tree is altered and this modified tree is usually not completely different from the old tree. Hence it should be possible to avoid scanning and searching the entire tree for new matches. We describe general techniques to exploit the incremental nature of normalization to speed up each reduction step. Specifically, using these techniques we show that the search for new matches in the subject tree following a replacement can be made independent of the size of the subject tree.
Maria Paola Bonacina, Jieh Hsiang
The known definitions of fairness for completion-based methods are designed to ensure the confluence of the resulting system. Thus, a search plan which is fair according to these definitions may force the prover to perform deductions completely irrelevant to prove the intended theorem. In a theorem proving strategy, on the other hand, one is usually only interested in proving a specific theorem. Therefore the notion of fairness should be defined accordingly. In this paper we present a target-oriented definition of fairness for completion, which takes into the account the theorem to be proved and therefore does not require computing all the critical pairs. If the inference rules are complete and the search plan is fair with respect to our definition, then the strategy is complete. Our framework contains also notions of redundancy and contraction. We conclude by comparing our definition of fairness and the related concepts of redundancy and contraction with those in related works.
Jürgen Avenhaus
Andrea Sattler-Klein
Reinhard Bündgen
Miki Hermann
Claude Marché
As a corollary, we show that ground AC-completion, when using a total AC-simplification ordering and an appropriate control, must terminate.
Using a recent result of Narendran and Rusinowitch (in this volume), this implies that the word problem for such a theory is decidable.
Paliath Narendran, Michaël Rusinowitch
Ulrich Fraus
Michel Billaud
Aline Deruyver
Raj Agarwal, David R. Musser, Deepak Kapur, Xumin Nie
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
1989
Franz Baader
The conditions may be regarded as tools which can be used to determine the unification type of given theories. They are also helpful in understanding what makes a theory to be of type zero.
Leo Bachmair
Timothy B. Baird, Gerald E. Peterson, Ralph W. Wilkerson
Hubert Bertling, Harald Ganzinger
Reinhard Bündgen, Wolfgang Küchlin
Hubert Comon-Lundh
This method allows to reduce the problem of inductive proofs in equational theories to Huet and Hullot's proofs by consistency [HH82]. In particular, it is no longer necessary to use the socalled "inductive reducibility test" which is the most expensive part of the Jouannaud and Kounalis algorithm [JK86].
John Darlington, Yike Guo
Max Dauchet
Conal Elliott
Another development is the discovery that by enriching λ→ to include dependent function types, the resulting calculus (λΠ) forms the basis of a very elegant and expressive Logical Framework, encompassing the syntax, rules, and proofs for a wide class of logics.
This paper presents an algorithm in the spirit of Huet's, for unification in λΠ. This algorithm gives us the best of both worlds: the automation previously possible in λ→, and the greatly enriched expressive power of λΠ. It can be used to considerable advantage in many of the current applications of Huet's algorithm, and has important new applications as well. These include automated and semi-automated theorem proving in encoded logics, and automatic type inference in a variety of encoded languages.
Stephen J. Garland, John V. Guttag
Herbert Göttler
Dieter Hofbauer, Clemens Lautemann
Stéphane Kaplan, Christine Choppy
Mike Lai
In addition, what makes this approach different from the others is that notions such as AC-compatibility or coherence modulo AC of reductions induced by sets of rules, which are essential in [Pe-S] or [Jo-Ki] respectively, are not required here. Consequently, a proof of correctness of the completion algorithm (given in [Lai 2]) for constructing a desired set of rules based on this approach can be compared directly with that of Huet in [Hu 2]. In fact, it turns out that all we have to do is to replace terms in [Hu 2] by AC-equivalence classes of terms. The main reason is that all the complications due to AC-compatibility or coherence modulo AC simply are not present here.
Finally, we shall discuss how to minimize the unnecessary computation of some critical pairs during the completion.
Dallas Lankford
Dana May Latch, Ron Sigal
George F. McNulty
Aart Middeldorp
Chilukuri K. Mohan
Chilukuri K. Mohan, Mandayam K. Srivas
Tohru Naoi, Yasuyoshi Inagaki
Sanjai Narain
Tobias Nipkow
Friedrich Otto
Laurence Puel
Uday S. Reddy
R. C. Sekar, Shaunak Pawagi, I. V. Ramakrishnan
Joachim Steinbach
Robert Strandh
The most serious problem with their approach becomes evident when one tries to use their result in a programming system. Once a redex has been found, it must be replaced by a term built from the structure of the right-hand side corresponding to the redex, and from parts of the old term. Then, the reduction process must be restarted so that other redexes can be found. With their approach, a large part of the term tree may have to be rescanned.
Hoffmann and O'Donnell [HO82a] improved the situation by defining the class of strongly left-sequential programs. For this class, a particularly simple reduction algorithm exists. A stack is used to hold information about the state of the reduction process. When a redex has been found and replaced by the corresponding right-hand side, the stack holds all the relevant information needed to restart the reduction process in a well defined state such that no unnecessary rescanning of the term is done.
However, it turns out that the approach of Hoffmann and O'Donnell is unnecessarily restrictive. In this paper, we define a new class of Equational Programs, called the forward branching programs. This class is much larger than the class of strongly left-sequential programs. Together with a new reduction algorithm, briefly discussed in this paper, our approach allows us to use the hardware stack to hold reduction information in a way similar to the way a block structured programming language uses the stack to hold local variables. In effect, our approach allows us to use innermost stabilization, while preserving the overall outermost reduction strategy.
Sophie Tison
Yoshihito Toyama, Jan Willem Klop, Hendrik Pieter Barendregt
Sergei G. Vorobyov
Hantao Zhang, Deepak Kapur
Habib Abdulrab, Jean-Pierre Pécuchet
Siva Anantharaman, Jieh Hsiang, Jalel Mzali
Jürgen Avenhaus, Jörg Denzinger, Jürgen Müller
Jürgen Avenhaus, Klaus Madlener, Joachim Steinbach
Michel Bidoit, Francis Capy, Christine Choppy
Maria Paola Bonacina, Giancarlo Sanna
Jim Christian
Max Dauchet, Aline Deruyver
Deepak Kapur, Hantao Zhang
Hessam Khoshnevisan, K. M. Sephton
Naomi Lindenstrauss
John Pedersen
1987
Robert Strandh
This paper discusses important relationships between two equational programs. In particular we define the term mutual confluence and show that two equational programs with the mutual confluence property have the same output behavior with very general assumptions about the reduction strategy. As an application of our result, we discuss source-to-source transformations of an equational program E to an equational program F. Our transformations are used as a part of a compiler to improve execution time of E by avoiding the creation of too many nodes in the reduction process. We show that our transformations indeed give E and F the mutual confluence property, thus preserving the output behavior of E when transformed to F.
Preserving the output behavior is more general than preserving just normal forms, in that we allow for infinite computations where we output stable parts of the term, i.e., parts that can never change as a result of further reductions.
Stéphane Kaplan
Ursula Martin
Paul Walton Purdom Jr.
Eric Sopena
Craig C. Squier, Friedrich Otto
Does every finitely presented monoid with a decidable word problem have a presentation (Σ;R) where R is a finite canonical rewriting system?
To obtain this answer a certain homological finiteness condition for monoids is considered. If M is a monoid that can be presented by a finite canonical rewriting system, then M is an (FP)3-monoid. Since there are well-known examples of finitely presented groups that have easily decidable word problem, but that do not meet this condition, this implies that there are finitely presented monoids (and groups) with decidable word problem that cannot be presented by finite canonical rewriting systems.
Jos C. M. Baeten, Jan A. Bergstra, Jan Willem Klop
Max Dauchet, Francesco de Comité
Annie Despland, Monique Mazaud, Raymond Rakotozafy
Our approach is based on a target machine description where the basic concepts used (access modes, access classes and instructions) are bottom-up hierarchically described by tree-patterns. These tree-patterns are written in an abstract tree language which is also used to write the intermediate program representation (input to the code generator).
The first phase of code production is based on access mode template-driven rewritings in which the program intermediate representation is progressively transformed into its "canonical form". The result is that each program instruction is reduced to a sequence of elementary instructions, each of these elementary instructions representing an instance of an instruction pattern.
The local and global optimizations phases as well as the storage management phase may be realized by multipass rewritings and attribute evaluations of the canonical form.
In the last phase of code production, each pattern instruction instance of the updated intermediate form is replaced by the corresponding instance of the associated pattern code.
Klaus Madlener, Friedrich Otto
Friedrich Otto
Richard Göbel
Zhenyu Qian
Hélène Kirchner
The goal of that paper is neither to discover recurrence relations in a set of rules generated by completion, nor to predict a priori the divergence of completion, but rather to propose a formalism to deal with the problem of divergence, namely the definition of meta-rules. This paper is an attempt to give answers for different questions:
1) given an infinite set of rules, the first problem is to find a finite set of schemas, here called meta-rules, where some variables, called meta-variables, may have infinite sets of possible values. [...]
2) The main problem is to be able to use mats-rules for deciding the validity or satisfiability of an equation in the equational theory defined by the infinite set of rules. [...]
3) Of course a preliminary definition of how to use meta-rules must be given. [...]
4) Meta-rules can be used to solve equations, with a narrowing-like process. [...]
Leo Bachmair, Nachum Dershowitz
Hans-Jürgen Bürckert, Alexander Herold, Manfred Schmidt-Schauß
Decidability results about the membership of equational theories to the classes above are presented. It is proved that Noetherianness, simplicity, almost collapse freeness and Ω-freeness are undecidable. We show that it is not possible to decide where a given equational theory resides in the unification hierarchy and where in the matching hierarchy.
Jean H. Gallier, Wayne Snyder
As an example of the flexibility of this approach, we apply it to the problem of higher-order unification, and find an improved version of Huet's procedure [8]. Our major new result is the presentation and justification of a method for enumerating (relatively minimal) complete sets of unifiers modulo arbitrary sets of equations.
Pierre Réty
Peter Padawitz
Christine Choppy, Stéphane Kaplan, Michèle Soria
R. Ramesh, I. V. Ramakrishnan
In this paper we present a parallel algorithm for linear tree pattern matching on a PRAM (parallel random access machine) model. Our algorithm exhibits optimal speedup, in the sense that its processor-time product matches the worst-case time complexity of the fastest sequential algorithm.
1985
Hantao Zhang, Jean-Luc Rémy
Friedrich Otto
Stavros S. Cosmadakis, Paris C. Kanellakis
Our first application is a novel way of formulating functional and inclusion dependencies (the most common database constraints) using equations. The central computational problem of dependency implication is directly reduced to equational reasoning. Mathematical techniques from universal algebra provide new proof procedures and better lower bounds for dependency implication. The use of REVE, a general purpose transformer of equations into term rewriting systems, is illustrated on nontrivial sets of functional and inclusion dependencies.
Our second application demonstrates that the uniform word problem for lattices is equivalent to implication of dependencies expressing transitive closure, together with functional dependencies. This natural generalization of functional dependencies, which is not expressible using conventional database theory formulations, has a natural inference system and an efficient decision procedure.
Neil D. Jones, Peter Sestoft, Harald Søndergaard
Pierre Réty, Claude Kirchner, Hélène Kirchner, Pierre Lescanne
Hassan Aït-Kaci
Michaël Rusinowitch
Leo Bachmair, David A. Plaisted
Associative path orderings require less expertise than polynomial orderings. They are applicable to term rewriting systems for which a precedence ordering on the set of operator symbols can be defined that satisfies a certain condition, the associative pair condition. The precedence ordering can often be derived from the structure of the reduction rules. We include termination proofs for various term rewriting systems (for rings, boolean algebra, etc.) and, in addition, point out ways of dealing with equational theories for which the associative pair condition does not hold.
David Detlefs, Randy Forgaard
Christine Choppy, Colette Johnen
Sara Porat, Nissim Francez
Jieh Hsiang
(2) In [KaN84], Kapur & Narendran proposed a method similar to [HsD83]. Motivated by the Kapur-Narendran method, we introduce a notion of splitting for theorem proving in first order predicate calculus. The splitting strategy provides a better utilization of the reduction mechanism of term rewriting systems than the N-strategy in [HsD83], although it generates more critical pairs. Comparisons and the relation between the splitting strategy, Kapur-Narendran method, and the N-strategy are also given.
We conjecture that our way of dealing with first order theories with full equality can be extended to the splitting and the Kapur-Narendran methods as well.
Due to the lack of space, we only give a sketch of the proofs of the completeness of the two theorem proving methods. They will be provided in detail in a longer version of the paper.
Laurent Fribourg
Abdelilah Kandri-Rody, Deepak Kapur, Paliath Narendran
Katherine A. Yelick
Albrecht Fortenbach
Stefan Arnborg, Erik Tidén
Paul Walton Purdom Jr., Cynthia A. Brown
The algorithm uses a compact data structure called a compressed dag to represent the set of patterns. All the variables are represented by a single pattern node. Variable usages are disambiguated by a variable map within the pattern nodes. Two expressions that differ only in the names of their variables are represented by the same node in the compressed dag. A single compressed dag contains all the patterns in the system.
The matching proceeds bottom-up from the leaves of the subject and set of patterns to the roots. The subject keeps track of the variable bindings needed to perform the match. A hashing method is used to speedily retrieve specific nodes of the compressed dag.
The algorithm has been implemented as a part of a Knuth-Bendix completion procedure. In comparison with the standard matching algorithm previously used, the new algorithm reduced the number of calls to the basic match routine to about 1/5 of their former number. It promises to be an effective tool in producing more efficient rewriting systems.
Dan Benanav, Deepak Kapur, Paliath Narendran
Marek Zaionc
Last updated on 17 April 2024.
Come back to main page.