Normal form (abstract rewriting): Difference between revisions

Content deleted Content added

Inline

Revision as of 14:15, 30 June 2013

In abstract rewriting, an object is in normal form if cannot be rewritten any further. Depending on the rewriting system and the object, several normal forms may exist, or none at all.

Definition

Stated formally, if (A,→) is an abstract rewriting system, some x∈A is in normal form if no y∈A exists such that x→y.

For example, using the term rewriting system with a single rule g(x,y)→x, the term g(g(4,2),g(3,1)) can be rewritten as follows, applying the rule to the outermost occurrence of g:

g(g(4,2),g(3,1)) → g(4,2) → 4.

Since no rule applies to the last term, 4, it cannot be rewritten any further, and hence is a normal form of the term g(g(4,2),g(3,1)) with respect to this term rewriting system.

Normalization properties

Related concepts refer to the possibility of rewriting an element into normal form. An object of an abstract rewrite system is said be weakly normalizing, if it can be rewritten somehow into a normal form, that is, if some rewrite sequence starting from it cannot be extended any further. An object is said to be strongly normalizing, if it can be rewritten in any way into a normal form, that is, if every rewrite sequence starting from it eventually cannot be extended any further. An abstract rewrite system is said be weakly and strongly normalizing, or to have the weak and the strong normalization property, if each of its objects is weakly and strongly normalizing, respectively.

For example, the above single-rule system is strongly normalizing, since each rule application properly decreases term size and hence there cannot be an infinite rewrite sequence starting from any term. In contrast, the two-rule system { g(x,y)→x, g(x,x)→g(3,x) } is weakly, ^[1] but not strongly ^[2] normalizing, although each term not containing g(3,3) is strongly normalizing. ^[3] The term g(4,4) has two normal forms in this system, viz. g(4,4) → 4 and g(4,4) → g(3,4) → 3, hence the system is not confluent. The single-rule system g(x,y)→g(y,x) is not weakly (and hence not strongly) normalizing, since e.g. from the term g(4,2) a single rewrite sequence starts, viz. g(4,2)→g(2,4)→'g(4,2)→g(2,4)→..., which is infinitely long.

Newman's lemma states that if an abstract reduction system A is strongly normalizing and is weakly confluent, then A is confluent.

The result enables us to further generalize the critical pair lemma.^{[clarification needed]}

References

Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. {{cite book}}: Invalid |ref=harv (help)

^ since every term containing g can be rewritten by a finite number of appliations of the first rule to a term without any g, which is in normal form
^ since to the term g(3,3), the second rule can be applied over and over again, without reaching any normal form
^ For a given term, let m and n denote the total number of g and of g applied to identical arguments, respectively. Application of any rule properly decreases the value of m+n, which is possible only finitely many times.

P ≟ NP

This theoretical computer science–related article is a stub. You can help Wikipedia by expanding it.

[1] since every term containing g can be rewritten by a finite number of appliations of the first rule to a term without any g, which is in normal form

[2] since to the term g(3,3), the second rule can be applied over and over again, without reaching any normal form

[3] For a given term, let m and n denote the total number of g and of g applied to identical arguments, respectively. Application of any rule properly decreases the value of m+n, which is possible only finitely many times.

[1]

[2]

[3]

