Polygraphs of finite derivation type

Understand

Craig Squier proved that, if a monoid can be presented by a finite convergent string rewriting system, then it satisfies the homological finiteness condition left-FP3.

• Using this result, he constructed finitely presentable monoids with a decidable word problem, but that cannot be presented by finite convergent rewriting systems.
• Later, he introduced the condition of finite derivation type, which is a homotopical finiteness property on the presentation complex associated to a monoid presentation.
• He showed that this condition is an invariant of finite presentations and he gave a constructive way to prove this finiteness property based on the computation of the critical branchings: being of finite derivation type is a necessary condition for a finitely presented monoid to admit a finite convergent presentation.