Redeeming Newman; orthogonality in rewriting

Past, present and future in a 1-algebraic setting


Despite sixty percent of Newman's seminal 1942 paper being devoted to residual theory, that remains obscure due to that his instantiation of the theory there to the (non-erasing) λβ-calculus was fatally flawed. We redeem the approach showing:

  1. any rewrite system instantiating his theory induces a so-called 1-ra, an axiomatically orthogonal rewrite system, entailing co-initial reductions have least upperbounds;
  2. the rewrite system underlying any (non-erasing) syntactically orthogonal TRS instantiates his theory.