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$ Commented Nov 26, 2017 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
    Commented Nov 26, 2017 at 18:06

1 Answer 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.

  • $\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
    Commented Nov 27, 2017 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
    Commented Nov 27, 2017 at 20:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.