Termination of 3-Polygraphs
Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, Samuel Mimram · Cambridge University Press eBooks · 2025
This chapter presents techniques for proving the termination of 3-polygraphs. A first method is based on a certain type of well-founded orders called reduction orders. Attention then turns to functorial interpretations: these amount to construct a functor from the underlying category to another category which already bears a reduction order. This covers quite a few useful examples. To address more complex cases, a powerful technique, due to Guiraud, is presented, based on the construction of a derivation from the polygraph. Here, termination is obtained by specifying quantities on 2-cells which decrease during rewriting, based on information propagated by the 2-cells themselves.