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 Answer 1

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$
4
  • 1
    $\begingroup$ So is this the answer to your own question? $\endgroup$
    – cody
    Commented Oct 2, 2020 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$ Commented Oct 2, 2020 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
    Commented Oct 2, 2020 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$ Commented Oct 2, 2020 at 22:30

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.