Normal form (abstract rewriting): Difference between revisions

Content deleted Content added

Inline

Revision as of 01:49, 12 September 2021

In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all.

Definition

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

An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form. A rewrite system has the weak normalization property or is (weakly) normalizing (WN) if every object is weakly normalizing. An object a is strongly normalizing if every sequence of rewrites starting from a eventually terminates with an a normal form. An abstract rewrite system is strongly normalizing, terminating, noetherian, or has the (strong) normalization property, if each of its objects is strongly normalizing.^[1]

A rewriting system has the normal form property (NF) if for all objects a and normal forms b, b can be reached from a by a series of rewrites and inverse rewrites only if a reduces to b. A rewriting system has the unique normal form property (UN) if for all normal forms a, b ∈ S, a can be reached from b by a series of rewrites and inverse rewrites only if a is equal to b. A rewriting system has the unique normal form property with respect to reduction (UN^→) if for every term reducing to normal forms a and b, a is equal to b.^[2]

Results

Some well known results:

SN implies WN.^[3]
Confluence implies NF implies UN implies UN^→.^[2]
WN and UN imply confluence.^[4]

Examples

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. The 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.

Untyped lambda calculus

The pure untyped lambda calculus does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term $\lambda x.xxx$ . It has the following rewrite rule: For any term $t$ ,

(\mathbf {\lambda } x.xxx)t\rightarrow ttt

But consider what happens when we apply $\lambda x.xxx$ to itself:

{\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \ldots \,\end{aligned}}

Therefore the term $(\lambda x.xxx)(\lambda x.xxx)$ is neither strongly nor weakly normalizing.

Typed lambda calculus

Various systems of typed lambda calculus including the simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are strongly normalizing.

A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete, otherwise one could solve the halting problem by seeing if the program type-checks. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or System F), for example a self-interpreter.^[5]

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. ISBN 9780521779203.

^ Ohlebusch, Enno (1998). "Church-Rosser theorems for abstract reduction modulo an equivalence relation". Rewriting Techniques and Applications. 1379: 18. doi:10.1007/BFb0052358.
^ ^a ^b Klop, J.W.; de Vrijer, R.C. (February 1989). "Unique normal forms for lambda calculus with surjective pairing". Information and Computation. 80 (2): 97–113. doi:10.1016/0890-5401(89)90014-X.
^ "logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?". Computer Science Stack Exchange. Retrieved 12 September 2021.
^ Terese (20 March 2003). Term Rewriting Systems. Cambridge University Press. p. 17. ISBN 978-0-521-39115-3.
^ Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 June 2015). Genetic Programming Theory and Practice XII. Springer. p. 59. ISBN 978-3-319-16030-6. Retrieved 8 September 2021.

[5] Each occurrence of g where the rule is applied is highlighted in boldface.

[6] 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.

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

[8] 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] Ohlebusch, Enno (1998). "Church-Rosser theorems for abstract reduction modulo an equivalence relation". Rewriting Techniques and Applications. 1379: 18. doi:10.1007/BFb0052358.

[NF-2] Klop, J.W.; de Vrijer, R.C. (February 1989). "Unique normal forms for lambda calculus with surjective pairing". Information and Computation. 80 (2): 97–113. doi:10.1016/0890-5401(89)90014-X.

[3] "logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?". Computer Science Stack Exchange. Retrieved 12 September 2021.

[4] Terese (20 March 2003). Term Rewriting Systems. Cambridge University Press. p. 17. ISBN 978-0-521-39115-3.

[9] Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 June 2015). Genetic Programming Theory and Practice XII. Springer. p. 59. ISBN 978-3-319-16030-6. Retrieved 8 September 2021.

[1]

[2]

[3]

[4]

[note 1]

[note 2]

[note 3]

[note 4]

[5]

@@ Line 1: / Line 1: @@
-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, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all.
 ==Definition==
