Term Rewriting Systems
Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, Samuel Mimram
Abstract
The study of universal algebra, that is, the description of algebraic structures by means of symbolic expressions subject to equations, dates back to the end of the 19th century. It was motivated by the large number of fundamental mathematical structures fitting into this framework: groups, rings, lattices, and so on. From the 1970s on, the algorithmic aspect became prominent and led to the notion of term rewriting system. This chapter briefly revisits these ideas from a polygraphic viewpoint, introducing only what is strictly necessary for understanding. Term rewriting systems are introduced as presentations of Lawvere theories, which are particular cartesian categories. It is shown that a term rewriting system can also be described by a 3-polygraph in which variables are handled explicitly, i.e., by taking into account their duplication and erasure. Finally, a precise meaning is given to the statement that term rewriting systems are "cartesian polygraphs".