Is there a notion of "inevitable reduction?"

Question

I was just working on a semantics paper and realized I needed a notion of inevitable reduction. I came up with this definition:

Let $\rightarrow$ be a binary relation. We say that $a$ inevitably reduces to $b$, or $a \rightarrow^{\forall *} b$, if either $a=b$ or, for all derivations $a \rightarrow x_1 \rightarrow x_2 \rightarrow \dots$ (where the $x_i$ are either infinite or terminate in a normal form), there is some $i$ such that $x_i = b$.

This seems way too simple and fundamental to not already exist, but I've never encountered it before. (I've read "Term Rewriting and All That" in full, and just took a skim through "Advanced Topics in Term Rewriting".) It's clearly related to confluence, and can also be stated in terms of dominators. Still, I have no leads for finding prior uses.

So, anyone know prior work on this?

Answer 1

I have never heard of this exact concept in rewrite theory, which certainly doesn't prove it hasn't been considered.

However, I will make the point that it may not be quite as useful a concept as it first appears, at least in classical rewrite theory because it behaves poorly under substitution:

If $t\rightarrow t'$ is an inevitable reduction, and $t$ contains a free variable $x$ which also appears in $t'$, then $t[u/x]\rightarrow t'[u/x]$ is never an inevitable reduction if $u$ is not normal (since if $u\rightarrow u'$ then $t[u/x] \rightarrow t'[u'/x]$ can avoid $t'[u/x]$).

It would seem that inevitable reducts are quite rare in general, even for pretty reasonable systems, except for normal forms (which are interesting for other reasons). Obviously this only holds for general notions of reductions; specific strategies might have many more (deterministic strategies only have inevitable reductions).

In general, rewrite theorists are more interested in which redexes need to be reduced (to hit normal forms) rather than which terms need to be hit. This has been studied quite a bit, under the name of needed reductions: a needed redex is one that must be triggered in order to reach a normal form. See e.g. Needed reduction and spine strategies for the lambda calculus or Reduction Strategies for Left-Linear Term Rewriting Systems.

I believe this latter notion is stable under substitution for reasonable systems (say, orthogonal).