Editing Rewriting (section)

== Abstract rewriting systems ==
{{Main|Abstract rewriting system}}

From the above examples, it is 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''<ref name="Book and Otto, p. 10">Book and Otto, p. 10</ref> or ''abstract rewriting system'' (abbreviated ''ARS'').<ref>Bezem et al., p. 7,</ref> An ARS is simply a set ''A'' of objects, together with a [[binary relation]] → on ''A'' called the ''reduction relation'', ''rewrite relation''<ref>Bezem et al., p. 7</ref> or just ''reduction''.<ref name="Book and Otto, p. 10"/>

Many notions and notations can be defined in the general setting of an ARS. <math>\overset{*}\rightarrow</math> is the [[reflexive transitive closure]] of <math>\rightarrow</math>. <math>\leftrightarrow</math> is the [[symmetric closure]] of <math>\rightarrow</math>. <math>\overset{*}{\leftrightarrow}</math> is the [[reflexive transitive symmetric closure]] of <math>\rightarrow</math>. The [[Word problem (mathematics)|word problem]] for an ARS is determining, given ''x'' and ''y'', whether <math>x \overset{*}{\leftrightarrow} y</math>. An object ''x'' in ''A'' is called ''reducible'' if there exists some other ''y'' in ''A'' such that <math>x \rightarrow y</math>; otherwise it is called ''irreducible'' or a [[Normal form (abstract rewriting)|normal form]]. An object ''y'' is called a "normal form of ''x''" if <math>x \stackrel{*}{\rightarrow} y</math>, and ''y'' is irreducible. If the normal form of ''x'' is unique, then this is usually denoted with <math>x{\downarrow}</math>. If every object has at least one normal form, the ARS is called ''normalizing''. <math>x \downarrow y</math> or ''x'' and ''y'' are said to be ''joinable'' if there exists some ''z'' with the property that <math>x \overset{*}{\rightarrow} z \overset{*}{\leftarrow} y</math>. An ARS is said to possess the [[Church–Rosser property]] if <math>x \overset{*}{\leftrightarrow} y</math> implies <math>x \downarrow y</math>. An ARS is [[Confluence (abstract rewriting)|confluent]] if for all ''w'', ''x'', and ''y'' in ''A'',  <math>x \overset{*}{\leftarrow} w \overset{*}{\rightarrow} y</math> implies <math>x \downarrow y</math>. An ARS is ''locally confluent'' if and only if for all ''w'', ''x'', and ''y'' in ''A'',  <math>x \leftarrow w \rightarrow y</math> implies <math>x\mathbin\downarrow y</math>. An ARS is said to be ''terminating'' or ''noetherian'' if there is no infinite chain <math>x_0 \rightarrow x_1 \rightarrow x_2 \rightarrow \cdots</math>. A confluent and terminating ARS is called ''convergent'' or ''canonical''.

Important theorems for abstract rewriting systems are that an ARS is [[Confluence (abstract rewriting)|confluent]] [[iff]] 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 (mathematics)|word problem]] for an ARS is [[undecidable problem|undecidable]] in general.