6
$\begingroup$

While doing some bibliography on term-rewriting, I often found these two properties to define a term rewrite rule (see for example here and this one):

A term rewrite rule is a pair $\langle l,r\rangle$ of terms, written $l \rightarrow r$, such that

1) $l$ is not a variable

2) all variables in $r$ occur also in $l$.

I fail to understand the reason of these properties, at least for the definition of a rule (I can see why they would matter for termination or confluence proofs). Why a term rewriting system could not contain a rule such as $x \rightarrow x + 1 - 1$ or $x \rightarrow x + y - y$ ? Just to provide some context, I'm trying to use TRS in the context of obfuscation, where such rewritings have meaning.

Can someone explain why rules composing a TRS would need these properties?

Improve this question
$\endgroup$
4
  • $\begingroup$ Indeed the rules are sufficient for the term rewrite system to be terminating. This observation is known as Lankford Theorem. Cf. Section 4 of the Rewriting chapter by Dershowitz and Plaisted from the Handbook of Automated Reasoning rewriting.loria.fr/documents/rewriting.pdf $\endgroup$
    – Dima Chubarov
    Commented Jan 11, 2017 at 8:09
  • $\begingroup$ Which theorem are you referring to? The rules are by no means sufficient for termination, e.g. $c\rightarrow c$ for some constant $c$ satisfies the above rules. $\endgroup$
    – cody
    Commented Jan 12, 2017 at 13:59
  • $\begingroup$ Thanks for the reference, I didn't know this one. But does this means that we could create a non-terminating TRS with rules not verifying these properties? @cody : I think the theorem is 4.6, even if it's not clear for me why ordering would be somehow equivalent to the two properties $\endgroup$
    – noutoff
    Commented Jan 12, 2017 at 14:07
  • $\begingroup$ It is not. The existence of a simplification ordering implies both rules 1. and 2., since in a simplification ordering $l>x$ for all $x$ in $l$, so in particular $l \not> r$ if it violates either rule. $\endgroup$
    – cody
    Commented Jan 12, 2017 at 16:13

1 Answer 1

Reset to default
3
$\begingroup$

In general, there is no obstacle to define a rewrite system as above, and a few sources do indeed require rules 1. and 2. only as additional hypotheses.

However the hypotheses are almost always necessary (but not sufficient!) for both termination and confluence, which is indeed the main object of study of rewriting as a field.

Perhaps it's useful to remind why this is the case:

Termination:

  1. If $x\rightarrow t$ is allowed as a rule, then any term $u$ rewrites to $t[u/x]$. In particular, the system is non-terminating.
  2. If $l\rightarrow r$ and $r$ contains a fresh variable $y$ not in $l$, then for example, $l\rightarrow r[l/y]$, and so the system is non-terminating.

Confluence:

  1. Take $x \rightarrow f(x)$ and $g(a)\rightarrow b$. Then $$ g(f(a))\leftarrow g(a)\rightarrow b$$ for instance, breaking confluence. In particular, you can "insert" an $f$ around any term you like, which makes confluence very hard to satisfy.

  2. If there are constants $a$ and $b$, then given the rule $f(x)\rightarrow g(y)$, you get $$ g(a)\leftarrow f(x)\rightarrow g(b)$$ again, breaking confluence.

Now every theorem involving either termination or confluence could be prefaced with "assuming 1. and 2. holds, ..." but it makes sense to restrict your attention to systems where the theorems aren't trivially false. I don't think anyone would be shocked by a paper which lifts these restrictions though, at least condition 2. (condition 1. really creates anarchy). Condition 2. is mostly about non-determinism, for which rewriting is a nice framework in general.

There are some systems in which free variables can appear in the RHS, but usually not any fresh variable $y$ is allowed: there are additional constraints which need to be satisfied, e.g.

$$f(x) \rightarrow f(y)\ \mid\ 0\leq y < x $$

where $x$ and $y$ are allowed to be integers. These types of systems are called constraint rewriting systems and are extensively studied.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks for your response! I'm actually not considering termination or confluence properties for obfuscation, as it's not really the purpose. But as I use rewriting systems for deobfuscation (in my case, simplification of expressions) where it is much closer to "classic" rewriting (i-e it's possible to prove termination / confluence), I wanted to know if the notions and notations could be used for obfuscation, even if that's just for the definitions and not the theorems, etc. Would you have a reference with a definition of rewrite rule that does not include the two properties? $\endgroup$
    – noutoff
    Commented Jan 12, 2017 at 15:38
  • $\begingroup$ I'm afraid nothing comes to mind at the moment. It's probably useful to note that production rules in the classical theory of grammars allow these kinds of rules, more or less. Classically the theory was described for strings, but the formalism easily extends to trees (unsurprisingly called Tree Grammars), which I don't know much about. $\endgroup$
    – cody
    Commented Jan 12, 2017 at 16:11
  • $\begingroup$ Production rules definitely seem worth investigating! $\endgroup$
    – noutoff
    Commented Jan 12, 2017 at 16:18

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.