Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2002 | Book

Motivation Read chapter Read first chapter

Advanced Topics in Term Rewriting

Author: Enno Ohlebusch

Publisher: Springer New York

Included in: Professional Book Archive

Login to get access
insite
SEARCH

About this book

Term rewriting techniques are applicable in various fields of computer sci­ ence: in software engineering (e.g., equationally specified abstract data types), in programming languages (e.g., functional-logic programming), in computer algebra (e.g., symbolic computations, Grabner bases), in pro­ gram verification (e.g., automatically proving termination of programs), in automated theorem proving (e.g., equational unification), and in algebra (e.g., Boolean algebra, group theory). In other words, term rewriting has applications in practical computer science, theoretical computer science, and mathematics. Roughly speaking, term rewriting techniques can suc­ cessfully be applied in areas that demand efficient methods for reasoning with equations. One of the major problems one encounters in the theory of term rewriting is the characterization of classes of rewrite systems that have a desirable property like confluence or termination. If a term rewriting system is conflu­ ent, then the normal form of a given term is unique. A terminating rewrite system does not permit infinite computations, that is, every computation starting from a term must end in a normal form. Therefore, in a system that is both terminating and confluent every computation leads to a result that is unique, regardless of the order in which the rewrite rules are applied. This book provides a comprehensive study of termination and confluence as well as related properties.

Table of Contents

Frontmatter
1. Motivation
Abstract
Equations were among the first mathematical achievements of mankind. For example, they appear in old Babylonian texts written in cuneiform characters that date back to the third millennium B.C. This is not surprising because equational reasoning (replacing equals with equals, that is) occurs frequently in day-to-day life. For example, in calculating a simple arithmetic expression like (3 + 3) * 6, one first uses the equation 3 + 3 = 6 to replace the expression or the term (3 + 3) * 6 with 6*6. In a second step this term further rewrites to 36, the result of the computation. In calculating the intuitively simplest term equal to (3 + 3) * 6, no one would use the equation 3 + 3 = 6 to replace the term (3 + 3) * 6 with the term (3 + 3) * (3 + 3). In other words, the equation 3 + 3 = 6 is used as a rewrite rule: the left-hand side can be replaced with the right-hand side, but not vice versa. This one-directional replacement of equals with equals is what distinguishes term rewriting from equational logic.
Enno Ohlebusch
2. Abstract Reduction Systems
Abstract
We will introduce term rewriting by first abstracting from the term structure. In other words, to start, we will concentrate on the so-called abstract reduction systems (ARSs).
Enno Ohlebusch
3. Term Rewriting Systems
Abstract
In this chapter we will present the basic concepts of term rewriting that are needed in this book. More details on term rewriting, its applications, and related subjects can be found in the textbook of Baader and Nipkow [BN98]. Readers versed in German are also referred to the textbooks of Avenhaus [Ave95], Bündgen [Bün98], and Drosten [Dro89]. Moreover, there are several survey articles [HO80, DJ90, Klo92, Pla93] that can also be consulted.
Enno Ohlebusch
4. Confluence
Abstract
In this chapter, we will recall several well-known results concerning confluence. First, it will be shown that confluence is in general an undecidable property of TRSs. Then we shall see that confluence is decidable for finite terminating systems. Moreover, two sufficient criteria for confluence of possibly nonterminating TRSs will be given.
Enno Ohlebusch
5. Termination
Abstract
In this chapter we will first sketch a proof of the well-known fact that termination is undecidable. In Chapter 6 this result will be strengthened in several respects. In Section 5.2 standard methods for proving termination are reviewed: Polynomial interpretations yield polynomial termination, whereas recursive path orderings show simple termination. As a matter of fact, there are several other properties related to termination that form the so-called termination hierarchy. We will review this hierarchy in Section 5.3. After that, some newer techniques for proving termination will be treated: the dependency pair method, semantic labeling, and type introduction. Finally, we will study innermost termination.
Enno Ohlebusch
6. Relative Undecidability
Abstract
In order to motivate relative undecidability, let us consider the following scenario. All methods for proving termination of a TRS ℛ fail but an implementation of the dependency pair method is able to prove innermost termination of ℛ automatically. In view of the fact that nonterminating but innermost terminating systems hardly occur in practice, it is most likely that ℛ is in fact terminating. But how can we prove this?
Enno Ohlebusch
7. Conditional Rewrite Systems
Abstract
Conditional term rewriting systems naturally come into play in the algebraic specification of abstract data types. The specification by positive conditional equations is not only more natural but also more expressive; see [BM84, BN98]. Papers like Kaplan [Kap84] and Bergstra and Klop [BK86] are mainly motivated by this point of view. Now, conditional term rewriting plays a fundamental role in the integration of functional and logic programming; see Hanus [Han94] for an overview of this field. Moreover, it should not be forgotten that conditional systems have been used as a proof-theoretic tool for establishing properties of unconditional term rewriting systems as well as λ-calculus extensions; for an overview, see Klop and de Vrijer [KV90].
Enno Ohlebusch
8. Modularity
Abstract
Modularity is a well-known programming paradigm in computer science. Programmers should design their programs in a modular way, that is, as a combination of small programs. These so-called modules are implemented separately and are then integrated to form the program as a whole. Because TRSs have many important applications in computer science, it is important (not only from a theoretical viewpoint but also from a practical point of view) to know under which conditions a combined system inherits desirable properties from its constituent systems. For this reason modular aspects of term rewriting have been extensively studied in the past decade. To render a detailed account of all known modularity results goes beyond the scope of this book. Instead, we will give an overview of the most important results for TRSs (Section 8.2) and CTRSs (Section 8.7). We will also present selected results in detail.
Enno Ohlebusch
9. Graph Rewriting
Abstract
For reasons of efficiency, term rewriting is usually implemented by graph rewriting. In term rewriting, expressions are represented as terms, whereas in graph rewriting1 these are represented as directed graphs. In contrast to the former, the latter representation allows a sharing of common subexpressions. In graph rewriting expressions are evaluated by rule-based graph transformations. Here we will only consider directed acyclic graphs.
Enno Ohlebusch
10. Proving Termination of Logic Programs
Abstract
Proving correctness of a program consists in showing partial correctness (that is, the program meets its specification) and termination (that is, the program cannot run forever). Methods for deciding termination of programs cannot exist because termination is in general undecidable. This motivates the search for sufficient conditions that guarantee termination of a program. If such a technique is successful, it will return the answer: “Yes, the program is terminating.” In all other cases, it might not be able to determine whether the program terminates. In the last decade, the problem of (automatically) proving termination of logic programs has been receiving increasing attention. Many methods have been proposed to prove termination of logic programs; we will not attempt to review all of them here. Instead, we refer to the overview article of De Schreye and Decorte [SD94] ; more recent techniques are discussed in Krishna Rao et al. [KRKS98].
Enno Ohlebusch
Backmatter
Metadata
Title
Advanced Topics in Term Rewriting
Author
Enno Ohlebusch
Copyright Year
2002
Publisher
Springer New York
Electronic ISBN
978-1-4757-3661-8
Print ISBN
978-1-4419-2921-1
DOI
https://doi.org/10.1007/978-1-4757-3661-8