Normal form (abstract rewriting): Difference between revisions

Content deleted Content added

Inline

Revision as of 20:59, 27 April 2024

In abstract rewriting,^[1] 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. Many properties of rewriting systems relate to normal forms.

Definitions

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 rewriting 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 a normal form. An abstract rewriting system is strongly normalizing, terminating, noetherian, or has the (strong) normalization property (SN), if each of its objects is strongly normalizing.^[2]

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.^[3]

Results

This section presents some well known results. First, SN implies WN.^[4]

Confluence (abbreviated CR) implies NF implies UN implies UN^→.^[3] The reverse implications do not generally hold. {a→b,a→c,c→c,d→c,d→e} is UN^→ but not UN as b=e and b,e are normal forms. {a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.

WN and UN^→ imply confluence. Hence CR, NF, UN, and UN^→ coincide if WN holds.^[5]

Examples

One example is that simplifying arithmetic expressions produces a number - in arithmetic, all numbers are normal forms. A remarkable fact is that all arithmetic expressions have a unique value, so the rewriting system is strongly normalizing and confluent:^[6]

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 ⇒ 2 ⇒ 3 ⇒ ...) and loops such as the transformation function of the Collatz conjecture (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., it is an open problem if there are any other loops of the Collatz transformation).^[7] Another example is the single-rule system { r(x,y) → r(y,x) }, which has no normalizing properties 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. This leads to the idea of rewriting "modulo commutativity" where a term is in normal form if no rules but commutativity apply.^[8]

The system {b → a, b → c, c → b, c → d} (pictured) is an example of a weakly normalizing but not strongly normalizing system. a and d are normal forms, and b and c can be reduced to a or d, but the infinite reduction b → c → b → c → ... means that neither b nor c is strongly normalizing.

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$ (application is left associative). 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 \ \cdots \,\end{aligned}}

Therefore, the term $(\lambda x.xxx)(\lambda x.xxx)$ is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.

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. This means that there are computable functions that cannot be defined in the simply typed lambda calculus, and similarly for the calculus of constructions and System F. A typical example is that of a self-interpreter in a total programming language.^[10]

Notes

References

^ Franz Baader; Tobias Nipkow (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. Lecture Notes in Computer Science. Vol. 1379. p. 18. doi:10.1007/BFb0052358. ISBN 978-3-540-64301-2.
^ ^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.
^ Ohlebusch, Enno (17 April 2013). Advanced Topics in Term Rewriting. Springer Science & Business Media. pp. 13–14. ISBN 978-1-4757-3661-8.
^ Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. p. 1. ISBN 0-521-39115-6.
^ Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. p. 2. ISBN 0-521-39115-6.
^ Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "6. Rewrite Systems". In Jan van Leeuwen (ed.). Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 9–10. CiteSeerX 10.1.1.64.3114. ISBN 0-444-88074-7.
^ N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. p. 268. ISBN 0-444-88074-7.
^ 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] Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.

[2] Ohlebusch, Enno (1998). "Church-Rosser theorems for abstract reduction modulo an equivalence relation". Rewriting Techniques and Applications. Lecture Notes in Computer Science. Vol. 1379. p. 18. doi:10.1007/BFb0052358. ISBN 978-3-540-64301-2.

[NF-3] 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.

[4] "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.

[5] Ohlebusch, Enno (17 April 2013). Advanced Topics in Term Rewriting. Springer Science & Business Media. pp. 13–14. ISBN 978-1-4757-3661-8.

[6] Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. p. 1. ISBN 0-521-39115-6.

[7] Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. p. 2. ISBN 0-521-39115-6.

[8] Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "6. Rewrite Systems". In Jan van Leeuwen (ed.). Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 9–10. CiteSeerX 10.1.1.64.3114. ISBN 0-444-88074-7.

[Dershowitz.Jouannaud.1990.Fig2-9] N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. p. 268. ISBN 0-444-88074-7.

[10] 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]

[5]

[6]

[7]

[8]

[9]

[10]

