<p>I'm not sure there is a name for this specific property, though I would say "All right-hand sides are in head-normal form".</p>

<p>To be honest, this seems like a very strange property to request, especially since an inner reduction may provoke a head reduction, like so:</p>

<p>$$ {\cal R} = \{a \rightarrow b, f(b)\rightarrow f(a)\}$$
(I'm using letters for function symbols instead of numbers, as is traditional). In this case $f(a)$, the right hand side of the second rule, does not match any rule at it's head, but it may match the second rule if you apply the $a\rightarrow b$ reduction inside.</p>

CC BY-SA 3.0
2017-11-27T20:46:43.637Z
this is exactly a case I would like to exclude as there is a rule $a\rightarrow b$ which has its rhs $b$ contained non-trivially in an other rule’s lhs $f(b)$, would the first rule be $a\rightarrow f(b)$ it would be okay as then the containment would be trivial
Adam
CC BY-SA 3.0
2017-11-27T20:50:31.460Z
the reason behind this property is that we can start reducing a tree at its root and when no new rule is applicable we can move on to the children without looking back
Adam
CC BY-SA 3.0
2017-11-27T19:58:53.997Z
2017-11-27T19:58:53.997Z
cody
<p>Given TRS let's call it <strong>top-reducible</strong> or <strong>left-reducible</strong> if no rule's right hand side is contained in any rule's left hand side non-trivially. </p>

<p>A term A is contained in an other one B trivially if they overlap at their roots e.g. <code>2(y)</code> is contained in <code>1(2(x))</code> non-trivially while <code>1(y)</code> is contained in <code>1(2(x))</code> trivially) (I also don't know if this 'containment' has a name)</p>

<p>E.g.</p>

<ul>
<li>A TRS with a single rule <code>1(2(x)) -&gt; 2(x)</code> is not top-reducible.</li>
<li>A TRS with rules <code>1(2(x)) -&gt; 3(x)</code>, <code>4(3(5(x,y))) -&gt; 1(5(x,y))</code> is not top-reducible.</li>
</ul>

CC BY-SA 3.0
2017-11-26T15:23:03.133Z
I don't know if your property on rewriting  rule has a name, but I'm not sure I completely understand your notion of "trivial containment".  Is $a(b,x)$ trivially contained in $a(y,c)$?  ($a,b,c$ are function symbols, $x,y$ variables).  If yes, then I think what you call "trivial containment" is a symmetric notion (so the terminology "containment" is perhaps a bit misleading) and it's usually called *unifiability*.
Damiano Mazza
CC BY-SA 3.0
2017-11-26T18:06:55.763Z
Usually, people refer to "top reducible" as "head reducible" or "having a head redex". Likewise, "contained" should be "matches". The relation is *not* symmetric, as @DamianoMazza points out.
cody
<reference-request><fl.formal-languages><term-rewriting-systems>
Is there a name for this property of a term rewriting system?
Adam
# Is there a name for this property of a term rewriting system?

(Asked by: username_0 on 2017-11-25)

Given TRS let's call it **top-reducible** or **left-reducible** if no rule's right hand side is contained in any rule's left hand side non-trivially.

A term A is contained in an other one B trivially if they overlap at their roots e.g. `2(y)` is contained in `1(2(x))` non-trivially while `1(y)` is contained in `1(2(x))` trivially) (I also don't know if this 'containment' has a name)

E.g.

* A TRS with a single rule `1(2(x)) -> 2(x)` is not top-reducible.
* A TRS with rules `1(2(x)) -> 3(x)`, `4(3(5(x,y))) -> 1(5(x,y))` is not top-reducible.

**Tags:** reference-request, fl.formal-languages, term-rewriting-systems
> **Comments:**
> **username_1**: I don't know if your property on rewriting  rule has a name, but I'm not sure I completely understand your notion of "trivial containment".  Is $a(b,x)$ trivially contained in $a(y,c)$?  ($a,b,c$ are function symbols, $x,y$ variables).  If yes, then I think what you call "trivial containment" is a symmetric notion (so the terminology "containment" is perhaps a bit misleading) and it's usually called *unifiability*.  
> **username_2**: Usually, people refer to "top reducible" as "head reducible" or "having a head redex". Likewise, "contained" should be "matches". The relation is *not* symmetric, as @DamianoMazza points out.  

---

## 1 answers

### Answer by username_2 on 2017-11-27. Score: 1

I'm not sure there is a name for this specific property, though I would say "All right-hand sides are in head-normal form".

To be honest, this seems like a very strange property to request, especially since an inner reduction may provoke a head reduction, like so:

$$ {\cal R} = \{a \rightarrow b, f(b)\rightarrow f(a)\}$$
(I'm using letters for function symbols instead of numbers, as is traditional). In this case $f(a)$, the right hand side of the second rule, does not match any rule at it's head, but it may match the second rule if you apply the $a\rightarrow b$ reduction inside.

> **Comments:**
> **username_0**: this is exactly a case I would like to exclude as there is a rule $a\rightarrow b$ which has its rhs $b$ contained non-trivially in an other rule’s lhs $f(b)$, would the first rule be $a\rightarrow f(b)$ it would be okay as then the containment would be trivial  
> **username_0**: the reason behind this property is that we can start reducing a tree at its root and when no new rule is applicable we can move on to the children without looking back  

---

