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

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.     

Proving termination of context-sensitive rewriting by transformation

Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite sequences. Proving termination of CSR has been recently recognized as an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. Specifically, a number of transformations that permit treating this problem as a standard termination problem have been described. The main goal of this paper is to contribute to a better comprehension and practical use of transformations for proving termination of CSR. We provide new completeness results regarding the use of the transformations in two restricted (but relevant) settings: (a) proofs of termination of canonical CSR and (b) proofs of termination of CSR by using transformations together with simplification orderings. We have also made an experimental evaluation of the transformations, which complements the theoretical analysis from a practical point of view. This leads to new hierarchies of the transformations which are useful to guide their practical use when implementing tools for proving termination of CSR.     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

Induction for termination with local strategies

In this paper, we propose a method for specifically proving termination of rewriting with particular strategies: local strategies on operators. An inductive proof procedure is proposed, based on an explicit induction on the termination property. Given a term, the proof principle relies on alternatively applying the induction hypothesis on its subterms, by abstracting the subterms with induction variables, and narrowing the obtained terms in one step, according to the strategy. The induction relation, an F -stable ordering having the subterm property, is not given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints.     

Infinitary Combinatory Reduction Systems

We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary λ-calculus are special cases.Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary λ-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes U has a complete development, then all complete developments of U end in the same term and that (2) any tiling diagram involving strongly convergent reductions S and T can be completed iff at least one of S/T and T/S is strongly convergent.We also prove an ancillary result of independent interest: a set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property.     

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.     

Implicit induction in conditional theories

We propose a new procedure for proof by induction in conditional theories where case analysis is simulated by term rewriting. This technique reduces considerably the number of variables of a conjecture to be considered for applying induction schemes. Our procedure is presented as a set of inference rules whose correctness has been formally proved. Moreover, when the axioms are ground convergent and the functions are completely defined, it is possible to apply the system for refuting conjectures. The procedure is even refutationally complete for conditional equations with Boolean preconditions over free constructors. The method is entirely implemented in the proverSPIKE. This system has solved interesting problems in a completely automatic way, that is, without interaction with the user and without ad hoc heuristics. It has also proved the challenging Gilbreath card trick, with only two easy lemmas.Preliminary versions of the results have been presented at the 13th International Joint Conference on Artificial Intelligence, Chambéry (France), 1993 (Bouhoula and Rusinowith, 1993).     

Certifying Term Rewriting Proofs in ELAN

Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions (ρσ-calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity).     

On confluence and residuals in Cauchy convergent transfinite rewriting

We show that non-collapsing orthogonal term rewriting systems do not have the transfinite Church-Rosser property in the setting of Cauchy convergence. In addition, we show that for (a transfinite version of) the Parallel Moves Lemma to hold, any definition of residual for Cauchy convergent rewriting must either part with a number of fundamental properties enjoyed by rewriting systems in the finitary and strongly convergent settings, or fail to hold for very simple rewriting systems.     

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

External Rewriting for Skeptical Proof Assistants

This paper presents the design, the implementation, and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external because it consists in performing term rewriting in a specific and efficient environment and checking the computations later in a proof assistant. Two typical systems are considered in this work: ELAN, based on the rewriting calculus, as the term rewriting-based environment, and Coq, based on the calculus of inductive constructions as the proof assistant. We first formalize the proof terms for deduction by rewriting and strategies in ELAN using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into Coq syntax where they can be directly type checked. For the method to be applicable for rewriting modulo associativity and commutativity, we provide an effective method to prove equalities modulo these axioms in Coq using ELAN. These results have been integrated into an ELAN-based rewriting tactic in Coq.     

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.     

A decidable word problem without equivalent canonical term rewriting system

We present a weak associative single-axiom system having the following property: the word problem is decidable with an efficient algorithm even though there does not exist any finite equivalent canonical term rewriting system.     

A calculus for and termination of rippling

Rippling is a type of rewriting developed for inductive theorem proving that uses annotations to direct search. Rippling has many desirable properties: for example, it is highly goal directed, usually involves little search, and always terminates. In this paper we give a new and more general formalization of rippling. We introduce a simple calculus for rewriting annotated terms, close in spirit to first-order rewriting, and prove that is has the formal properties desired of rippling. Next we develop criteria for proving the termination of such annotated rewriting, and introduce orders on annotated terms that lead to termination. In addition, we show how to make rippling more flexible by adapting the termination orders to the problem domain. Our work has practical as well as theoretical advantages: it has led to a very simple implementation of rippling that has been integrated in the Edinburgh CLAM system. Funded by the German Ministry for Research and Technology under grant ITS 9102. Supported by a Human Capital and Mobility Research Fellowship from the European Commission. Both authors thank members of the Edinburgh Mathematical Reasoning Group, as well as Alan Bundy, Leo Bachmair, Dieter Hutter, and Michael Rusinowitch, for their comments on previous drafts. Additional support was also received from the MInd grant EC-US 019-76094.     

Automated proofs of the moufang identities in alternative rings

In this paper we present automatic proofs of the Moufang identities in alternative rings. Our approach is based on the term rewriting (Knuth-Bendix completion) method, enforced with various features. Our proofs seem to be the first computer proofs of these problems done by a general purpose theorem prover. We also present a direct proof of a certain property of alternative rings without employing any auxiliary functions. To our knowledge our computer proof seems to be the first direct proof of this property, by human or by a computer.On leave from the Department of Computer Science, UNYY at Stony Brook, New York. Research supported in part by NSF grants CCR-8805734, INT-8715231, and CCR-8901322.     

项重写的图实现

图重写能够有效地实现项重写。文章从项重写的图实现的角度出发，研究了图重写模拟项重写的正确性和完备性：在无环出现的情况下，图重写对一切项重写下正确；在无环出现的条件下，图重写对左线性合流的项重写是完备的。     

Decidability for Left-Linear Growing Term Rewriting Systems

A term rewriting system is called growing if each variable occurring on 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-nonlinear 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 right-ground 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.     

高效率重写型程序的设计

本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例．比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中．动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。