0
$\begingroup$

I am studying term rewriting by reading Baader/Nipkow's book: "Term Rewriting and All That".

I want to prove a lemma about terms, position of subterms and replacement of subterms. The notation is as follows:

$s|_{p}$ denotes the subterm of $s$ at position $p$.
$s[t]_{p}$ denotes the term obtained from $s$ by replacing the subterm at position $p$ by $t$.

The lemma I want to prove is:

Lemma 3.1.4 Let $s, t, r$ be terms and $p, q$ be strings over the positive integers.

  1. If $pq \in Pos(s)$, then $s|_{pq} = (s|_{p})|_{q}$.

  2. If $p \in Pos(s)$ and $q \in Pos(t)$, then

    2.1 $(s[t]_{p})|_{pq} = t|_{q}$

    2.2 $(s[t]_{p})[r]_{pq} = s[t[r]_{q}]_{p}$

  3. If $pq \in Pos(s)$, then

    3.1 $(s[t]_{pq})|_{p} = (s|_{p})[t]_{q}$

    3.2 $(s[t]_{pq})[r]_{p} = s[r]_{p}$.

  4. If $p$ and $q$ are parallel positions in $s$ (i.e. $p || q$), then

    4.1 $(s[t]_{p})|_{q} = s|_{q}$

    4.2 $(s[t]_{p})[r]_{q} = (s[r]_{q})[t]_{p}$

The book provides proof for the first item:

As an example, we show, by induction on the length of $p$ that $s|_{pq} = (s|_{p})|_{q}$ holds for all $pq \in Pos(s)$.

For $p = \epsilon$, we have $pq = q$, and thus $s|_{pq} = s|_{q}$. In addition, $p = \epsilon$ implies $s|_{p} = s$, which shows $s|_{q} = (s|_{p})|_{q}$.

Now assume that $p = ip'$. Because $ip'q \in Pos(S)$, we know that $s$ is of the form $s = f(s_1, \ldots, s_n)$ with $i \leq n$. By definition, $s|_{pq} = s|_{ip'q} = s_{i}|_{p'q}$, and by induction $s_{i}|_{p'q} = (s_{i}|_{p'})|_{q}$. Again, by definition, we obtain $s_{i}|_{p'} = s|_{ip'} = s|_{p}$, which finishes the proof of the induction step.

I want to prove that the other items are also true. I wrote my attempt as an answer, but of course, I welcome other solutions or feedback. Thanks in advance.

$\endgroup$
0
$\begingroup$

Item 2. If $p \in Pos(s)$ and $q \in Pos(t)$:

2.1 $(s[t]_{p})|_{pq} = t|_{q}$.
We prove by induction on the length of $p$:

Case $p = \epsilon$:
$(s[t]_{\epsilon})|_{\epsilon q} = t|_{\epsilon q} = t|_{q}$.

