Newman's lemma

Newman's lemma

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 to a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.[1]

An earlier proof of the theorem was given by Church and Rosser.


Contents

Notes

  1. ^ Harrison, p. 260, Paterson(1990), p. 354.

References

  • M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223--243, 1942.
  • 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.
  • Paterson, Michael S. (1990). Automata, languages, and programming: 17th international colloquium. Lecture notes in computer science. 443. Warwick University, England: Springer. ISBN 9783540528265. 
  • A. Church and J. B. Rosser, Some properties of conversion, Transactions of the American Mathematical Society, 39(3), 1936.

Textbooks

  • Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
  • Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
  • John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 9780521899574, chapter 4 "Equality".

External links


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Max Newman — on a mountain in North Wales, ca. 1950 Born 7 February 1897(1897 02 07) 54 Lamont Road …   Wikipedia

  • Diamond Lemma — In der theoretischen Informatik besagt das Diamond Lemma (auch: der Satz von Newman, nach Max Newman), dass eine fundierte Relation genau dann konfluent ist, wenn sie lokal konfluent ist. Dieses Resultat ist die Grundlage zur Entscheidbarkeit der …   Deutsch Wikipedia

  • Satz von Newman — In der theoretischen Informatik besagt das Diamond Lemma (auch: der Satz von Newman, nach Max Newman), dass eine fundierte Relation genau dann konfluent ist, wenn sie lokal konfluent ist. Dieses Resultat ist die Grundlage zur Entscheidbarkeit der …   Deutsch Wikipedia

  • List of mathematics articles (N) — NOTOC N N body problem N category N category number N connected space N dimensional sequential move puzzles N dimensional space N huge cardinal N jet N Mahlo cardinal N monoid N player game N set N skeleton N sphere N! conjecture Nabla symbol… …   Wikipedia

  • List of lemmas — This following is a list of lemmas (or, lemmata , i.e. minor theorems, or sometimes intermediate technical results factored out of proofs). See also list of axioms, list of theorems and list of conjectures. 0 to 9 *0/1 Sorting Lemma ( comparison… …   Wikipedia

  • Knuth-Bendix completion algorithm — The Knuth Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it has effectively solved the word problem for the specified algebra. An… …   Wikipedia

  • Normal form (term rewriting) — In considering rewriting systems, a normal form is an element of the system which cannot be rewritten any further. Consider the basic term rewriting system with reduction rule ρ : g ( x , y ) → x . The term g ( g (4, 2), g (3, 1)) has the… …   Wikipedia

  • Normal form (abstract rewriting) — In abstract rewriting, a normal form is an element of the system which cannot be rewritten any further. Stated formally, for some reduction relation ⋅ → ⋅ over X a term t in X is a normal form if there does not exist a term t′ in X such …   Wikipedia

  • Abstract rewriting system — In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviation ARS) is a formalism that captures the quintessential notion and properties of… …   Wikipedia

  • Confluence (term rewriting) — Confluence is a property of term rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. Motivating example Consider the rules of regular arithmetic. We can think of these rules as… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”