In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.[1]
Equivalently, for every binary relation with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique minimal element in every connected component of the relation considered as a graph.
Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet in 1980.[2] Newman's original proof was considerably more complicated.[3]
- ^ Franz Baader, Tobias Nipkow, (1998) Term Rewriting and All That, Cambridge University Press ISBN 0-521-77920-0
- ^ Gérard Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems", Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797–821. https://doi.org/10.1145/322217.322230
- ^ Harrison, p. 260, Paterson (1990), p. 354.
© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search