Abstract rewriting system
In its simplest form, an ARS is simply a set (of "objects") together with a binary relation, traditionally denoted with
; this definition can be further refined if we index (label) subsets of the binary relation.
Despite its simplicity, an ARS is sufficient to describe important properties of rewriting systems like normal forms, termination, and various notions of confluence.
Historically, there have been several formalizations of rewriting in an abstract setting, each with its idiosyncrasies.
This is due in part to the fact that some notions are equivalent, see below in this article.
The formalization that is most commonly encountered in monographs and textbooks, and which is generally followed here, is due to Gérard Huet (1980).
[1] An abstract reduction system (ARS) is the most general (unidimensional) notion about specifying a set of objects and rules that can be applied to transform them.
More recently, authors use the term abstract rewriting system as well.
[2] (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.
[3] This (entrenched) terminology using "reduction" is a little misleading, because the relation is not necessarily reducing some measure of the objects.
In some contexts it may be beneficial to distinguish between some subsets of the rules, i.e. some subsets of the reduction relation →, e.g. the entire reduction relation may consist of associativity and commutativity rules.
As a mathematical object, an ARS is exactly the same as an unlabeled state transition system, and if the relation is considered as an indexed union, then an ARS is the same as a labeled state transition system with the indices being the labels.
In a state transition system one is interested in interpreting the labels as actions, whereas in an ARS the focus is on how objects may be transformed (rewritten) into others.
From this definition, it's apparent one may define the joinability relation as
, but in this notation the down arrow is a binary relation, i.e. we write
for all objects x, y. Equivalently, the Church–Rosser property means that the reflexive transitive symmetric closure is contained in the joinability relation.
[7] In an ARS with the Church–Rosser property the word problem may be reduced to the search for a common successor.
The existence of these equivalent properties allows one to prove that a system is Church–Rosser with less work.
Furthermore, the notions of confluence can be defined as properties of a particular object, something that's not possible for Church–Rosser.
For an ARS the following three conditions are equivalent: (i) it has the Church–Rosser property, (ii) it is confluent, (iii) it is semi-confluent.
then Because of these equivalences, a fair bit of variation in definitions is encountered in the literature.
For instance, in Terese 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.
[10] 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 the common one given here in a confluent system, but it is more inclusive in a non-confluent ARS.
An abstract rewriting system is said to be terminating or noetherian if there is no infinite chain
In example 1 for instance, there is an infinite rewriting chain, namely
A confluent and terminating ARS is called canonical,[11] or convergent.
In a convergent ARS, every object has a unique normal form.
The original 1942 proof of this result by Newman was rather complicated.
It wasn't until 1980 that Huet published a much simpler proof exploiting the fact that when
