In the theory of rewriting systems, Newman's 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 it is confluent precisely when it is locally confluent. Today, this is seen as a purely combinatorial result based on well-foundedness due a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.

PropertyValue
dbpprop:abstract
  • In the theory of rewriting systems, Newman's 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 it is confluent precisely when it is locally confluent. Today, this is seen as a purely combinatorial result based on well-foundedness due a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.
  • In der theoretischen Informatik besagt das Diamond Lemma, dass eine fundierte Relation genau dann konfluent ist, wenn sie lokal konfluent ist. Dieses Resultat ist die Grundlage zur Entscheidbarkeit der Konfluenz bei terminierenden Termersetzungssystemen. Da das Diagramm im Beweis dieses Satzes entfernt an einen Diamanten erinnert, hat er diesen Namen bekommen.
  • O lema de Newman é uma propriedade sobre sistemas de redução abstratos utilizada para mostrar a confluência de tais sistemas.
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • In the theory of rewriting systems, Newman's 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 it is confluent precisely when it is locally confluent. Today, this is seen as a purely combinatorial result based on well-foundedness due a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.
  • In der theoretischen Informatik besagt das Diamond Lemma, dass eine fundierte Relation genau dann konfluent ist, wenn sie lokal konfluent ist. Dieses Resultat ist die Grundlage zur Entscheidbarkeit der Konfluenz bei terminierenden Termersetzungssystemen. Da das Diagramm im Beweis dieses Satzes entfernt an einen Diamanten erinnert, hat er diesen Namen bekommen.
  • O lema de Newman é uma propriedade sobre sistemas de redução abstratos utilizada para mostrar a confluência de tais sistemas.
rdfs:label
  • Newman's lemma
  • Diamond Lemma
  • Lema de Newman
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of