3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\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.