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

<p>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 <em>it behaves poorly under substitution</em>:</p>

<p>If <span class="math-container">$t\rightarrow t'$</span> is an inevitable reduction, and <span class="math-container">$t$</span> contains a free variable <span class="math-container">$x$</span> which also appears in <span class="math-container">$t'$</span>, then <span class="math-container">$t[u/x]\rightarrow t'[u/x]$</span> is <strong>never</strong> an inevitable reduction if <span class="math-container">$u$</span> is not normal (since if <span class="math-container">$u\rightarrow u'$</span> then <span class="math-container">$t[u/x] \rightarrow t'[u'/x]$</span> can avoid <span class="math-container">$t'[u/x]$</span>).</p>

<p>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 <em>only</em> have inevitable reductions).</p>

<p>In general, rewrite theorists are more interested in which <em>redexes</em> 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 <strong>needed reductions</strong>: a needed redex is one that must be triggered in order to reach a normal form. See e.g. <a href="https://www.sciencedirect.com/science/article/pii/0890540187900010" rel="noreferrer">Needed reduction and spine strategies for the lambda calculus</a> or <a href="https://www.semanticscholar.org/paper/Reduction-Strategies-for-Left-Linear-Term-Rewriting-Toyama/126754ca605074da72f41442757e5be57b790213" rel="noreferrer">Reduction Strategies for Left-Linear Term Rewriting Systems</a>.</p>

<p>I believe this latter notion <em>is</em> stable under substitution for reasonable systems (say, orthogonal).</p>

CC BY-SA 4.0
2019-04-18T17:21:18.610Z
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.
James Koppel
CC BY-SA 4.0
2019-04-18T16:11:31.603Z
2019-04-18T16:11:31.603Z
cody
<p>I was just working on a semantics paper and realized I needed a notion of <em>inevitable reduction</em>. I came up with this definition:</p>

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

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

<p>So, anyone know prior work on this?</p>

CC BY-SA 4.0
2019-04-18T09:39:30.413Z
Are you looking for a property of the TRS or of individual terms in a TRS?
Martin Berger
CC BY-SA 4.0
2019-04-18T16:04:06.690Z
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.
James Koppel
<reductions><semantics><term-rewriting-systems>
Is there a notion of "inevitable reduction?"
James Koppel
# Is there a notion of "inevitable reduction?"

(Asked by: username_0 on 2019-04-16)

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?

**Tags:** reductions, semantics, term-rewriting-systems
> **Comments:**
> **username_1**: Are you looking for a property of the TRS or of individual terms in a TRS?  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2019-04-18. Score: 5 | Accepted answer

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](https://www.sciencedirect.com/science/article/pii/0890540187900010) or [Reduction Strategies for Left-Linear Term Rewriting Systems](https://www.semanticscholar.org/paper/Reduction-Strategies-for-Left-Linear-Term-Rewriting-Toyama/126754ca605074da72f41442757e5be57b790213).

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

> **Comments:**
> **username_0**: 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.  

---

