Counterexamples in infinitary rewriting with non-fully-extended rules

We show counterexamples exist to confluence modulo hypercollapsing subterms, fair normalisation, and the normal form property in orthogonal infinitary higher-order rewriting with non-fully-extended rules. This sets these systems apart from both fully-extended and finite systems, where no such counterexamples are possible.     

On sufficient-completeness and related properties of term rewriting systems

Summary The decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.Partially supported by the National Science Foundation Grant no. DCR-8408461     

Decidable call-by-need computations in term rewriting

The theorem of Huet and Lévy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if the term under consideration has a normal form, forms the basis of all results on optimal normalizing strategies for orthogonal rewrite systems. However, needed redexes are not computable in general. In the paper we show how the use of approximations and elementary tree automata techniques allows one to obtain decidable conditions in a simple and elegant way. Surprisingly, by avoiding complicated concepts like index and sequentiality we are able to cover much larger classes of rewrite systems. We also study modularity aspects of the classes in our hierarchy. It turns out that none of the classes is preserved under signature extension. By imposing various conditions we recover the preservation under signature extension. By imposing some more conditions we are able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations.     

Conversion to tail recursion in term rewriting

Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs).     

Constructing malware normalizers using term rewriting

A malware mutation engine is able to transform a malicious program to create a different version of the program. Such mutation engines are used at distribution sites or in self-propagating malware in order to create variation in the distributed programs. Program normalization is a way to remove variety introduced by mutation engines, and can thus simplify the problem of detecting variant strains. This paper introduces the “normalizer construction problem” (NCP), and formalizes a restricted form of the problem called “NCP=”, which assumes a model of the engine is already known in the form of a term rewriting system. It is shown that even this restricted version of the problem is undecidable. A procedure is provided that can, in certain cases, automatically solve NCP= from the model of the engine. This procedure is analyzed in conjunction with term rewriting theory to create a list of distinct classes of normalizer construction problems. These classes yield a list of possible attack vectors. Three strategies are defined for approximate solutions of NCP=, and an analysis is provided of the risks they entail. A case study using the virus suggests the approximations may be effective in practice for countering mutated malware. R. Mathur is presently at McAfee AVERT Labs.     

Using term rewriting to verify software

This paper describes a uniform approach to the automation of verification tasks associated with while statements, representation functions for abstract data types, generic program units, and abstract base classes. Program units are annotated with equations containing symbols defined by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and sufficient completeness. Sets of axioms are developed by stepwise extensions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural induction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductive arguments and providing hints for necessary lemmas, without which formal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain     

On tree automata that certify termination of left-linear term rewriting systems

We present a new method for automatically proving termination of left-linear term rewriting systems on a given regular language of terms. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present two methods to construct the enrichment: roof heights for left-linear systems, and match heights for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.     

Operational termination of conditional term rewriting systems

We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs.     

Shallow confluence of conditional term rewriting systems

Recursion can be conveniently modeled with left-linear positive/negative-conditional term rewriting systems, provided that non-termination, non-trivial critical overlaps, non-right-stability, non-normality, and extra variables are admitted. For such systems we present novel sufficient criteria for shallow confluence and arrive at the first decidable confluence criterion admitting non-trivial critical overlaps. To this end, we restrict the introduction of extra variables of right-hand sides to binding equations and require the critical pairs to have somehow complementary literals in their conditions. Shallow confluence implies [level] confluence, has applications in functional logic programming, and guarantees the object-level consistency of the underlying data types in the inductive theorem prover QuodLibet.     

Nondeterministic algebraic specifications and nonconfluent term rewriting

Algebraic specifications are generalized to the case of nondeterministic operations by admitting models with set-valued functions (multialgebras). General (in particular, nonconfluent) term-rewriting systems are studied as a specification language for this semantic framework. A calculus for nondeterministic specifications is given which is similar to term rewriting but which employs an additional determinacy predicate. Soundness, ground completeness, and initiality results are given. Small examples illustrate the range of possible applications.     

Well limit behaviors of term rewriting systems

