Rewriting - Abstract Rewriting Systems

Abstract Rewriting Systems

From the above examples, it's clear that we can think of rewriting systems in an abstract manner. We need to specify a set of objects and the rules that can be applied to transform them. The most general (unidimensional) setting of this notion is called an abstract reduction system, (abbreviated ARS), although more recently authors use abstract rewriting system as well. (The preference for the word "reduction" here instead of "rewriting" constitutes a departure from the uniform use of "rewriting" in the names of systems that are particularizations of ARS. Because the word "reduction" does not appear in the names of more specialized systems, in older texts reduction system is a synonym for ARS).

An ARS is simply a set A, whose elements are usually called objects, together with a binary relation on A, traditionally denoted by →, and called the reduction relation, rewrite relation or just reduction. This (entrenched) terminology using "reduction" is a little misleading, because the relation is not necessarily reducing some measure of the objects; this will become more apparent when we discuss string rewriting systems further in this article.

Example 1. Suppose the set of objects is T = {a, b, c} and the binary relation is given by the rules a → b, b → a, a → c, and b → c. Observe that these rules can be applied to both a and b in any fashion to get the term c. Such a property is clearly an important one. Note also, that c is, in a sense, a "simplest" term in the system, since nothing can be applied to c to transform it any further. This example leads us to define some important notions in the general setting of an ARS. First we need some basic notions and notations.

• is the transitive closure of, where = is the identity relation, i.e. is the smallest preorder (reflexive and transitive relation) containing . It is also called the reflexive transitive closure of .
• is, that is the union of the relation → with its inverse relation, also known as the symmetric closure of .
• is the transitive closure of, that is is the smallest equivalence relation containing . It is also known as the reflexive transitive symmetric closure of .