1
$\begingroup$

I am studying Term Rewriting by reading Baader's book "Term Rewriting and All That". I am in the chapter of Equational Unification, in the section of Commutative Functions. I am trying to do the following exercise:

Let $s, t \in T(\Sigma, V)$. By exercise 10.10 we know that the $\approx_{C}$-classes of these terms are finite. Let $\{s_1, \ldots, s_m \}$ be the $\approx_{C}$-class of $s$, and let $\{t_1, \ldots, t_n \}$ the $\approx_{C}$-class of $t$. Show that: $$ \mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \}) $$ and that $\{ \sigma \ | \ \sigma \ \text{ is an mgu of } s_i =^{?} t_j \text{ for some } i, j, 1 \leq i \leq m, 1 \leq j \leq n \}$ is a complete set of C-unifiers of $s \approx_{C}^{?} t$.

It seems obvious, but how can I prove that: $$\mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \}) ? \tag{1}$$

After I prove that, I know how to proceed: let $\delta$ be an arbitrary C-unifier of $s \approx_{C}^{?} t$. By the equation (1) above, this means that $\exists_{i, j}: \ s_i \delta = t_i \delta$. Take $\sigma$ the mgu of $s_i =^{?} t_j$ and we have that $\sigma$ is more general than $\delta$. Therefore, $\{ \sigma \ | \ \sigma \ \text{ is an mgu of } s_i =^{?} t_j \text{ for some } i, j, 1 \leq i \leq m, 1 \leq j \leq n \}$ is a complete set of C-unifiers of $s \approx_{C}^{?} t$.

How can I prove (1)? Any hint/suggestion is very much appreciated. Thanks in advance.

$\endgroup$
1
$\begingroup$

Note that for all $s, t \in T(\Sigma, V)$ we have:
$$s \approx_{C} t \iff \exists_{i, j}: s_i = t_j \tag{*}$$

Using (*) for the terms $s \sigma$ and $t \sigma$ we obtain: $$s \sigma \approx_{C} t \sigma \iff \exists_{i, j}: s_i \sigma = t_j \sigma, $$i.e, $$\mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \})$$

$\endgroup$
  • 1
    $\begingroup$ So is this the answer to your own question? $\endgroup$ – cody Oct 2 '20 at 19:56
  • $\begingroup$ Yes @cody I was having trouble with that question, but I think I found a way. I registered my attempt in case anyone in the future has the same issue. But of course I welcome other answers or comments :) $\endgroup$ – Gabriel F. Silva Oct 2 '20 at 21:54
  • 1
    $\begingroup$ My only comment is twofold: it's not obvious that step 1 implies step 2 (why should the equivalence class be closed under substitution?) Secondly: you should accept your answer if you think it solves the question. $\endgroup$ – cody Oct 2 '20 at 22:18
  • $\begingroup$ Thanks for the comments, I added more details to the answer. I will accept as soon as the StackExchange system allows me to accept my own answer (2 days, I think). $\endgroup$ – Gabriel F. Silva Oct 2 '20 at 22:30

Your Answer

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

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