Rewriting
Encyclopedia
In mathematics
, computer science
, and logic
, rewriting covers a wide range of (potentially non-deterministic) methods of replacing subterms of a formula with other terms. What is considered are rewriting systems (also known as rewrite systems or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable. Rewriting systems then do not provide an algorithm
for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer program
s, and several declarative programming languages are based on term rewriting.
, the procedure for determining the conjunctive normal form
(CNF) of a formula can be conveniently written as a rewriting system. The rules of such a system would be:
(double negative elimination
)
(De Morgan's laws)
(Distributivity
)
,
where the symbol (
) indicates that an expression matching the left side of the rule can be rewritten to one formed by the right side. In this system, we can perform a rewrite from left to right only when the logical interpretation of the left side entails
that of the right).
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.
; otherwise it is called irreducible or a normal form. An object y is called a normal form of x if 
, and y is irreducible. If x has a unique normal form, then this is usually denoted with 
. In example 1 above, c is a normal form, and 
. If every object has at least one normal form, the ARS is called normalizing.
A related, but weaker notion than the existence of normal forms is that of two objects being joinable: x and y are said joinable if there exists some z with the property that
. From this definition, it's apparent one may define the joinability relation as 
, where 
is the composition of relations
. Joinability is usually denoted, somewhat confusingly, also with
, but in this notation the down arrow is a binary relation, i.e. we write 
if x and y are joinable.
One of the important problems that may be formulated in an ARS is the word problem: given x and y are they equivalent under
? This is a very general setting for formulating the word problem for the presentation of an algebraic structure
. For instance, the word problem for groups
is a particular case of an ARS word problem. Central to an "easy" solution for the word problem is the existence of unique normal forms: in this case if two objects have the same normal form, then they are equivalent under
. The word problem for an ARS is undecidable
in general.
implies 
. In words, the Church-Rosser property means that the reflexive transitive symmetric closure is contained in the joinability relation. Alonzo Church
and J. Barkley Rosser proved in 1936 that lambda calculus
has this property; hence the name of the property. (The fact that lambda calculus has this property is also known as the Church-Rosser theorem.) In an ARS with the Church-Rosser property the word problem may be reduced to the search for a common successor. In a Church-Rosser system, an object has at most one normal form; that is the normal form of an object is unique if it exists, but it may well not exist.
Several different properties are equivalent to the Church-Rosser property, but may be simpler to check in any particular setting. In particular, confluence is equivalent to Church-Rosser. The notion of confluence can be defined for individual elements, something that's not possible for Church-Rosser. An ARS
is said:
Theorem. For an ARS the following conditions are equivalent: (i) it has the Church-Rosser property, (ii) it is confluent.
Corollary. In a confluent ARS if
then
Because of these equivalences, a fair bit of variation in definitions is encountered in the literature. For instance, in Bezem et al. 2003 the Church-Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church-Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate. Because of the above corollary, one may define a normal form y of x as an irreducible y with the property that
. This definition, found in Book and Otto, is equivalent to common one given here in a confluent system, but it is more inclusive in a non-confluent ARS.
Local confluence on the other hand is not equivalent with the other notions of confluence given in this section, but it is strictly weaker than confluence.
. In a terminating ARS, every object has at least one normal form, thus it is normalizing. The converse is not true. In example 1 for instance, there is an infinite rewriting chain, namely 
, even though the system is normalizing. A confluent and terminating ARS is called convergent. In a convergent ARS, every object has a unique normal form. But it is sufficient for the system to be confluent and normalizing for a unique normal to exist for every element, as seen in example 1.
Theorem (Newman's Lemma
): A terminating ARS is confluent if and only if it is locally confluent.
(words) over an alphabet to extend a rewriting relation, R to all strings in the alphabet that contain left- and respectively right-hand sides of some rules as substring
s. Formally a semi-Thue systems is a tuple
where 
is a (usually finite) alphabet, and R is a binary relation between some (fixed) strings in the alphabet, called rewrite rules. The one-step rewriting relation relation 
induced by R on 
is defined as: for any strings s, and t in 
if and only if there exist x, y, u, v in 
such that s = xuy, t = xvy, and u R v. Since 
is a relation on 
, the pair 
fits the definition of an abstract rewriting system. Obviously R is subset of 
. If the relation 
is symmetric
, then the system is called a Thue system.
In a SRS, the reduction relation
is compatible with the monoid operation, meaning that 
implies 
for all strings x, y, u, v in 
. Similarly, the reflexive transitive symmetric closure of 
, denoted 
, is a congruence
, meaning it is an equivalence relation
(by definition) and it is also compatible with string concatenation. The relation
is called the Thue congruence generated by R. In a Thue system, i.e. if R is symmetric, the rewrite relation 
coincides with the Thue congruence 
.
The notion of a semi-Thue system essentially coincides with the presentation of a monoid. Since
is a congruence, we can define the factor monoid 
of the free monoid 
by the Thue congruence in the usual manner. If a monoid 
is isomorphic with 
, then the semi-Thue system 
is called a monoid presentation of 
.
We immediately get some very useful connections with other areas of algebra. For example, the alphabet {a, b} with the rules { ab → ε, ba → ε }, where ε is the empty string
, is a presentation of the free group
on one generator. If instead the rules are just { ab → ε }, then we obtain a presentation of the bicyclic monoid. Thus semi-Thue systems constitute a natural framework for solving the word problem
for monoids and groups. In fact, every monoid has a presentation of the form
, i.e. it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.
The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the Post-Markov theorem.
, or expressions with nested sub-expressions. For example, the system shown under Logic above is a term rewriting system. The terms in this system are composed of binary operators
and 
and the unary operator 
. Also present in the rules are variables, which are part of the rules themselves rather than the term; these each represent any possible term (though a single variable always represents the same term throughout a single rule).
The term structure in such a system is usually presented using a grammar
. In contrast to string rewriting systems, whose objects are flat sequences of symbols, the objects of a term rewriting system form a term algebra
, which can be visualized as a tree of symbols, the structure of the tree fixed by the signature
used to define the terms.
The system given under Logic above is an example of a term rewriting system.
, operating on graphs instead of (ground-) terms
/ their corresponding tree
representation.
provides a means for discussing multiprocessing in more formal terms, such as via the trace monoid
and the history monoid
. Rewriting can be performed in trace systems as well.
provers.
s. The potential existence or uniqueness of normal forms can be used to classify and describe certain rewriting systems. There are rewriting systems which do not have normal forms: a trivial example is the rewriting system on two terms a and b with a → b, b → a.
The property exhibited above where terms can be rewritten regardless of the choice of rewriting rule to obtain the same normal form is known as confluence
. The property of confluence is linked with the property of having unique normal forms.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, rewriting covers a wide range of (potentially non-deterministic) methods of replacing subterms of a formula with other terms. What is considered are rewriting systems (also known as rewrite systems or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable. Rewriting systems then do not provide an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer program
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
s, and several declarative programming languages are based on term rewriting.
Logic
In logicLogic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, the procedure for determining the conjunctive normal form
Conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
(CNF) of a formula can be conveniently written as a rewriting system. The rules of such a system would be:
(double negative eliminationDouble negative elimination
In propositional logic, the inference rules double negative elimination allow deriving the double negative equivalent by adding or removing a pair of negation signs...
)
(De Morgan's laws) (DistributivityDistributivity
In mathematics, and in particular in abstract algebra, distributivity is a property of binary operations that generalizes the distributive law from elementary algebra.For example:...
)
,where the symbol (
) indicates that an expression matching the left side of the rule can be rewritten to one formed by the right side. In this system, we can perform a rewrite from left to right only when the logical interpretation of the left side entailsEntailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
that of the right).
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
Binary relation
In mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
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 closureTransitive closureIn mathematics, the transitive closure of a binary relation R on a set X is the transitive relation R+ on set X such that R+ contains R and R+ is minimal . If the binary relation itself is transitive, then the transitive closure will be that same binary relation; otherwise, the transitive closure...
of
, where = is the identity relation, i.e. 
is the smallest preorderPreorderIn mathematics, especially in order theory, preorders are binary relations that are reflexive and transitive.For example, all partial orders and equivalence relations are preorders...
(reflexiveReflexiveReflexive may refer to:In fiction:*MetafictionIn grammar:*Reflexive pronoun, a pronoun with a reflexive relationship with its self-identical antecedent*Reflexive verb, where a semantic agent and patient are the same...
and transitive relation) containing
. It is also called the reflexive transitive closure of 
. -
is 
, that is the union of the relation → with its inverse relationInverse relationIn mathematics, the inverse relation of a binary relation is the relation that occurs when you switch the order of the elements in the relation. For example, the inverse of the relation 'child of' is the relation 'parent of'...
, also known as the symmetric closureSymmetric closureIn mathematics, the symmetric closure of a binary relation R on a set X is the smallest symmetric relation on X that contains R....
of
. -
is the transitive closureTransitive closureIn mathematics, the transitive closure of a binary relation R on a set X is the transitive relation R+ on set X such that R+ contains R and R+ is minimal . If the binary relation itself is transitive, then the transitive closure will be that same binary relation; otherwise, the transitive closure...
of
, that is 
is the smallest equivalence relationEquivalence relationIn mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
containing
. It is also known as the reflexive transitive symmetric closure of 
.
Normal forms, joinability and the word problem
An object x in A is called reducible if there exist some other y in A and; otherwise it is called irreducible or a normal form. An object y is called a normal form of x if , and y is irreducible. If x has a unique normal form, then this is usually denoted with . In example 1 above, c is a normal form, and . If every object has at least one normal form, the ARS is called normalizing.A related, but weaker notion than the existence of normal forms is that of two objects being joinable: x and y are said joinable if there exists some z with the property that
. From this definition, it's apparent one may define the joinability relation as , where is the composition of relationsComposition of relations
In mathematics, the composition of binary relations is a concept of forming a new relation from two given relations R and S, having as its most well-known special case the composition of functions.- Definition :...
. Joinability is usually denoted, somewhat confusingly, also with
, but in this notation the down arrow is a binary relation, i.e. we write if x and y are joinable.One of the important problems that may be formulated in an ARS is the word problem: given x and y are they equivalent under
? This is a very general setting for formulating the word problem for the presentation of an algebraic structureWord problem (mathematics)
In mathematics and computer science, a word problem for a set S with respect to a system of finite encodings of its elements is the algorithmic problem of deciding whether two given representatives represent the same element of the set...
. For instance, the word problem for groups
Word problem for groups
In mathematics, especially in the area of abstract algebra known as combinatorial group theory, the word problem for a finitely generated group G is the algorithmic problem of deciding whether two words in the generators represent the same element...
is a particular case of an ARS word problem. Central to an "easy" solution for the word problem is the existence of unique normal forms: in this case if two objects have the same normal form, then they are equivalent under
. The word problem for an ARS is undecidableUndecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
in general.
The Church-Rosser property and confluence
An ARS is said to possess the Church-Rosser property if and only if implies . In words, the Church-Rosser property means that the reflexive transitive symmetric closure is contained in the joinability relation. Alonzo ChurchAlonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
and J. Barkley Rosser proved in 1936 that lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
has this property; hence the name of the property. (The fact that lambda calculus has this property is also known as the Church-Rosser theorem.) In an ARS with the Church-Rosser property the word problem may be reduced to the search for a common successor. In a Church-Rosser system, an object has at most one normal form; that is the normal form of an object is unique if it exists, but it may well not exist.
Several different properties are equivalent to the Church-Rosser property, but may be simpler to check in any particular setting. In particular, confluence is equivalent to Church-Rosser. The notion of confluence can be defined for individual elements, something that's not possible for Church-Rosser. An ARS
is said:- confluent if and only if for all w, x, and y in A,
implies 
. Roughly speaking, confluence says that no matter how two paths diverge from a common ancestor (w), the paths are joining at some common successor. This notion may be refined as property of a particular object w, and the system called confluent if all its elements are confluent. - locally confluent if and only if for all w, x, and y in A,
implies 
. This property is sometimes called weak confluence.
Theorem. For an ARS the following conditions are equivalent: (i) it has the Church-Rosser property, (ii) it is confluent.
Corollary. In a confluent ARS if
then
- If both x and y are normal forms, then x = y.
- If y is a normal form, then
Because of these equivalences, a fair bit of variation in definitions is encountered in the literature. For instance, in Bezem et al. 2003 the Church-Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church-Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate. Because of the above corollary, one may define a normal form y of x as an irreducible y with the property that
. This definition, found in Book and Otto, is equivalent to common one given here in a confluent system, but it is more inclusive in a non-confluent ARS.Local confluence on the other hand is not equivalent with the other notions of confluence given in this section, but it is strictly weaker than confluence.
Termination and convergence
An abstract rewriting system is said to be terminating or noetherian if there is no infinite chain. In a terminating ARS, every object has at least one normal form, thus it is normalizing. The converse is not true. In example 1 for instance, there is an infinite rewriting chain, namely , even though the system is normalizing. A confluent and terminating ARS is called convergent. In a convergent ARS, every object has a unique normal form. But it is sufficient for the system to be confluent and normalizing for a unique normal to exist for every element, as seen in example 1.Theorem (Newman's Lemma
Newman's lemma
In the theory of rewriting systems, Newman's lemma states that a terminating abstract rewriting system , that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent...
): A terminating ARS is confluent if and only if it is locally confluent.
String rewriting systems
A string rewriting system (SRS), also known as semi-Thue system, exploits the free monoid structure of the stringsString (computer science)
In formal languages, which are used in mathematical logic and theoretical computer science, a string is a finite sequence of symbols that are chosen from a set or alphabet....
(words) over an alphabet to extend a rewriting relation, R to all strings in the alphabet that contain left- and respectively right-hand sides of some rules as substring
Substring
A subsequence, substring, prefix or suffix of a string is a subset of the symbols in a string, where the order of the elements is preserved...
s. Formally a semi-Thue systems is a tuple
Tuple
In mathematics and computer science, a tuple is an ordered list of elements. In set theory, an n-tuple is a sequence of n elements, where n is a positive integer. There is also one 0-tuple, an empty sequence. An n-tuple is defined inductively using the construction of an ordered pair...
where is a (usually finite) alphabet, and R is a binary relation between some (fixed) strings in the alphabet, called rewrite rules. The one-step rewriting relation relation induced by R on is defined as: for any strings s, and t in if and only if there exist x, y, u, v in such that s = xuy, t = xvy, and u R v. Since is a relation on , the pair fits the definition of an abstract rewriting system. Obviously R is subset of . If the relation is symmetricSymmetric relation
In mathematics, a binary relation R over a set X is symmetric if it holds for all a and b in X that if a is related to b then b is related to a.In mathematical notation, this is:...
, then the system is called a Thue system.
In a SRS, the reduction relation
is compatible with the monoid operation, meaning that implies for all strings x, y, u, v in . Similarly, the reflexive transitive symmetric closure of , denoted , is a congruenceCongruence relation
In abstract algebra, a congruence relation is an equivalence relation on an algebraic structure that is compatible with the structure...
, meaning it is an equivalence relation
Equivalence relation
In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
(by definition) and it is also compatible with string concatenation. The relation
is called the Thue congruence generated by R. In a Thue system, i.e. if R is symmetric, the rewrite relation coincides with the Thue congruence .The notion of a semi-Thue system essentially coincides with the presentation of a monoid. Since
is a congruence, we can define the factor monoid of the free monoid by the Thue congruence in the usual manner. If a monoid is isomorphic with , then the semi-Thue system is called a monoid presentation of .We immediately get some very useful connections with other areas of algebra. For example, the alphabet {a, b} with the rules { ab → ε, ba → ε }, where ε is the empty string
Empty string
In computer science and formal language theory, the empty string is the unique string of length zero. It is denoted with λ or sometimes Λ or ε....
, is a presentation of the free group
Free group
In mathematics, a group G is called free if there is a subset S of G such that any element of G can be written in one and only one way as a product of finitely many elements of S and their inverses...
on one generator. If instead the rules are just { ab → ε }, then we obtain a presentation of the bicyclic monoid. Thus semi-Thue systems constitute a natural framework for solving the word problem
Word problem (mathematics)
In mathematics and computer science, a word problem for a set S with respect to a system of finite encodings of its elements is the algorithmic problem of deciding whether two given representatives represent the same element of the set...
for monoids and groups. In fact, every monoid has a presentation of the form
, i.e. it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the Post-Markov theorem.
Term rewriting systems
A term rewriting system (TRS) is a rewriting system where the objects are termsTerm (logic)
In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...
, or expressions with nested sub-expressions. For example, the system shown under Logic above is a term rewriting system. The terms in this system are composed of binary operators
and and the unary operator . Also present in the rules are variables, which are part of the rules themselves rather than the term; these each represent any possible term (though a single variable always represents the same term throughout a single rule).The term structure in such a system is usually presented using a grammar
Formal grammar
A formal grammar is a set of formation rules for strings in a formal language. The rules describe how to form strings from the language's alphabet that are valid according to the language's syntax...
. In contrast to string rewriting systems, whose objects are flat sequences of symbols, the objects of a term rewriting system form a term algebra
Term algebra
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
, which can be visualized as a tree of symbols, the structure of the tree fixed by the signature
Signature (logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...
used to define the terms.
The system given under Logic above is an example of a term rewriting system.
Graph rewriting systems
A generalization of term rewrite systems are graph rewrite systemsGraph rewriting
Graph transformation, or Graph rewriting, concerns the technique of creating a new graph out of an original graph using some automatic machine. It has numerous applications, ranging from software verification to layout algorithms....
, operating on graphs instead of (ground-) terms
Term (mathematics)
A term is a mathematical expression which may form a separable part of an equation, a series, or another expression.-Definition:In elementary mathematics, a term is either a single number or variable, or the product of several numbers or variables separated from another term by a + or - sign in an...
/ their corresponding tree
Tree (graph theory)
In mathematics, more specifically graph theory, a tree is an undirected graph in which any two vertices are connected by exactly one simple path. In other words, any connected graph without cycles is a tree...
representation.
Trace rewriting systems
Trace theoryTrace theory
In mathematics and computer science, trace theory aims to provide a concrete mathematical underpinning for the study of concurrent computation and process calculi...
provides a means for discussing multiprocessing in more formal terms, such as via the trace monoid
Trace monoid
In mathematics and computer science, a trace is a set of strings, wherein certain letters in the string are allowed to commute, but others are not. It generalizes the concept of a string, by not forcing the letters to always be in a fixed order, but allowing certain reshufflings to take place...
and the history monoid
History monoid
In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process...
. Rewriting can be performed in trace systems as well.
Philosophy
Rewriting systems can be seen as programs that infer end-effects from a list of cause-effect relationships. In this way, rewriting systems can be considered to be automated causalityCausality
Causality is the relationship between an event and a second event , where the second event is understood as a consequence of the first....
provers.
Properties of rewriting systems
Observe that in both of the above rewriting systems, it is possible to get terms rewritten to a "simplest" term, where this term cannot be modified any further from the rules in the rewriting system. Terms which cannot be written any further are called normal formNormal form (term rewriting)
In abstract rewriting, a normal form is an element of the system which cannot be rewritten any further. Stated formally, for some reduction relation ⋅ → ⋅ over X a term t in X is a normal form if there does not exist a term t′ in X such that t → t′.Consider...
s. The potential existence or uniqueness of normal forms can be used to classify and describe certain rewriting systems. There are rewriting systems which do not have normal forms: a trivial example is the rewriting system on two terms a and b with a → b, b → a.
The property exhibited above where terms can be rewritten regardless of the choice of rewriting rule to obtain the same normal form is known as confluence
Confluence (term rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.- Motivating example :Consider...
. The property of confluence is linked with the property of having unique normal forms.
See also
- Critical pair (logic)Critical pair (logic)In mathematical logic, a critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms.For example, in the term rewriting system with rules...
- Knuth-Bendix completion algorithmKnuth-Bendix completion algorithmThe Knuth–Bendix completion algorithm is an algorithm for transforming a set of equations into a confluent term rewriting system...
- L-systemL-systemAn L-system or Lindenmayer system is a parallel rewriting system, namely a variant of a formal grammar, most famously used to model the growth processes of plant development, but also able to model the morphology of a variety of organisms...
s specify re-writing that is done in parallel. - Regulated rewritingRegulated rewritingRegulated rewriting is a specific area of formal languages studying grammatical systems which are able to take some kind of control over the production applied in a derivation step. For this reason, the grammatical systems studied in Regulated Rewriting theory are also called "Grammars with...
- Rho calculusRho calculusThe rho-calculus is a formalism intended to combine the higher-order facilities of lambda calculus with the pattern matching of term rewriting.-External links:*...
Further reading
316 pages. A textbook suitable for undergraduates.- Marc Bezem, Jan Willem KlopJan Willem KlopJan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinatorwhere- External links :*...
, Roel de Vrijer ("Terese"), Term Rewriting Systems, Cambridge University Press, 2003, ISBN 0521391156. This is the most recent comprehensive monograph. It uses however a fair deal of non-yet-standard notations and definitions. For instance the Church-Rosser property is defined to be identical with confluence. - Ronald V. BookRonald V. BookRonald Vernon Book worked in theoretical computer science. He published more than 150 papers in scientific journals...
and Friedrich Otto, String-Rewriting Systems, Springer (1993). - Nachum Dershowitz and Jean-Pierre Jouannaud Rewrite Systems, Chapter 6 in Jan van LeeuwenJan van LeeuwenJan van Leeuwen is a Dutch computer scientist, a professor at the Department of Information and Computing Sciences at the Utrecht University....
(Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320. The preprintPreprintA preprint is a draft of a scientific paper that has not yet been published in a peer-reviewed scientific journal.-Role:Publication of manuscripts in a peer-reviewed journal often takes weeks, months or even years from the time of initial submission, because manuscripts must undergo extensive...
of this chapter is freely available from the authors, but it misses the figures.
External links
- The Rewriting Home Page
- IFIP Working Group 1.6
- Researchers in rewriting by Aart Middeldorp, University of Innsbruck
- Termination Portal