Multi-redexes and multi-treks induce residual systems

least upper bounds and left-cancellation up to homotopy

Residual theory in rewriting goes back to Church, Rosser and Newman at the end of the 1930s. We investigate an axiomatic approach to it developed in 2002 by Melliès. He gave four axioms (SD) self-destruction, (F) finiteness, (FD) finite developments, and (PERM) permutation, showing that they entail two key properties of reductions, namely having

  1. least upper bounds (lubs) and
  2. left-cancellation
These properties are shown hold up to the equivalence generated by identifying the legs of local confluence diagrams inducing the same residuation, which corresponds to Lévy's permutation equivalence. Melliès in fact presented two sets of axioms, one for redexes as in classical residual theory and another more general one for treks. We show his results factor through the theory of residual systems we introduced in 2000, in that any rewrite system satisfying the four axioms (for redexes or treks) can be enriched to a residual system such that 1. and 2. follow from the theory of residual systems. We exemplify the axioms are sufficient but not necessary.