# Identifying/equating constants in a term rewrite system

Suppose we have a term rewrite system $\mathcal{R} = (R, \Sigma)$ with basic rewrite rules $R$ over a signature $\Sigma$. Suppose also that this rewrite system $\mathcal{R}$ is confluent and terminating, and that each constant symbol of $\Sigma$ is a normal form with respect to $\mathcal{R}$.

Now suppose that we want to identify/equate some of the constants of $\Sigma$. For example, if we have two constants $c, d$ in the signature $\Sigma$, then we may want to 'merge' $c$ and $d$ into a single constant $e$ (thereby obtaining a new signature $\Sigma'$ that is the same as $\Sigma$ except that $c$ and $d$ have been replaced by $e$), and then modify the basic rewrite rules in $R$ accordingly (by replacing all occurrences of $c$ and $d$ by $e$).

If we identify/equate some constants of $\Sigma$ in this way, and then modify the rules in $R$ accordingly, so that we obtain a slightly modified term rewrite system $\mathcal{R}' = (R', \Sigma')$, is there any way to prove that $\mathcal{R}'$ will still be confluent and terminating?

Obviously, if $R$ has a rule like $c \to d$ and we merge $c$ and $d$ into the single constant $e$, then this rule will become the rule $e \to e$, and so the resulting system will not be terminating. But this is why I assumed that each constant of $\Sigma$ is a normal form with respect to $\mathcal{R}$ (so that $R$ will not have rules like $c \to d$).

## 1 Answer

Counterexample:

$f(c) \rightarrow f(d)$

In general, there are some modularity theorems for termination and confluence that may apply if, e.g. your constants do not appear at all in any rule.

There are probably some weaker assumptions that can make this work though.

• Thanks for the answer. I think we can weaken the assumption that you mentioned, to the assumption that no rule contains distinct constants. I will post a proof as an answer, if this works out. – User7819 Jun 29 '18 at 0:52