<p>I think you have misunderstood the definitions:</p>

<p><strong>TERESE (9.1.1):</strong></p>

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

<p>This means that</p>

<ol>
<li>If $a\rightarrow_S b$, then $a\rightarrow b$ (sub-ARS condition)</li>
<li>If there exists $b$ such that $a\rightarrow b$, then there exists $b'$ such that $a\rightarrow_S b'$ (same normal forms).</li>
</ol>

<p>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$.</p>

<p><strong>TERESE (9.1.12):</strong></p>

<p>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 <em>not</em> in $A$ is normalizing.</p>

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

<ol>
<li>Ends on a normal form</li>
<li>Ends in $A$.</li>
</ol>

<p>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.</p>

CC BY-SA 3.0
2012-07-10T12:24:00.297Z
2012-07-10T12:24:00.297Z
cody
<p>A strategy for a rewriting system is a sub-rewriting system with the same objects and same normal forms.</p>

<p>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 <strong>normalizing</strong> if the restriction of S (as a relation) to steps which do not have their sources in N is terminating.</p>

<p>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.</p>

<lo.logic><term-rewriting-systems><normalization>
Explanation of definition of normalizing: 9.1.12 in Terese "Term Rewriting Systems"?
Jonathan Gallagher
# Explanation of definition of normalizing: 9.1.12 in Terese "Term Rewriting Systems"?

(Asked by: username_0 on 2012-07-03)

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.

**Tags:** lo.logic, term-rewriting-systems, normalization


---

## 1 answers

### Answer by username_1 on 2012-07-10. Score: 1 | Accepted answer

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.


---

