Proving termination of normalization functions for conditional expressions

Boyer and Moore have discussed a function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its recursion relation, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the computational meaning of those two proofs.A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential.     

Proving geometry theorems with rewrite rules

We investigate the application of rewrite rules to proving theorems from elementary geometry. We have proven 80 theorems, some of them quite difficult. There is a discussion of the formulation of the problem and degenerate conditions. The authors thank the National Science Foundation for its support of the work described in this article.     

A path ordering for proving termination of AC rewrite systems

We describe a method that extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy for proving termination of associative-commutative (AC) rewrite systems. Instead of comparing the arguments of an AC-operator using the multiset extension, wepartition them into disjoint subsets and use each subset only once for comparison. To preserve transitivity, we introduce two techniques —pseudocopying andelevating of arguments of an AC operator. This method imposesno restrictions at all on the underlying precedence relation on function symbols. It can therefore prove termination of a much more extensive class of AC rewrite systems than can previous methods, such as associative path ordering, that restrict AC operators to be minimal or subminimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented inRRL, Rewrite Rule Laboratory, a theorem-proving environment based on rewrite techniques and completion.A preliminary version appears in Proc. of10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India (1990).Partially supported by the National Science Foundation Grant no. CCR-8906678.Partially supported by the National Science Foundation Grant no. CCR-9009755Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.     

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 GHC programs

A transformational approach for proving termination of parallel logic programs such as GHC programs is proposed. A transformation from GHC programs to term rewriting systems is developed; it exploits the fact that unifications in GHC-resolution correspond to matchings. The termination of a GHC program for a class of queries is implied by the termination of the resulting rewrite system. This approach facilitates the applicability of a wide range of termination techniques developed for rewrite systems in proving termination of GHC programs. The method consists of three steps: (a) deriving moding information from a given GHC program, (b) transforming the GHC program into a term rewriting system using the moding information, and finally (c) proving termination of the resulting rewrite system. Using this method, the termination of many benchmark GHC programs such as quick-sort, merge-sort, merge, split, fair-split and append, etc., can be proved. This is a revised and extended version of Ref. 12). The work was partially supported by the NSF Indo-US grant INT-9416687 Kapur was partially supported by NSF Grant nos. CCR-8906678 and INT-9014074. M. R. K. Krishna Rao, Ph.D.: He currently works as a senior research fellow at Griffith University, Brisbane, Australia. His current interests are in the areas of logic programming, modular aspects and noncopying implementations of term rewriting, learning logic programs from examples and conuterexamples and dynamics of mental states in rational agent architectures. He received his Ph.D in computer science from Tata Institute of Fundamental Research (TIFR), Bombay in 1993 and worked at TIFR and Max Planck Institut für Informatik, Saarbrücken until January 1997. Deepak Kapur, Ph.D.: He currently works as a professor at the State University of New York at Albany. His research interests are in the areas of automated reasoning, term rewriting, constraint solving, algebraic and geometric reasoning and its applications in computer vision, symbolic computation, formal methods, specification and verification. He obtained his Ph.D. in Computer Science from MIT in 1980. He worked at General Electric Corporate Research and Development until 1987. Prof. Kapur is the editor-in-chief of the Journal of Automated Reasoning. He also serves on the editorial boards of Journal of Logic Programming, Journal on Constraints, and Journal of Applicable Algebra in Engineering, Communication and Computer Science. R. K. Shyamasundar, Ph.D.: He currently works as a professor at Tata Institute of Fundamental Research (TIFR), Bombay. His current intersts are in the areas of logic programming, reactive and real time programming, constraint solving, formal methods, specification and verification. He received his Ph.D in computer science from Indian Institute of Science, Bangalore in 1975 and has been a faculty member at Tata Institute of Fundamental Research since then. He has been a visiting/regular faculty member at Technological University of Eindhoven, University of Utrecht, IBM TJ Watson Research Centre, Pennsylvania State University, University of Illinois at Urbana-Champaign, INRIA and ENSMP, France. He has served on (and chaired) Program Committees of many International Conferences and has been on the Editorial Committees.     

Murg term rewrite systems

The union of a monadic and a right-ground term rewrite system is called a murg term rewrite system. We show that for murg TRSs the ground common ancestor problem is undecidable. We show that for a murg term rewrite system it is undecidable whether the set of descendants of a ground tree is a recognizable tree language. We show that it is undecidable whether a murg term rewrite system over Σ preserves Σ-recognizability.     

Proving termination of nonlinear command sequences

We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop’s condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.     

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

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.     

Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.     

Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems

The aim of this paper is to propose an algorithm to decide the confluence of finite ground term rewrite systems. Actually a more general class of possibly infinite ground term rewrite systems is studied. It is well known that the confluence is not decidable for general term rewrite systems, but this paper proves it is for ground term rewrite systems following a conjecture made by Huet and Oppen in their survey. The result is also applied to the confluence of left-linear and right-ground term rewrite systems. We also sketch an algorithm for checking this property. This algorithm is based on tree automata and tree transducers. Here, we regard them as rewrite systems and specialists in automata theory would translate that easily in their language.     

Termination of rewrite systems by elementary interpretations

We focus on termination proofs of rewrite systems, especially of rewrite systems containing associative and commutative operators. We prove their termination by elementary interpretations, more specifically, by functions defined by addition, multiplication and exponentiation. We discuss a method based on polynomial interpretations and propose an implementation of a mechanisation of the comparison of expressions built with polynomials and exponentials.     

Generating priority rewrite systems for OSOS process languages

We propose an algorithm for generating a Priority Rewrite System (PRS) for an arbitrary process language in the OSOS format such that rewriting of process terms is sound for bisimulation and head normalising. The algorithm is inspired by a procedure which was developed by Aceto, Bloom and Vaandrager and presented in Turning SOS rules into equations [L. Aceto, B. Bloom, F.W. Vaandrager, Turning SOS rules into equations, Information and Computation 111 (1994) 1–52].For a subclass of OSOS process languages representing finite behaviours the PRSs that are generated by our algorithm are strongly normalising (terminating) and confluent, where termination is proved using the dependency pair and dependency graph techniques. Additionally, such PRSs are complete for bisimulation on closed process terms modulo associativity and commutativity of the choice operator of CCS. We illustrate the usefulness of our results, and the benefits of rewriting with priorities in general, with several examples.     

Smoothed (conditional) perturbation analysis of discrete event dynamical systems

A new sample path analysis approach based on the smoothing property of conditional expectation for estimating the performance sensitivity of discrete event dynamical systems is proposed. Several examples are presented to show how this approach overcomes a difficulty of the ordinary infinitesimal perturbation analysis. The basic message is that one can get more knowledge about the system performance by observing and analyzing the sample path than by using the conventional simulation approach. It is also pointed out that the classical queueing theory approach for getting the performance sensitivity and the sample path based infinitesimal perturbation analysis approach can be unified in the framework of the new approach, the smoothed (conditional) perturbation analysis.     

Invariants and closures in the theory of rewrite systems

The article investigates some useful concepts of rewrite systems, especially invariants and closures. The concepts are formalised with so-called string expressions, for which an axiomatisation is given. The central operator in the theory of rewrite systems, the rewrite operator, is introduced with formulas that permit a calculational approach. The connections with distributed programming are also explained.     

On decidability of LTL model checking for process rewrite systems

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL) with both future and past operators. It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes.We show that the problem is decidable for wPRS if we consider properties defined by LTL formulae with only modalities strict eventually, strict always, and their past counterparts. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.