@@ Line 1: / Line 1: @@
+{{Short description|Expression that cannot be rewritten further}}
 In [[abstract rewriting]],<ref>{{cite book |author=[[Franz Baader]] |author2=[[Tobias Nipkow]] |title=Term Rewriting and All That |year=1998 |publisher=[[Cambridge University Press]] |isbn=9780521779203 |url=https://books.google.com/books?id=N7BvXVUCQk8C&q=%22normal+form%22}}</ref> 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. Many properties of rewriting systems relate to normal forms.
@@ Line 4: / Line 5: @@
 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 rewriting 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 a normal form. An abstract rewriting system is ''strongly normalizing'', ''terminating'', ''noetherian'', or has the '''(strong) normalization property''' (SN), 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 |series=Lecture Notes in Computer Science |date=1998 |volume=1379 |page=18 |doi=10.1007/BFb0052358 |isbn=978-3-540-64301-2 |url=https://www.google.com/books/edition/Rewriting_Techniques_and_Applications/ESr6CAAAQBAJ?hl=en&gbpv=1&pg=PA18}}</ref>
+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 rewriting 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 a normal form. An abstract rewriting system is ''strongly normalizing'', ''terminating'', ''noetherian'', or has the '''(strong) normalization property''' (SN), if each of its objects is strongly normalizing.<ref>{{cite book |last1=Ohlebusch |first1=Enno |title=Rewriting Techniques and Applications |chapter=Church-Rosser theorems for abstract reduction modulo an equivalence relation |series=Lecture Notes in Computer Science |date=1998 |volume=1379 |page=18 |doi=10.1007/BFb0052358 |isbn=978-3-540-64301-2 |chapter-url=https://books.google.com/books?id=ESr6CAAAQBAJ&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://dx.doi.org/10.1016/0890-5401%2889%2990014-X}}</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 |doi-access=free }}</ref>
 == Results==
@@ Line 14: / Line 15: @@
 [[Confluence (term rewriting)|Confluence]] (abbreviated CR) implies NF implies UN implies UN<sup>→</sup>.<ref name=NF/> The reverse implications do not generally hold. {a→b,a→c,c→c,d→c,d→e} is UN<sup>→</sup> but not UN as b=e and b,e are normal forms. {a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.
-WN and UN<sup>→</sup> imply confluence. Hence CR, NF, UN, and UN<sup>→</sup> coincide if WN holds.<ref>{{cite book |last1=Ohlebusch |first1=Enno |title=Advanced Topics in Term Rewriting |date=17 April 2013 |publisher=Springer Science & Business Media |isbn=978-1-4757-3661-8 |pages=13–14 |url=https://www.google.com/books/edition/Advanced_Topics_in_Term_Rewriting/jSHaBwAAQBAJ?hl=en&gbpv=1&pg=PA13 |language=en}}</ref>
+WN and UN<sup>→</sup> imply confluence. Hence CR, NF, UN, and UN<sup>→</sup> coincide if WN holds.<ref>{{cite book |last1=Ohlebusch |first1=Enno |title=Advanced Topics in Term Rewriting |date=17 April 2013 |publisher=Springer Science & Business Media |isbn=978-1-4757-3661-8 |pages=13–14 |url=https://books.google.com/books?id=jSHaBwAAQBAJ&pg=PA13 |language=en}}</ref>
 == Examples ==
 One example is that simplifying arithmetic expressions produces a number - in arithmetic, all numbers are normal forms. A remarkable fact is that all arithmetic expressions have a unique value, so the rewriting system is strongly normalizing and confluent:<ref>{{cite book |author1=Terese |title=Term rewriting systems |date=2003 |publisher=Cambridge University Press |location=Cambridge, UK |isbn=0-521-39115-6 |page=1}}</ref>
-:(3 + 5) * (1 + 2) -> 8 * (1 + 2) -> 8 * 3 -> 24
+:(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24
-:(3 + 5) * (1 + 2) -> (3 + 5) * 3 -> 3*3 + 5*3 -> 9 + 5*3 -> 9 + 15 -> 24
+:(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24
-Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 -> 2 -> 3 -> ...) and loops such as the transformation function of the [[Collatz conjecture]] (1 -> 2 -> 4 -> 1 -> ..., it is an open problem if there are any other loops of the Collatz transformation).<ref>{{cite book |author1=Terese |title=Term rewriting systems |date=2003 |publisher=Cambridge University Press |location=Cambridge, UK |isbn=0-521-39115-6 |page=2}}</ref> Another example is the single-rule system { ''r''(''x'',''y'')&nbsp;→&nbsp;''r''(''y'',''x'') }, which has no normalizing properties since from any term, e.g. ''r''(4,2) a single rewrite sequence starts, viz. ''r''(4,2)&nbsp;→&nbsp;''r''(2,4)&nbsp;→&nbsp;''r''(4,2)&nbsp;→&nbsp;''r''(2,4)&nbsp;→&nbsp;..., which is infinitely long. This leads to the idea of rewriting "modulo [[commutativity]]" where a term is in normal form if no rules but commutativity apply.<ref>{{cite book| first1=Nachum|last1=Dershowitz,|first2=Jean-Pierre|last2=Jouannaud| chapter-title=Rewrite Systems|title=Handbook of Theoretical Computer Science| year=1990| volume=B|chapter=6| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen| series=Handbook of Theoretical Computer Science|citeseerx=10.1.1.64.3114|isbn=0-444-88074-7|pages=9-10}}</ref>
+Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 ⇒ 2 ⇒ 3 ⇒ ...) and loops such as the transformation function of the [[Collatz conjecture]] (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., it is an open problem if there are any other loops of the Collatz transformation).<ref>{{cite book |author1=Terese |title=Term rewriting systems |date=2003 |publisher=Cambridge University Press |location=Cambridge, UK |isbn=0-521-39115-6 |page=2}}</ref> Another example is the single-rule system { ''r''(''x'',''y'')&nbsp;→&nbsp;''r''(''y'',''x'') }, which has no normalizing properties since from any term, e.g. ''r''(4,2) a single rewrite sequence starts, viz. ''r''(4,2)&nbsp;→&nbsp;''r''(2,4)&nbsp;→&nbsp;''r''(4,2)&nbsp;→&nbsp;''r''(2,4)&nbsp;→&nbsp;..., which is infinitely long. This leads to the idea of rewriting "modulo [[commutativity]]" where a term is in normal form if no rules but commutativity apply.<ref>{{cite book| first1=Nachum|last1=Dershowitz|first2=Jean-Pierre|last2=Jouannaud| chapter=6. Rewrite Systems|title=Handbook of Theoretical Computer Science| year=1990| volume=B| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen|citeseerx=10.1.1.64.3114|isbn=0-444-88074-7|pages=9–10}}</ref>
+[[File:Cyclic_locally,_but_not_globally_confluent_rewrite_system.png|thumb|Weakly but not strongly normalizing rewrite system<ref name="Dershowitz.Jouannaud.1990.Fig2">{{cite book | isbn=0-444-88074-7 | editor=Jan van Leeuwen | title=Formal Models and Semantics | publisher=Elsevier | series=Handbook of Theoretical Computer Science | volume=B | year=1990 | author=N. Dershowitz and J.-P. Jouannaud | contribution=Rewrite Systems | page=268}}</ref>]]
+The system {''b'' → ''a'', ''b'' → ''c'', ''c'' → ''b'', ''c'' → ''d''} (pictured) is an example of a weakly normalizing but not strongly normalizing system. ''a'' and ''d'' are normal forms, and ''b'' and ''c'' can be reduced to ''a'' or ''d'', but the infinite reduction ''b'' → ''c'' → ''b'' → ''c'' → ... means that neither ''b'' nor ''c'' is strongly normalizing.
 === Untyped lambda calculus ===
@@ Line 43: / Line 47: @@
 </math>
-Therefore the term <math>(\lambda x . x x x) (\lambda x . x x x)</math> is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.
+Therefore, the term <math>(\lambda x . x x x) (\lambda x . x x x)</math> is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.
 === Typed lambda calculus ===
@@ Line 50: / Line 54: @@
 [[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 [[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>
+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. This means that there are computable functions that cannot be defined in the simply typed lambda calculus, and similarly for the [[calculus of constructions]] and [[System F]]. A typical example is that of a [[Meta-circular evaluator#Self-interpretation in total programming languages|self-interpreter in a total programming language]].<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://books.google.com/books?id=rfDLCQAAQBAJ&pg=PA59 |access-date=8 September 2021 |language=en}}</ref>
 == See also ==
@@ Line 73: / Line 77: @@
 [[Category:Lambda calculus]]
 [[Category:Logic in computer science]]
+{{Normal forms in logic}}

v t e Normal forms in logic
Propositional logic	Negation normal form Conjunctive normal form Disjunctive normal form Algebraic normal form (Zhegalkin polynomial) Blake canonical form Canonical normal form Horn clause
Predicate logic	Skolem normal form Herbrandization Prenex normal form
Other	Beta normal form Modal clausal form Normal form (natural deduction)