nLab rewriting




Given an alphabet of letters and symbols (perhaps ‘typed’, so that certain symbols are declared to be ‘symbols for functions’, etc., e.g. ‘++’ is a symbol for a binary operation), then one can form strings of letters to give words or more generally (well formed) formulae involving symbols of all types.

In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. On some formulae of a rewriting system, the rewriting rules may produce conflicts, when two or more rules can be applied.

Example type

One type of example of a rewriting system is given by a group presentation, (X,R)(X,R), where XX is a set of generators for a group GG and RR is a subset of pairs of elements in the free group on XX. As a definite example, take

  • X={a,b}X = \{a,b\}

  • R={(aaa,1),(bb,1),(abab,1)}R = \{(a a a,1),(b b,1),(a b a b,1)\}

(and the group being presented is the symmetric group, S 3S_3 on three symbols). We think of (aaa,1)(a a a,1) as a ‘rewrite rule’: ‘’replace aaaa a a by 1’’, often written aaa1a a a \rightsquigarrow 1 (or just aaa1a a a \to 1).

Working with the presentation, we can then start generating words in the generators, for instance aaababa a a b a b and then see how that word can be ‘rewritten’ using the rewrite rules to babb a b using the first rule and to aaa a using the last. There is thus a potential conflict between these rewritten forms of the word.

It is usual to choose a ‘normal form’ for each word. In the example, in the symmetric group and the above presentation the elements of the group are often listed as 1,a,a 2,b,ab,a 2b1, a, a^2, b, a b, a^2 b. These might be our choice of normal forms for the elements. In other words any element has a unique representative in the form a ib ja^i b^j, and we choose to label them that way. With the two uses of the rules applied to aaababa a a b a b, the first did not gave a normal form, the second did.

In order to transform a rewriting system into a computation algorithm, one needs to apply the rules in a deterministic way, using a reduction strategy. We also need to know that there is a unique normal form that can be found for each word and that the ‘algorithm’ will terminate, that is it really is an algorithm!.

We therefore will need to discuss confluence, normal form, termination and reduction strategies?.



  • Axel Thue, Probleme über Veränderungen von Zeichenreihen nach gegebenen Regeln., Kristiania Vidensk. Selsk, Skr. (1914), no. 10, 493–524.

  • Max H. A. Newman, On theories with a combinatorial definition of “equivalence”, Annals of Mathematics 43 2 (1942) 223-243 [doi:10.2307/1968867]

    (proves Newman's lemma)

  • Ronald V. Book, Friedrich Otto, String-rewriting systems, Texts and Monographs in Computer Science, Springer-Verlag, 1993.

  • Fabio Gadducci, On the algebraic approach to concurrent term rewriting, PhD thesis (1996) [pdf, pdf]

  • Franz Baader, Tobias Nipkow, Term rewriting and all that, Cambridge University Press (1998) [webpage]

  • Andrea Corradini, Fabio Gadducci, An algebraic presentation of term graphs, via gs-monoidal categories, Applied Categorical Structures 7 (1999) 299-331 [doi:10.1023/A:1008647417502]

    (introducing gs-monoidal categories for term rewriting)

  • Terese, Term rewriting systems, Cambridge Tracts in Theoretical Computer Science, vol. 55, Cambridge University Press, 2003.

See also:

On rewriting in group presentations:

Higher dimensional rewriting

For the higher dimensional forms of rewriting, one source is in the work of Guiraud and Malbos:

This also includes emerging homotopical theory of computation based on polygraphs (introduced by Albert Burroni) and polygraphic resolutions (introduced by François Métayer):

  • Yves Lafont, Algebra and geometry of rewriting, Applied Categorical Structures 15:4 (2007) 415–437 doi

Again within the context of higher dimensional forms of rewriting, Tibor Beke has given a categorification of certain rewriting procedures of Knuth. This is of relevance here as it contains a strong result on coherence theory:

An approach via diagrammatic sets is in

with slides (for GeoCat 2020), here.

See also:

  • Neil Ghani, C. Lüth, Rewriting via coinserters, Nordic Journal of Computing 10 (2003) 290–312 pdf

On the online proof assistant Globular for higher dimensional rewriting via semistrict globular higher categories:

See also:

Tracelets are the intrinsic carriers of causal information in categorical rewriting systems. In this work, we assemble tracelets into a symmetric monoidal decomposition space, inducing a cocommutative Hopf algebra of tracelets. This Hopf algebra captures important combinatorial and algebraic aspects of rewriting theory, and is motivated by applications of its representation theory to stochastic rewriting systems such as chemical reaction networks.

The following machine learning-inspired rewriting systems for meta/hyper-graphs claim to be related to homotopy type theory

  • Ben Goertzel, Reflective metagraph rewriting as a foundation for an AGI “Language of Thought”, arXiv:2112.08272
  • Xerxes D Arsiwalla, Jonathan Gorard, Pregeometric spaces from Wolfram model rewriting systems as homotopy types arXiv:2111.03460

Last revised on July 12, 2024 at 14:39:52. See the history of this page for a list of all contributions to it.