Case $p = ip'$:
$(s[t]_{ip'})|_{ip'q} = f(s_1, \ldots, s_i[t]_{p'}, \ldots, s_n)|_{ip'q} = (s_{i}[t]_{p'})|_{p'q}$. By induction hypothesis, $(s_{i}[t]_{p'})|_{p'q} = t|_{q}$.

2.2 $(s[t]_{p})[r]_{pq} = s[t[r]_{q}]_{p}$.
We prove by induction on the length of $p$:

Case $p = \epsilon$:
Notice that $(s[t]_{\epsilon})[r]_{\epsilon q} = t[r]_{q}$ and also that: $s[t[r]_{q}]_{\epsilon} = t[r]_{q}$.

Case $p = ip'$:
$(s[t]_{ip'})[r]_{ip'q} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{ip'q} = f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{p'q}, \ldots, s_n)$. By induction hypothesis, $$(s_{i}[t]_{p'})[r]_{p'q} = s_i[t[r]_{q}]_{p'}$$ and hence $f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{p'q}, \ldots, s_n) = f(s_1, \ldots, s_i[t[r]_{q}]_{p'}, \ldots, s_n) = s[t[r]_{q}]_{ip'}$.

Item 3. If $pq \in Pos(s)$, then :

3.1 $(s[t]_{pq})|_{p} = (s|_{p})[t]_{q}$.
We prove by induction on the length of $p$:

Case $p = \epsilon$:
notice that $(s[t]_{\epsilon q})|_{\epsilon} = s[t]_{q}$ and also that $(s|_{\epsilon})[t]_{q} = s[t]_{q}$.

Case $p = ip'$:
$(s[t]_{ip'q})|_{ip'} = f(s_1, \ldots, s_{i}[t]_{p'q}, \ldots, s_n)|_{ip'} = (s_{i}[t]_{p'q})|_{p'}$. By induction hypothesis:

$$(s_{i}[t]_{p'q})|_{p'} = (s_{i}|_{p'})[t]_{q}$$

But $(s|_{ip'})[t]_{q} = (s_{i}|_{p'})[t]_{q}$ and thus the result holds.

3.2 $(s[t]_{pq})[r]_{p} = s[r]_{p}$.
We prove by induction on the length of $p$:

Case $p = \epsilon$:
$(s[t]_{\epsilon q})[r]_{\epsilon} = r = s[r]_{\epsilon}$.

Case $p = ip'$:
$(s[t]_{ip'q})[r]_{ip'} = f(s_1, \ldots, s_{i}[t]_{p'q}, \ldots, s_n)[r]_{ip'q} = f(s_1, \ldots, (s_{i}[t]_{p'q})[r]_{p'}, \ldots, s_n)$. By induction hypothesis:

$$(s_{i}[t]_{p'q})[r]_{p'} = s_{i}[r]_{p'} $$

and therefore we have $f(s_1, \ldots, (s_{i}[t]_{p'q})[r]_{p'}, \ldots, s_n) = f(s_1, \ldots, s_{i}[r]_{p'}, \ldots, s_n) = s[r]_{ip'}$.

Item 4. If $p$ and $q$ are parallel positions in $s$ (i.e. $p || q$), then

4.1 $(s[t]_{p})|_{q} = s|_{q}$
We prove by induction on the length of $p$:

Case $p = \epsilon$: This case can't happen, as $p$ and $q$ would not be parallel positions.

Case $ p = ip'$:
We now prove this by induction on the length of $q$.
If $q = \epsilon$:

This can't happen, as $p$ and $q$ would not be parallel positions.

If $q = jq'$:

There are two possibilities, according to whether $i = j$ or not.
Case $i = j$:

$(s[t]_{ip'})|_{iq'} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_{n})|_{iq'} = (s_{i}[t]_{p'})|_{q'}$. We have that $p'$ and $q'$ are parallel positions and thus, by induction hypothesis: $$(s_{i}[t]_{p'})|_{q'} = s_{i}|_{q'}.$$ Since we also have $s|_{iq'} = s_{i}|_{q'}$ the result holds.

Case $i \neq j$:

Let's suppose without loss of generality that $i > j$. Then:
$$(s[t]_{ip'})|_{jq'} = f(s_1, \ldots, s_{j}, \ldots, s_{i}[t]_{p'}, \ldots, s_{n})|_{jq'} = s_{j}|_{q'}.$$ Since we also have $s|_{jq'} = s_{j}|_{q'}$ the result holds.

4.2 $(s[t]_{p})[r]_{q} = (s[r]_{q})[t]_{p}$:

Case $p = \epsilon$: This case can't happen, as $p$ and $q$ would not be parallel positions.

Case $ p = ip'$:
We now prove this by induction on the length of $q$.
If $q = \epsilon$:

This can't happen, as $p$ and $q$ would not be parallel positions.

If $q = jq'$:

There are two possibilities, according to whether $i = j$ or not.
Case $i = j$:

$(s[t]_{ip'})[r]_{iq'} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{iq'} = f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{q'}, \ldots, s_n)$.
We have that $p'$ and $q'$ are parallel positions and thus, by induction hypothesis: $$ (s_{i}[t]_{p'})[r]_{q'} = (s_{i}[r]_{q'})[t]_{p'} $$ and hence $$f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{q'}, \ldots, s_n) = f(s_1, \ldots, (s_{i}[r]_{q'})[t]_{p'} , \ldots, s_n)= f(s_1, \ldots, s_{i}[r]_{q'}, \ldots, s_n)[t]_{ip'} = (s[r]_{q})[t]_{p}.$$

Case $i \neq j$:

Let's suppose without loss of generality that $i > j$. Then:
$$(s[t]_{ip'})[r]_{jq'} = f(s_1, \ldots, s_{j}, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{jq'} = f(s_1, \ldots, s_{j}[r]_{q'}, \ldots, s_{i}[t]_{p'}, \ldots, s_n) = f(s_1, \ldots, s_{j}[r]_{q'}, \ldots, s_{i}, \ldots, s_n)[t]_{ip'} = (s[r]_{jq'})[t]_{ip'}.$$

$\endgroup$

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.