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:
-
any rewrite system instantiating his theory induces a so-called 1-ra,
an axiomatically orthogonal rewrite system, entailing co-initial reductions have least upperbounds;
-
the rewrite system underlying any (non-erasing) syntactically orthogonal TRS instantiates his theory.