A complete tour of completion methods

Prof. Jean-Pierre Jouannaud (LIAMA and Tsinghua University)

Completion has two incarnations: for computing a standard or Grobner base of a
polynomial ideal -and decide its membership-, or for computing a reduced
rewrite system for an equational theory -and decide its word problem. Both play
an important role for various programming applications.

We shall review the known completion algorithms designed over the years,
starting with Janet's algorithm in 1906, in a modern setting and compare
them. Buchberger's algorithm (1968) corresponds to the specialization of Knuth
and Bendix completion to ground equations (1969). Janet's algorithm has no
counterpart yet, but the one of the talk. Mora's algorithm appears as a
constructive version of Hironaka's theorem (1967) and relates to recent work of
the author generalizing Knuth and Bendix completion to non-terminating rewrite