Normal form (abstract rewriting): Difference between revisions
Matthiaspaul (talk | contribs) →Notes: +See also |
Matthiaspaul (talk | contribs) CE |
||
| Line 1: | Line 1: | ||
<!---hope to have achieved it: {{Cleanup|date=August 2009}}---> |
|||
In [[abstract rewriting]], an object is in '''normal form''' if it cannot be rewritten any further. Depending on the rewriting system and the object, several normal forms may exist, or none at all. |
In [[abstract rewriting]], an object is in '''normal form''' if it cannot be rewritten any further. Depending on the rewriting system and the object, several normal forms may exist, or none at all. |
||
| Line 5: | Line 4: | ||
Stated formally, if (''A'',→) is an [[Abstract rewriting system#Definition|abstract rewriting system]], some ''x''∈''A'' is in '''normal form''' if no ''y''∈''A'' exists such that ''x''→''y''. |
Stated formally, if (''A'',→) is an [[Abstract rewriting system#Definition|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 <ref group=note> |
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 <ref group="note">Each occurrence of ''g'' where the rule is applied is highlighted in '''boldface'''.</ref> of ''g'': |
||
:'''''g'''''(''g''(4,2),''g''(3,1)) → '''''g'''''(4,2) → 4. |
:'''''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. |
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. |
||
| Line 17: | Line 16: | ||
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. |
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, |
In contrast, the two-rule system { ''g''(''x'',''y'')→''x'', ''g''(''x'',''x'')→''g''(3,''x'') } is weakly, |
||
<ref group=note> |
<ref group="note">Since every term containing ''g'' can be rewritten by a finite number of applications of the first rule to a term without any ''g'', which is in normal form.</ref> |
||
but not strongly |
but not strongly |
||
<ref group=note> |
<ref group="note">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. |
||
| ⚫ | |||
normalizing, although each term not containing ''g''(3,3) is strongly normalizing. |
|||
| ⚫ | |||
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 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]]. |
||
| Line 28: | Line 25: | ||
==Normalization and confluency== |
==Normalization and confluency== |
||
[[Newman's lemma]] states that if an [[abstract rewriting 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]]. |
[[Newman's lemma]] states that if an [[abstract rewriting 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 |
The result enables to further generalize the [[critical pair lemma]].{{clarify|reason=Explicitly state and justify the thus generalized lemma, or omit this sentence.|date=June 2013}} |
||
== See also == |
== See also == |
||
Revision as of 18:07, 4 July 2017
In abstract rewriting, an object is in normal form if it 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 [note 1] 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 to 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 to 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, [note 2] but not strongly [note 3] normalizing, although each term not containing g(3,3) is strongly normalizing. [note 4] 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.
Another example: The single-rule system { r(x,y)→r(y,x) } has no normalizing properties (not weakly or strongly), since from any term, e.g. r(4,2) a single rewrite sequence starts, viz. r(4,2)→r(2,4)→r(4,2)→r(2,4)→..., which is infinitely long.
Normalization and confluency
Newman's lemma states that if an abstract rewriting system A is strongly normalizing and is weakly confluent, then A is confluent.
The result enables to further generalize the critical pair lemma.[clarification needed]
See also
Notes
- ^ Each occurrence of g where the rule is applied is highlighted in boldface.
- ^ Since every term containing g can be rewritten by a finite number of applications 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.
References
- Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press.
{{cite book}}: Invalid|ref=harv(help)