Lecture
In mathematics, linguistics, computer science, and logic, rewriting covers a wide range of methods for replacing subterms of a formula with other terms. Such methods can be implemented using rewriting systems (also known as rewrite systems, rewriting engines, or reduction systems). In their simplest form, they consist of a set of objects and relations that determine how these objects are transformed.
Rewriting can be non-deterministic. A single rule for rewriting a term may be applicable to it in several different ways, or several rules may be applicable at once. In such a case, rewriting systems provide not an algorithm for replacing one term with another, but a set of possible ways in which the rules can be applied. However, when combined with an appropriate algorithm, rewriting systems can be viewed as computer programs, and some theorem provers and declarative programming languages are based on term rewriting.
Rewriting — a broad range of techniques, methods, and theoretical results related to the procedures of sequentially replacing parts of formulas or terms of a formal language according to a given scheme — a system of rewriting rules. In its most general form, it refers to a collection of a set of objects and rules — relations between these objects that indicate how to transform this set.
Rewriting can be non-deterministic. For example, a system of rewriting rules may include a rule that can be applied to the same term in several different ways, without specifying which particular way should be applied in any given case. If a rewriting system is nevertheless formulated as an unambiguously understood algorithm, it can be regarded as a computer program. A number of interactive theorem-proving systems and declarative programming languages are based on rewriting techniques.
The basic properties of rewriting systems can be formulated without resorting to a specific implementation of them as operations on terms. For this purpose, the notion of an Abstract Reduction System or ARS (short for Abstract Reduction Systems) is often used. An ARS consists of some set A and a set of binary relations (→α)α∈I
on it, called reductions. It is said that a reduces or rewrites to b in one step with respect to a given ARS if the pair (a,b) belongs to some →α
. The most important properties of reduction systems are:
Obviously, confluence implies weak confluence, and termination, correspondingly, implies weak termination. However, confluence and termination are not related to each other. For example, a system consisting of the single rule a•b → b•a is confluent but not terminating. A system consisting of the two rules a → b and a → c is terminating but not confluent, while all three rules together form a system that is neither terminating nor confluent.
Termination of a reduction system makes it possible to assign to each element its normal form — an element to which it can be reduced but which can itself no longer be reduced. If confluence also holds, then such a normal form will always be unique, or canonical. In this connection, the Church-Rosser property is especially valuable, since it allows the problem of the equality of two elements a and b to be solved quickly and efficiently with respect to the system of equalities corresponding to the set of reductions without regard to direction. For this, it suffices to compute the normal forms of both elements. Since in this case the normal form will also be canonical, the elements will be equal if and only if the results coincide.
In logic, the procedure for obtaining the conjunctive normal form (CNF) of a formula can be implemented as a rewriting system. [ 6 ] For example, the rules of such a system would be as follows:
(double negation elimination)
(De Morgan's laws)
(distributivity)
In each rule, every variable denotes a subexpression, and the symbol ( 
) means that the expression corresponding to the left-hand side can be rewritten as the expression corresponding to the right-hand side. In such a system, each rule is a logical equivalence, so rewriting an expression according to these rules does not change its truth value. Other useful rewriting systems in logic may not preserve truth values, see, for example, equisatisfiability.
Term rewriting systems can be used to compute arithmetic operations on natural numbers. To do this, each such number must be encoded as a term. The simplest encoding is used in the Peano axioms and is based on the constant 0 (zero) and the successor function S. For example, the numbers 0, 1, 2, and 3 are represented by the terms 0, S(0), S(S(0)), and S(S(S(0))) respectively. The following term rewriting system can then be used to compute the sum and product of given natural numbers.
For example, the computation of 2+2, resulting in 4, can be reproduced by rewriting the term as follows:
→(2)
→(2) 
where the label above each arrow indicates the rule used for each rewrite step.
As another example, the computation of 2⋅2 looks like this:
→sa
where the last step involves the calculations from the previous example.
In linguistics, phrase structure rules, also called rewrite rules, are used in some systems of generative grammar [ 8 ] as a means of generating grammatically correct sentences of a language. Such a rule usually has the form 
, where A is the label of a syntactic category, for example, a noun phrase or a sentence, and X is a sequence of such labels or morphemes, expressing the fact that A can be replaced by X when forming the structure of the sentence. For example, the rule 
means that a sentence may consist of a noun phrase (NP) followed by a verb phrase (VP); further rules will specify what subcomponents the noun phrase and verb phrase may consist of, and so on.
From the examples given above, it is clear that we can consider rewriting systems abstractly. We need to specify a set of objects and rules that can be applied to transform them. The most general (one-dimensional) realization of this concept is called an abstract reduction system [ 9 ] or an abstract rewriting system (abbreviated ARS). [ 10 ] An ARS is simply a set A of objects together with a binary relation → on A, called the reduction relation, the rewriting relation [ 11 ], or simply the reduction. [ 9 ]
Many concepts and notations can be defined in the general ARS setting. →∗
is the reflexive transitive closure of →
. ↔
is the symmetric closure of →. ↔∗
is the reflexive transitive symmetric closure of →. The word problem for an ARS consists in determining, for given x and y, whether x↔∗y
. An object x in A is called reducible if there exists some other y in A such that x→y
; otherwise it is called irreducible or a normal form. An object y is called "a normal form of x" if x→∗y
, and y is irreducible. If the normal form of x is unique, this is usually denoted x↓
. If every object has at least one normal form, the ARS is called normalizing. x↓y
, or x and y are said to be joinable, if there exists some z with the property that 
. An ARS is said to have the Church-Rosser property if x↔∗y implies x↓y. An ARS is confluent if for all w, x and y in A, 
implies x↓y. An ARS is locally confluent if and only if for all w, x and y in A, x←w→y
implies x↓y
. An ARS is called terminating or Noetherian if there is no infinite chain 
. A confluent and terminating ARS is called convergent or canonical.
Important theorems for abstract rewriting systems are that an ARS is confluent if and only if it has the Church-Rosser property, Newman's lemma (a terminating ARS is confluent if and only if it is locally confluent), and that the word problem for an ARS is in general undecidable.
A string rewriting system (SRS), also known as a semi-Thue system, uses the free monoid structure of strings (words) over an alphabet to extend a rewriting relation, R
, to all strings in the alphabet that contain the left- and right-hand sides of some rules as substrings. Formally, a semi-Thue system is a pair (Σ,R)
where Σ
is a (usually finite) alphabet, and R is a binary relation between certain (fixed) strings in the alphabet, called the set of rewrite rules. The one-step rewriting relation →R
induced by R on Σ∗
is defined as follows: if s, t
are some strings, then 
if there exist 
such that 
, 
, and uRv
. Since →R is a relation on Σ∗, the pair (Σ∗,→R)
fits the definition of an abstract rewriting system. Since the empty string is in , R is a subset of →R. If the relation R is symmetric, the system is called a Thue system.
In an SRS, the reduction relation 
is compatible with the monoid operation, meaning that x→R∗y
implies uxv→R∗uyv
for all strings x,y,u,v∈Σ∗. Similarly, the reflexive transitive symmetric closure of , denoted 
, is a congruence, that is, an equivalence relation (by definition), and is also compatible with string concatenation. The relation ↔R∗ is called the Thue congruence generated by . In a Thue system, i.e. if R is symmetric, the rewriting relation →R∗ coincides with the Thue congruence ↔R∗.
The notion of a semi-Thue system essentially coincides with a monoid presentation. Since ↔R∗ is a congruence, we can define the quotient monoid MR=Σ∗/↔R∗
of the free monoid Σ∗ with respect to Thue. If the monoid 
M is isomorphic to 
, then the semi-Thue system (Σ,R) is called a monoid presentation of M.
We immediately find very useful connections with other branches of algebra. For example, with the alphabet 
and the rules 
, where ε
is the empty string, this is a presentation of the free group on one generator. If instead the rules are simply 
, then we obtain a presentation of the bicyclic monoid. Thus, semi-Thue systems provide a natural foundation for solving the word problem for monoids and groups. In fact, every monoid has a presentation of the form (Σ,R), that is, it can always be represented by a semi-Thue system, possibly over an infinite alphabet.
The word problem for a semi-Thue system is in general undecidable; this result is sometimes called the Post-Markov theorem. [ 12 ]
Fig.1: Schematic triangle diagram of the application of the rewrite rule 
at position p
in the term, with the corresponding substitution σ
Fig.2: Left-hand-side term rule 
matched within the term 
A term rewriting system (TRS) — is a rewriting system whose objects are terms, that is, expressions with nested subexpressions. For example, the system shown above in the «Logic» section is a term rewriting system. The terms in this system consist of the binary operators (∨)
and (∧)
and the unary operator (¬)
. The rules also contain variables, which represent any possible term (although one variable always represents the same term within a single rule).
Unlike string rewriting systems, whose objects are sequences of symbols, the objects of a term rewriting system form a term algebra. A term can be represented as a tree of symbols, with the set of allowed symbols fixed by a given signature. As a formalism, term rewriting systems have all the power of Turing machines, that is, every computable function can be defined by a term rewriting system. [ 13 ]
Some programming languages are based on term rewriting. One such example is Pure, a functional programming language for mathematical applications.
A rewrite rule is a pair of terms, usually written as l→r
, to indicate that the left-hand side l can be replaced by the right-hand side r. A term rewriting system is a set R of such rules. A rule l→r can be applied to a term s if the left-hand term l matches some subterm of s, that is, if there is some substitution σ such that the subterm of s
rooted at some position p is the result of applying the substitution σ to the term l. The subterm corresponding to the left-hand side of the rule is called the redex, or reducible expression. [ 16 ] The resulting term t of applying this rule is the result of replacing the subterm at position p in s with the term r
to which the substitution σ has been applied, see figure 1. In this case, s is said to be rewritten in one step, or rewritten directly, to t
by the system R, formally denoted as s→Rt
, s→Rt, or as s→Rt
by some authors.
If a term t1
can be rewritten in several steps to a term tn
, that is, if t1→Rt2→R⋯→Rtn
, the term t1 is said to rewrite to tn, formally denoted as t1→R+tn
. In other words, the relation →R+
is the transitive closure of the relation →R; the notation →R∗ is also often used to denote the reflexive-transitive closure of →R, that is, 
if s=t
or s→R+t
Term rewriting given by a set R of rules can be regarded as an abstract rewriting system, as defined above, with terms as its objects and →R as its rewriting relation.
For example, 
is a rewrite rule commonly used to establish normal form with respect to the associativity of ∗
This rule can be applied to the numerator in the term with the corresponding substitution 
, see figure 2. Applying this substitution to the right-hand side of the rule gives the term 
, and replacing the numerator with this term gives 
, which is the result of applying the rewrite rule. In general, applying the rewrite rule achieved what is called «applying the law of associativity to "in elementary algebra. Alternatively, the rule could have been applied to the denominator of the original term, giving 
.
Questions of termination of rewriting systems in general are discussed in the section «Abstract rewriting system#Termination and convergence» . For term rewriting systems in particular, the following additional subtleties should be considered.
Termination is undecidable even for a system consisting of a single rule with a linear left-hand side. Termination is also undecidable for systems using only unary function symbols; however, it is decidable for finite ground systems.
The following term rewriting system is normalizing, but not terminating, and not confluent: 
The following two examples of term rewriting systems are due to Toyama:
and
g(x,y)→x,
g(x,y)→y.
Their union is a system that is not terminating, since
This result refutes a conjecture of Dershowitz [ 23 ] , who claimed that the union of two term rewriting systems R1
and R2
again terminates if all left-hand sides of R1 and right-hand sides of R2 are linear, and there are no « overlaps » between the left-hand sides of R1 and right-hand sides of R2Toyama's examples satisfy all of these properties.
See the sections Rewrite order and Path order (term rewriting) for information on the ordering relations used in termination proofs for term rewriting systems.
Higher-order rewriting systems are a generalization of first-order term rewriting systems to lambda terms, allowing the use of higher-order functions and bound variables. Various results about first-order TRSs can also be reformulated for HRSs. [ 25 ]
Graph rewriting systems are another generalization of term rewriting systems, operating on graphs instead of (ground) terms / their corresponding tree representation.
Trace theory provides a means for discussing multiprocessing in more formal terms, for example, through the trace monoid and the history monoid. Rewriting can also be carried out in trace systems.
Although the concept of rewriting was originally introduced for the lambda calculus, the main body of results and applications today concerns first-order rewriting. Rewriting systems of this kind are called Term Rewriting Systems, or TRS.
Higher-order rewriting systems are a generalization of first-order term rewriting systems to lambda terms, allowing higher-order functions and bound variables. Various results about first-order term rewriting systems can also be reformulated for higher orders.[
Comments