gotchaModerate
What is the difference between strong normalization and weak normalization in the context of rewrite systems?
Viewed 0 times
thewhatsystemsandrewriteweakdifferencebetweenstrongcontext
Problem
In the context of rewriting systems, how does strong normalization differ from weak normalization?
Solution
Weak normalization means that any term has a terminating rewriting sequence, i.e. admits a finite amount of rewritings which lead to a normal form (no more rewritings from that).
Strong normalization means that any term can never be rewritten infinitely many times. Any maximal rewriting sequence eventually reaches a normal form (hence it is finite).
For instance:
$$
S \rightarrow (SS) \qquad
S \rightarrow A
$$
is weakly normalizing (given any term, we can rewrite every $S$ into an $A$, after which normal form is reached) but not strongly normalizing ($S \rightarrow (SS) \rightarrow ((S S) S) \rightarrow \cdots$).
It is immediate to prove that strong normalization implies weak normalization.
Strong normalization means that any term can never be rewritten infinitely many times. Any maximal rewriting sequence eventually reaches a normal form (hence it is finite).
For instance:
$$
S \rightarrow (SS) \qquad
S \rightarrow A
$$
is weakly normalizing (given any term, we can rewrite every $S$ into an $A$, after which normal form is reached) but not strongly normalizing ($S \rightarrow (SS) \rightarrow ((S S) S) \rightarrow \cdots$).
It is immediate to prove that strong normalization implies weak normalization.
Context
StackExchange Computer Science Q#68080, answer score: 14
Revisions (0)
No revisions yet.