The limit behaviors of computations have not been fully explored. It is necessary to consider such limit behaviors when we consider the properties of infinite objects in computer science, such as infinite logic programs, the symbolic solutions of infinite polynomial equations. Usually, we can use finite objects to approximate infinite objects, and we should know what kinds of infinite objects are approximable and how to approximate them effectively. A sequence {R _k : k ε ω} of term rewriting systems has the well limit behavior if under the condition that the sequence has the set-theoretic limit or the distance-based limit, the sequence {Th(R _k ): k ε ω} of corresponding theoretic closures of R _k has the set-theoretic or distance-based limit, and lim _k→∞ Th(R _k ) is equal to the theoretic closure of the limit of {R _k : k ε ω}. Two kinds of limits of term rewriting systems are considered: one is based on the set-theoretic limit, the other is on the distance-based limit. It is proved that given a sequence {R _k : κ ε ω} of term rewriting systems R _k , if there is a well-founded ordering ≺ on terms such that every R _k is ≺-well-founded, and the set-theoretic limit of {R _k : κ ε ω} exists, then {R _k : κ ε ω} has the well limit behavior; and if (1) there is a well-founded ordering ≺ on terms such that every R _k is ≺-well-founded, (2) there is a distance d on terms which is closed under substitutions and contexts and (3) {R _k : k ε ω} is Cauchy under d then {R _κ: κ ε ω} has the well limit behavior. The results are used to approximate the least Herbrand models of infinite Horn logic programs and real Horn logic programs, and the solutions and Gr?bner bases of (infinite) sets of real polynomials by sequences of (finite) sets of rational polynomials.     

The undecidability of self-embedding for term rewriting systems

The self-embedding property of term rewriting systems is closely related to the uniform termination property, since a nonself-embedding term rewriting system is uniform terminating. The self-embedding property is shown to be undecidable and partially decidable. It follows that the nonself-embedding property is not partially decidable. This is true even for globally finite term rewriting systems. The same construction gives an easy alternate proof that uniform termination is undecidable in general and also for globally finite term rewriting systems. Also, the looping property is shown to be undecidable in the same way.     

A compact fixpoint semantics for term rewriting systems

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.     

A class of confluent term rewriting systems and unification

The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.     

The unification problem for confluent right-ground term rewriting systems

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 confluent right-ground TRSs is shown to be decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm for obtaining a substitution whose range consists of minimal terms is proposed. Our result extends the decidability of unification for canonical (i.e., terminating and confluent) right-ground TRSs given by Hullot [Proceedings of the 5th Conference on Automated Deduction, LNCS, vol. 87, 1980, p. 318] in the sense that the termination condition can be omitted.     

Indefinite integration as term rewriting: Integrals containing tangent

We describe the development of a term-rewriting system for indefinite integration; it is also called a rule-based evaluation system. The development is separated into modules, and we describe the module for a wide class of integrands containing the tangent function.     

Termination of term rewriting: interpretation and type elimination

We investigate proving termination of term rewriting systems by interpretation of terms in a well-founded monotone algebra. The well-known polynomial interpretations can be considered as a particular case in this framework. A classification of types of termination, including simple termination, is proposed based on properties in the semantic level. A transformation on term rewriting systems eliminating distributive rules is introduced. Using this distribution elimination a new termination proof of the system SUBST of Hardin and Laville (1986) is given. This system describes explicit substitution in λ-calculus.Another tool for proving termination is based on introduction and removal of type restrictions. A property of many-sorted term rewriting systems is called persistent if it is not affected by removing the corresponding typing restriction. Persistence turns out to be a generalization of direct sum modularity, but is more powerful for both proving confluence and termination. Termination is proved to be persistent for the class of term rewriting systems for which not both duplicating rules and collapsing rules occur, generalizing a similar result of Rusinowitch for modularity. This result has nice applications, in particular in undecidability proofs.     

Flatterms,discrimination nets,and fast term rewriting

We describe a new representation for first-order terms which is amenable to simple and fast traversal and matching operations. In addition, we describe some efficient discrimination net indexing algorithms which use the new term representation. We have implemented these ideas in a term rewriting system called HIPER, and have obtained substantial speedups.The work reported here was conducted at MCC and at the University of Texas at Austin.