-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]], ''x''∈''A'' is in '''normal form''' if no ''y''∈''A'' exists such that ''x''→''y'', i.e. ''x'' is an irreducible term.
+An object ''a'' is ''weakly normalizing'' if there exists at least one particular sequence of rewrites starting from ''a'' that eventually yields a normal form. A rewrite system has the '''weak normalization property''' or is ''(weakly) normalizing'' (WN) if every object is weakly normalizing. An object ''a'' is ''strongly normalizing'' if every sequence of rewrites starting from ''a'' eventually terminates with an a normal form. An abstract rewrite system is ''strongly normalizing'', ''terminating'', ''noetherian'', or has the ''(strong) normalization property'', if each of its objects is strongly normalizing.<ref>{{cite journal |last1=Ohlebusch |first1=Enno |title=Church-Rosser theorems for abstract reduction modulo an equivalence relation |journal=Rewriting Techniques and Applications |date=1998 |volume=1379 |page=18 |doi=10.1007/BFb0052358 |url=https://www.google.com/books/edition/Rewriting_Techniques_and_Applications/ESr6CAAAQBAJ?hl=en&gbpv=1&pg=PA18}}</ref>
+A rewriting system has the ''normal form property'' (NF) if for all objects ''a'' and normal forms ''b'', ''b'' can be reached from ''a'' by a series of rewrites and inverse rewrites only if ''a'' reduces to ''b''. A rewriting system has the ''unique normal form property'' (UN) if for all normal forms ''a'', ''b'' ∈ ''S'', ''a'' can be reached from ''b'' by a series of rewrites and inverse rewrites only if ''a'' is equal to ''b''. A rewriting system has the ''unique normal form property with respect to reduction'' (UN<sup>→</sup>) if for every term reducing to normal forms ''a'' and ''b'', ''a'' is equal to ''b''.<ref name=NF>{{cite journal |last1=Klop |first1=J.W. |last2=de Vrijer |first2=R.C. |title=Unique normal forms for lambda calculus with surjective pairing |journal=Information and Computation |date=February 1989 |volume=80 |issue=2 |pages=97–113 |doi=10.1016/0890-5401(89)90014-X |url=https://www.sciencedirect.com/science/article/pii/089054018990014X}}</ref>
+== Results==
+Some well known results:
+* SN implies WN.<ref>{{cite web |title=logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems? |url=https://cs.stackexchange.com/questions/68080/what-is-the-difference-between-strong-normalization-and-weak-normalization-in-th |website=Computer Science Stack Exchange |access-date=12 September 2021}}</ref>
+* [[Confluence (term rewriting)|Confluence]] implies NF implies UN implies UN<sup>→</sup>.<ref name=NF/>
+* WN and UN imply confluence.<ref>{{cite book |last1=Terese |title=Term Rewriting Systems |date=20 March 2003 |publisher=Cambridge University Press |isbn=978-0-521-39115-3 |page=17 |url=https://www.google.com/books/edition/Term_Rewriting_Systems/7QQ5u-4tRUkC?hl=en&gbpv=1&pg=PA17 |language=en}}</ref>
+== Examples ==
 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.
 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.
+The 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.
-==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.
-Often weakly normalizing is simply called '''normalizing''' and strongly normalizing is referred to as ''terminating''.<ref>{{cite journal |last1=Ohlebusch |first1=Enno |title=Church-Rosser theorems for abstract reduction modulo an equivalence relation |journal=Rewriting Techniques and Applications |date=1998 |volume=1379 |page=18 |doi=10.1007/BFb0052358 |url=https://www.google.com/books/edition/Rewriting_Techniques_and_Applications/ESr6CAAAQBAJ?hl=en&gbpv=1&pg=PA18}}</ref>
-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 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>
@@ Line 25: / Line 30: @@
 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.
+=== Untyped lambda calculus ===
-See [[Normalization property (abstract rewriting)]] for normalization properties of [[Lambda calculi]].
+The ''pure'' untyped [[lambda calculus]] does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term <math>\lambda x . x x x</math>. It has the following rewrite rule: For any term <math>t</math>,
+: <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math>
+But consider what happens when we apply <math>\lambda x . x x x</math> to itself:
+: <math>\begin{align}
+(\mathbf{\lambda} x . x x x) (\lambda x . x x x)
+& \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)
+\\
+& \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)
+\\
+& \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)
+\\
+& \rightarrow \ \ldots\,
+\end{align}
+</math>
+Therefore the term <math>(\lambda x . x x x) (\lambda x . x x x)</math> is neither strongly nor weakly normalizing.
+=== Typed lambda calculus ===
+Various systems of [[typed lambda calculus]] including the
-==Normalization and confluency==
+[[simply typed lambda calculus]], [[Jean-Yves Girard]]'s [[System F]], and [[Thierry Coquand]]'s [[calculus of constructions]] are strongly normalizing.
-[[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]].
+A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program [[termination analysis|terminates]]. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be [[Turing complete]], otherwise one could solve the halting problem by seeing if the program type-checks. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the [[calculus of constructions]] or [[System F]]), for example a [[Meta-circular evaluator#Self-interpretation in total programming languages|self-interpreter]].<ref>{{cite book |last1=Riolo |first1=Rick |last2=Worzel |first2=William P. |last3=Kotanchek |first3=Mark |title=Genetic Programming Theory and Practice XII |date=4 June 2015 |publisher=Springer |isbn=978-3-319-16030-6|page=59 |url=https://www.google.com/books/edition/Genetic_Programming_Theory_and_Practice/rfDLCQAAQBAJ?hl=en&gbpv=1&pg=PA59 |access-date=8 September 2021 |language=en}}</ref>
-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 ==
 * [[Canonical form]]
+* [[Typed lambda calculus]]
+* [[Rewriting]]
+* [[Total functional programming]]
+* [[Barendregt&ndash;Geuvers&ndash;Klop conjecture]]
+* [[Newman's lemma]]
+* [[Normalization by evaluation]]
 == Notes ==
@@ Line 46: / Line 78: @@
 [[Category:Formal languages]]
 [[Category:Rewriting systems]]
+[[Category:Lambda calculus]]
+[[Category:Logic in computer science]]