# Explanation of definition of normalizing: 9.1.12 in Terese "Term Rewriting Systems"?

A strategy for a rewriting system is a sub-rewriting system with the same objects and same normal forms.

Definition (from Terese "Term Rewriting Systems"). Let N be a superset of the normal forms of a rewriting system $\to$. A strategy S for $\to$ is normalizing if the restriction of S (as a relation) to steps which do not have their sources in N is terminating.

I understand that the authors want a more general notion of normalizing such as the strategy which finds a (weak) head normal form. However, take N to be be exactly the set of normal forms. Then the definition should express that the strategy always finds a normal form provided one exists. I am having trouble bridging the gap here... It seems that N should have to also include the terms which do not have a normal form.

I think you have misunderstood the definitions:

TERESE (9.1.1):

A strategy $S$ for an ARS $\rightarrow$ is a sub-ARS $\rightarrow_S$ of $\rightarrow$ having the same objects and normal forms.

This means that

1. If $a\rightarrow_S b$, then $a\rightarrow b$ (sub-ARS condition)
2. If there exists $b$ such that $a\rightarrow b$, then there exists $b'$ such that $a\rightarrow_S b'$ (same normal forms).

The second condition can be read as: if $a$ is not a normal form, then there is some rewrite step from $a$ which conforms to strategy $S$.

TERESE (9.1.12):

If $A$ is a superset of the set of normal forms for $\rightarrow$, a strategy $S$ is $A$-normalizing if the restriction of $S$ to terms not in $A$ is normalizing.

This means that a strategy is $A$-normalizing if every reduction sequence for $\rightarrow_S$ either

1. Ends on a normal form
2. Ends in $A$.

Clearly if $A=NF$ then only case 1. is relevant. However if $A$ is taken to be terms in head-normal form, then case 2. may occur independently of case 1.