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 that t → t′.
Consider the basic term rewriting system with reduction rule ρ : g(x, y) → x. The term g(g(4, 2), g(3, 1)) has the following reduction sequence, according to the usual outermost strategy, that is, if the reduction rule is applied to each outermost occurrence of g:
There is no rule that permits us to rewrite 4, so 4 is a normal form for this term rewriting system.
Related concepts refer to the possibility of rewriting an element into normal form. Weak normalization means that some element can be rewritten into a normal form. Strong normalization means that any reduction sequence starting from some element terminates. We say that the system is weakly normalizing (or strongly normalizing) if all elements are weakly normalizing (resp. strongly normalizing).
Newman's lemma states that if an abstract reduction system A is strongly normalizing and is weakly confluent, then A is in fact confluent. The result enables us to further generalize the critical pair lemma.
Famous quotes containing the words normal and/or form:
“Dada doubts everything. Dada is an armadillo. Everything is Dada, too. Beware of Dada. Anti-dadaism is a disease: selfkleptomania, man’s normal condition, is Dada. But the real dadas are against Dada.”
—Tristan Tzara (1896–1963)
“For women who do not love us, as for the “disappeared”, knowing that we no longer have any hope does not prevent us form continuing to wait. We live on our guard, on watch; women whose son has gone asea on a dangerous exploration imagine at any minute, although it has long been certain that he has perished, that he will enter, miraculously saved, and healthy.”
—Marcel Proust (1871–1922)