En mathématiques et en informatique, plus précisément dans la théorie des relations binaires, le lemme de Newman dit qu'une relation binaire noethérienne est confluente si elle est localement confluente[1]. Une démonstration relativement simple (induction sur une relation bien fondée) est due à Gérard Huet en 1980[2]. La démonstration originale de Newman est plus compliquée, mais la méthode des diagrammes décroissants[Quoi ?] montre bien comment elle fonctionne[3].
↑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.
↑Jan Willem Klop, Vincent van Oostrom, Roel C. de Vrijer, « A geometric proof of confluence by decreasing diagrams », J. Log. Comput. 10(3): 437-460 (2000).