Newman's lemma
From Wikipedia, the free encyclopedia
In the theory of term rewriting systems, Newman's lemma states that a strongly normalizing (or terminating) term rewriting system, that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent.
This is in fact a purely combinatorial result based on well-foundedness, that for a noetherian relation, local confluence implies confluence.
[edit] Reference
- M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223--243, 1942.
