1
$\begingroup$

Suppose we have a term rewriting system $\mathcal{R} = (\Sigma, R)$ with signature $\Sigma$ and set of basic rewrite rules $R$. Suppose we also have a set $S$ of ground rewrite rules, i.e. rewrite rules where both terms are ground terms. For my specific application, we can also assume that the right-hand sides of all rules in $S$ are single constants of $\Sigma$, and that the left- and right-hand sides of all rules in $S$ are distinct (so we don't have any rules in $S$ like $c \to c$, for some constant $c$). Now let $\mathcal{R}' = (\Sigma, R \cup S)$. If we know that the initial rewriting system $\mathcal{R}$ is confluent and terminating, are there any sufficient conditions on the rules $S$ and/or on the original system $\mathcal{R}$ that will ensure that the new system $\mathcal{R}'$ is still confluent and terminating?

In short: if we take a confluent and terminating term rewrite system and add some ground rules to it (subject to the extra conditions mentioned above), are there any conditions that will ensure that the new system is still confluent and terminating?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.