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)


  • 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.
  • $\begingroup$ 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. $\endgroup$ – Damiano Mazza Nov 26 '17 at 15:23
  • $\begingroup$ 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. $\endgroup$ – cody Nov 26 '17 at 18:06

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.

| cite | improve this answer | |
  • $\begingroup$ 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 $\endgroup$ – Adam Nov 27 '17 at 20:46
  • $\begingroup$ 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 $\endgroup$ – Adam Nov 27 '17 at 20:50

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.