5
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Are you looking for a property of the TRS or of individual terms in a TRS? $\endgroup$ – Martin Berger Apr 18 at 9:39
  • $\begingroup$ Individual terms. In the TRS with rules "f(x,y) -> x" and "f(x,y) -> y", the term "f(a,a)" inevitably reduces to "a", but there's nothing interesting you can say about the TRS as a whole regarding this. $\endgroup$ – James Koppel Apr 18 at 16:04
5
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Thanks for the answer! On reflection, most of the inevitable reductions I care about in my application are actually fragments where the system is deterministic. $\endgroup$ – James Koppel Apr 18 at 17:21

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.