Two-Dimensional Rewriting

摘要

The notion of higher dimensional equational reasoning has been introduced by Albert Burroni (see [Bur93]). It is a natural generalization of the equational rea-soning with ordinary words. In the two-dimensional case, the latter are replaced by two-dimensional words, which are pictured as planar diagrams. In fact, the two-dimensional equational reasoning is already used, for instance in theoretical physics (Penrose diagrams) and in topology (knot diagrams). Also, Burroni noticed that the equational reasoning with terms can be seen as a special case of two-dimensional equational reasoning. This rests on the fact that the strict monoidal category of fi-nite sets has a finite (two-dimensional) presentation by means of the 3 generators of figure 1 and the 7 equations of figure 2 (see [Laf95] and [Mas97]). Of course, it is not necessary to know about category theory to understand those intuitive equations!