@@ Line 1: / Line 1: @@
-{{Cleanup|date=August 2009}}
+<!---hope to have achieved it: {{Cleanup|date=August 2009}}--->
-In [[abstract rewriting]], a '''normal form''' is an element of the system which cannot be reduced by rewriting any further. Stated formally, for some [[reduction relation]] &sdot;&nbsp;&rarr;&nbsp;&sdot; over ''X'' a term ''t'' in ''X'' is a normal form if there does not exist a term ''t''&prime; in ''X'' such that ''t'' &rarr; ''t''&prime;.
+In [[abstract rewriting]], an object is in '''normal form''' if cannot be rewritten any further. Depending on the rewriting system and the object, several normal forms may exist, or none at all.
+==Definition==
-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 (term rewriting)|strategy]], that is, if the reduction rule is applied to each outermost occurrence of ''g'':
+Stated formally, if (''A'',&rarr;) is an [[Abstract_rewriting_system#Definition|abstract rewriting system]], some ''x''∈''A'' is in '''normal form''' if no ''y''∈''A'' exists such that ''x''&rarr;''y''.
-: <math> g(g(4,2), g(3,1)) \rightarrow_\rho g(4,2) \rightarrow_\rho 4.</math>
-There is no rule that permits us to rewrite 4, so 4 is a normal form for this term rewriting system.
+For example, using the term rewriting system with a single rule ''g''(''x'',''y'')→''x'', the term ''g''(''g''(4,2),''g''(3,1)) can be rewritten as follows, applying the rule to the outermost occurrence of ''g'':
-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).
+:''g''(''g''(4,2),''g''(3,1)) → ''g''(4,2) → 4.
+Since no rule applies to the last term, 4, it cannot be rewritten any further, and hence is a normal form of the term ''g''(''g''(4,2),''g''(3,1)) with respect to this term rewriting system.
+==Normalization properties==
-[[Newman's lemma]] states that if an [[abstract reduction system]] ''A'' is strongly normalizing and is [[confluence (term rewriting)|weakly confluent]], then ''A'' is in fact confluent. The result enables us to further generalize the [[critical pair lemma]].
+Related concepts refer to the possibility of rewriting an element into normal form.
+An object of an abstract rewrite system is said be '''weakly normalizing''', if it can be rewritten ''somehow'' into a normal form, that is, if ''some'' rewrite sequence starting from it cannot be extended any further.
+An object is said to be '''strongly normalizing''', if it can be rewritten ''in any way'' into a normal form, that is, if every rewrite sequence starting from it eventually cannot be extended any further.
+An abstract rewrite system is said be '''weakly''' and '''strongly normalizing''', or to have the '''weak''' and the '''strong normalization''' property, if each of its objects is weakly and strongly normalizing, respectively.
+For example, the above single-rule system is strongly normalizing, since each rule application properly decreases term size and hence there cannot be an infinite rewrite sequence starting from any term.
+In contrast, the two-rule system { ''g''(''x'',''y'')→''x'', ''g''(''x'',''x'')→''g''(3,''x'') } is weakly,
+<ref>since every term containing ''g'' can be rewritten by a finite number of appliations of the first rule to a term without any ''g'', which is in normal form</ref>
+but not strongly
+<ref>since to the term ''g''(3,3), the second rule can be applied over and over again, without reaching any normal form</ref>
+normalizing, although each term not containing ''g''(3,3) is strongly normalizing.
+<ref>For a given term, let ''m'' and ''n'' denote the total number of ''g'' and of ''g'' applied to identical arguments, respectively.
+Application of any rule properly decreases the value of ''m''+''n'', which is possible only finitely many times.</ref>
+The term ''g''(4,4) has two normal forms in this system, viz. ''g''(4,4) → 4 and ''g''(4,4) → ''g''(3,4) → 3, hence the system is not [[confluence (term rewriting)#General case and theory|confluent]].
+The single-rule system ''g''(''x'',''y'')→''g''(''y'',''x'') is not weakly (and hence not strongly) normalizing, since e.g. from the term ''g''(4,2) a single rewrite sequence starts, viz. ''g''(4,2)→''g''(2,4)→'g''(4,2)→''g''(2,4)→..., which is infinitely long.
+[[Newman's lemma]] states that if an [[abstract reduction system]] ''A'' is strongly normalizing and is [[confluence (term rewriting)#Local confluence|weakly confluent]], then ''A'' is  [[confluence (term rewriting)#General case and theory|confluent]].
+The result enables us to further generalize the [[critical pair lemma]].{{clarify|reason=Explicitly state and justify the thus generalized lemma, or omit this sentence.}}
 ==References==
 * {{cite book|first1=Franz|last1=Baader|authorlink1=Franz Baader|first2=Tobias|last2=Nipkow|authorlink2=Tobias Nipkow|title=Term Rewriting and All That|year=1998|publisher=Cambridge University Press|ref=harv}}
+{{reflist}}
 {{DEFAULTSORT:Normal Form (Term Rewriting)}}