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.     

On termination of the direct sum of term-rewriting systems

Some sufficient conditions are given for the termination of the direct sum of two term-rewriting systems: either no right-hand side of a rule is a variable, or no right-hand side contains more occurences of a variable than the corresponding left-hand side.     

Characterizing and proving operational termination of deterministic conditional term rewriting systems

We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms (i.e., terms over the signature of the DCTRS). This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of Duran et al. (2008) [10].     

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.     

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.     

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.     

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 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.     

Reachability and confluence are undecidable for flat term rewriting systems

Ground reachability, ground joinability and confluence are shown undecidable for flat term rewriting systems, i.e., systems in which all left and right members of rule have depth at most one.     

An initial algebra approach to term rewriting systems with variable binders

We present an extension of first-order term rewriting systems. It involves variable binding in the term language. We develop systems called binding term rewriting systems (BTRSs) in a stepwise manner. First we present the term language, then formulate equational logic. Finally, we define rewriting systems. This development is novel because we follow the initial algebra approach in an extended notion of Σ-algebras in various functor categories. These are based on Fiore-Plotkin-Turi’s presheaf semantics of variable binding and Lüth-Ghani’s monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs as initial algebras in suitable categories. Then, we show an important rewriting property of BTRSs: orthogonal BTRSs are confluent. Moreover, by using the initial algebra semantics, we give a complete characterisation of termination of BTRSs. Finally, we discuss our design choice of BTRSs from a semantic perspective. An erlier version appeared in Proc. Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP2003).     

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.     

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     

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     

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications

In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property.     

Relating confluence,innermost-confluence and outermost-confluence properties of term rewriting systems

Innermost-confluence is important in giving call-by-value and denotational semantics and outermost-confluence is important in giving call-by-need and lazy semantics of programs. In this paper, we give a few sets of sufficient conditions under which the properties of confluence, innermost-confluence and outermost-confluence coincide. Confluence and innermost-confluence coincide for weakly innermost normalizing overlay systems and confluence and outermost-confluence coincide for outermost normalizing left-linear overlay systems. In general, every weakly innermost (outermost) normalizingconfluent system isinnermost (outermost) confluent but the converse is not true.     

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).