Pergunta

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$).

Nenhuma solução correta

Licenciado em: CC-BY-SA com atribuição
Não afiliado a cs.stackexchange
scroll top