4
$\begingroup$

In the context of rewriting systems, how does strong normalization differ from weak normalization?

$\endgroup$
5
  • 5
    $\begingroup$ The article you linked literally answers your question. $\endgroup$
    – quicksort
    Dec 30 '16 at 23:10
  • $\begingroup$ I know it does, but I was having difficulty realising how the two kinds of normalization play together, which @chi kindly solved below. It is sometimes good practice (and a token of empathic thinking) to answer to the need behind the question than only take the question in its literal form. $\endgroup$
    – matanster
    Dec 30 '16 at 23:21
  • 3
    $\begingroup$ It would likewise be a kind gesture of the asker to explain in sufficient detail what would be expected from an answer, rather than expecting others to read his mind. $\endgroup$
    – quicksort
    Dec 30 '16 at 23:27
  • $\begingroup$ @quicksort Some people are worse than others in reading the crux of a simple question. Downvote and move on please. $\endgroup$
    – matanster
    Dec 30 '16 at 23:32
  • $\begingroup$ So do not make it harder for them. quicksort is right, it would be nice to reveal the expectations. Just because the mind reading succeded this time it will probably not be the case the most of the time. No downvote, sorry. $\endgroup$
    – Evil
    Dec 30 '16 at 23:46
10
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.