Rewriting Techniques, 2: termination, interpretation

2019–11–21

A matrix interpretation on integers is the following:

Then \((\mathbb{N}^d, (L_f)_f, >_I)\) is a well-founded monotone algebra.

Consider the TRS \(\{\ \mathtt{s}(\mathtt{a}) \to \mathtt{s}(\mathtt{p}(\mathtt{a})),\ \mathtt{p}(\mathtt{b}) \to \mathtt{p}(\mathtt{s}(\mathtt{b}))\ \}\).

  1. Prove that its termination cannot be proved by a polynomial interpretation on integers;

  2. Use the following matrix interpretation to prove termination w.r.t. \(>_{\{1,2\}}\). \[L_{\mathtt{s}}(X) = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix}X \qquad L_{\mathtt{p}}(X) = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix}X \qquad L_{\mathtt{a}} = \begin{bmatrix} 0 \\ 1 \end{bmatrix} \qquad L_{\mathtt{b}} = \begin{bmatrix} 1 \\ 0 \end{bmatrix}\]

  3. Why does it fail if we take \(>_{\{1\}}\) instead? Is there another matrix interpretation that works with this ordering?

(1) From the first rule, the degree of \(\mathtt{P}_\mathtt{p}\) must be one. The same holds for \(\mathtt{P}_\mathtt{s}\), thanks to the second rule. This implies that \(\mathtt{P}_{\mathtt{s}(\mathtt{a})}\) of the form \(s_1a + s_0\) whereas \(\mathtt{P}_{\mathtt{s}(\mathtt{p}(\mathtt{a}))}\) of the form \(s_1p_1a + s_1p_0 + s_0\) which, since \(p_1 \geq 1\), is sufficient to conclude that the termination of this TRS cannot be proved by a polynomial interpretation on integers.

(2) It holds that: \[L_{\mathtt{s}}(L_{\mathtt{a}}) = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1,2\}} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = L_{\mathtt{s}}(L_{\mathtt{p}}(L_{\mathtt{a}}))\] \[L_{\mathtt{p}}(L_{\mathtt{b}}) = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1,2\}} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = L_{\mathtt{p}}(L_{\mathtt{s}}(L_{\mathtt{b}}))\]

(3) From the second rule, \(\begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1\}} \begin{bmatrix} 1 \\ 0 \end{bmatrix}\) does not hold. No, let \(L_{\mathtt{s}}(X) = M_{\mathtt{s}} X + V_{\mathtt{s}}\) and \(L_{\mathtt{p}}(X) = M_{\mathtt{p}} X + V_{\mathtt{p}}\). For the first rule it will hold \[\begin{aligned} L_{\mathtt{s}}(L_{\mathtt{a}}) &= M_{\mathtt{s}}L_{\mathtt{a}} + V_{\mathtt{s}}\\ L_{\mathtt{s}}(L_{\mathtt{p}}(L_{\mathtt{a}})) &= M_{\mathtt{s}}M_{\mathtt{p}}L_{\mathtt{a}} + M_{\mathtt{s}}V_{\mathtt{p}} + V_{\mathtt{s}}\end{aligned}\] To make \(>_{\{1\}}\) it must therefore hold \[(M_{\mathtt{s}})_{1,1}(L_{\mathtt{a}})_{1,1} + \dots + (M_{\mathtt{s}})_{1,d}(L_{\mathtt{a}})_{1,d} > (M_{\mathtt{p}})_{1,1}((M_{\mathtt{s}})_{1,1}(L_{\mathtt{a}})_{1,1} + \dots + (M_{\mathtt{s}})_{1,d}(L_{\mathtt{a}})_{1,d}) + \dots\] which implies \((M_{\mathtt{p}})_{1,1} = 0\). Similarly, from the second rule, \((M_{\mathtt{s}})_{1,1} = 0\). This implies that no polynomial interpretation with the ordering \(>_{\{1\}}\) can be defined for this TRS, since for any \(m > n\), \((m,0,\dots,0) >_{\{1\}} (n,0,\dots,0)\) but \(L_{\mathtt{s}}(m,0,\dots,0) =_{\{1\}} L_{\mathtt{s}}(n,0,\dots,0)\).

Let \(A \subseteq \mathbb{N}\) and \(\mathtt{P}_{f}\) be respectively the domain and the interpretation, for each function symbol \(f\), of a polynomial interpretation of integers for a TRS (note: the TRS is therefore terminating). Take \(a \in A \setminus \{0\}\).

  1. Define \(\pi_a : T(F,X) \to A\) as the function which maps every variable \(x\) to \(a\) and every term of the form \(f(t_1,\dots,t_n)\) to \(\mathtt{P}_f(\pi_a(t_1),\dots,\pi_a(t_n))\). Prove that \(\pi_a(t)\) is greater or equal to the length of every reduction starting from \(t\).

  2. Show that there exists \(d\) and \(k\) positive integers such that for every \(f \in F\) of arity \(n\) and every \(a_1,\dots,a_n \in A \setminus \{0\}\) it holds \(\mathtt{P}_f(a_1,\dots,a_n) \leq d \prod_{i=1}^n a_i^k\).

  3. From the previous point, pick \(d\) to be also greater or equal than \(a\) and fix \(c \geq k + \log_2(d)\). Prove that \(\pi_a(t) \leq 2^{2^{c|t|}}\).

Consider now any finite TRS and a function symbol \(f\). Prove that there exists an integer \(k\) such that if \(s \to t\) then \(|t|_f \leq k(|s|_f + 1)\), where \(|.|_f\) is the number of \(f\).

Deduce that the TRS \[\{\ \mathtt{a}(\mathtt{0},y) \to \mathtt{s}(y),\ \mathtt{a}(\mathtt{s}(x),\mathtt{0}) \to \mathtt{a}(x,\mathtt{s}(\mathtt{0})),\ \mathtt{a}(\mathtt{s}(x),\mathtt{s}(y)) \to \mathtt{a}(x,\mathtt{a}(\mathtt{s}(x),y))\ \},\] simulating the Ackermann’s function, cannot be proved terminating using a polynomial interpretation over integers.

For next week: well-founded induction, multisets, RPO

Consider exercise on semantic labeling of TD1, where the following rewriting system was defined \[\begin{aligned} \mathsf{f}\ (\mathsf{s}\ X) &\to \mathsf{f}\ (\mathsf{p}\ (\mathsf{s}\ X)) \diamond (\mathsf{s}\ X) & \mathsf{p}\ (\mathsf{s}\ \mathsf{z}) &\to \mathsf{z} \\ \mathsf{p}\ (\mathsf{s}\ (\mathsf{s}\ X)) &\to \mathsf{s}\ (\mathsf{p}\ (\mathsf{s}\ X))\end{aligned}\]

  1. Prove that RPO cannot prove the termination of the system.

  2. Prove that a labeled system can be proved terminating with RPO.

  1. Considering the first rewrite rule, \(\mathsf{f} > \diamond\) is needed. Then we must check that

    1. \(\mathsf{f}\ (\mathsf{s}\ X) >_{\text{rpo}} \mathsf{f}\ (\mathsf{p}\ (\mathsf{s}\ X))\) and

    2. \(\mathsf{f}\ (\mathsf{s}\ X) >_{\text{rpo}} (\mathsf{s}\ X)\).

    Second condition is immediate since \(\mathsf{s}\ X \lhd \mathsf{f}\ (\mathsf{s}\ X)\).

    First condition needs \(\mathsf{s}\ X >_{rpo} \mathsf{p}\ (\mathsf{s}\ X)\) which is impossible since \(\mathsf{s}\ X <_{rpo} \mathsf{p}\ (\mathsf{s}\ X)\) since \(\mathsf{s}\ X \lhd \mathsf{p}\ (\mathsf{s}\ X)\).

  2. With the following interpretation on \(\mathbb{N}\): \(\mathsf{z} = 0, \mathsf{s}\ X = X + 1\), \(\mathsf{p}\ X = \max(0, X - 1)\), \(\mathsf{lab}(R)\) is the following (infinite) system, for all \(i \in \mathbb{N}\) \[\begin{aligned} \mathsf{f}_{i + 1}\ (\mathsf{s}_i\ X) &\to \mathsf{f}_i\ (\mathsf{p}_{i + 1}\ (\mathsf{s}_i\ X)) \diamond (\mathsf{s}\ X) & \mathsf{p}\ (\mathsf{s}\ \mathsf{z}) &\to \mathsf{z} \\ \mathsf{p}_{i + 2}\ (\mathsf{s}\ (\mathsf{s}\ X)) &\to \mathsf{s}_i\ (\mathsf{p}_{i + 1}\ (\mathsf{s}_i\ X)) \end{aligned}\] If we take \(\mathsf{f}_i > \diamond\), \(\mathsf{f}_{i} > \mathsf{f}_{i+1}\), \(\mathsf{f}_i > \mathsf{p}_{i + 1}\), the first rule is ensured decreasing. The second rule is trivially decreasing. Taking \(\mathsf{p}_{i+2} > \mathsf{s}_i\) and \(\mathsf{p}_{i + 2} > \mathsf{p}_{i + 1}\) makes the last rule decreasing.

We consider the Ackermann’s function \[\begin{aligned} \mathtt{Ack}\ \mathtt{0}\ y &= y + 1\\ \mathtt{Ack}\ x\ 0 &= \mathtt{Ack}\ (x-1)\ 1\\ \mathtt{Ack}\ x\ y &= \mathtt{Ack}\ (x-1)\ (\mathtt{Ack}\ x\ (y-1))\end{aligned}\]

  1. Prove its termination via well-founded induction.

  2. The following rewrite system simulates \(\mathtt{Ack}\) \[\begin{aligned} \mathtt{a}(\mathtt{0},y) &\to \mathtt{s}(y)\\ \mathtt{a}(\mathtt{s}(x),\mathtt{0}) &\to \mathtt{a}(x,\mathtt{s}(\mathtt{0}))\\ \mathtt{a}(\mathtt{s}(x),\mathtt{s}(y)) &\to \mathtt{a}(x,\mathtt{a}(\mathtt{s}(x),y)) \end{aligned}\] Prove its termination using a LPO.

  3. Consider the well-founded domain \((\mathtt{Mult}(\mathbb{N}\times\mathbb{N}), (>_\text{lex})_\text{mul})\). Prove the termination of \(\mathtt{Ack}\) using the following abstraction: \[\begin{aligned} \phi:\ T(\{\mathtt{a},\mathtt{s}\},X) &\to \mathtt{Mult}(\mathbb{N}\times \mathbb{N})\\ t &\to \{\!|\ (|u|,|v|) \mid t|_{p\in \text{Pos}(t)} = \mathtt{a}(u,v)\ |\!\} \end{aligned}\] where \(|\mathtt{0}| = 1\), \(|\mathtt{a}(x,y)| = |x|+|y|+1\) and \(|\mathtt{s}(x)| = |x| + 1\).

  1. Induction on \({(\mathbb{N}\times\mathbb{N}, >_\text{lex})}\). We prove that the calculus of \(\mathtt{Ack}\ u\ v\) terminates by induction \((u,v)\) ordered lexicographically on integers.

  2. Let \(>\) be such that \(\mathtt{a}> \mathtt{s}\) and let \(\mathtt{status}(\mathtt{a}) = \mathtt{status}(\mathtt{s}) = \text{lex}\). It holds:

  3. We can show that whenever \(s \to t\), then \(\phi(s) < \phi(t)\).

A weight function for a signature \(\Sigma\) is a pair \((w, w_0)\) consisting of a mapping \(w : \Sigma \to \mathbb{N}\) and a constant \(w_0 > 0\) such that \(w(c) \geq w_0\) for all constant \(c \in \Sigma\). Let \((w, w_0)\) be a weight function. The weight of a term \(t\) is defined as follows \[w(t) = \begin{cases} w_{0} & \text{if } t \text{ is a variable} \\ w(f) + \sum_{i=1}^n w(t_i) & \text{if } t = f(t_1, \dots, t_n) \end{cases}\] We denote \(|s|_x\) for \(x\) a variable the number of times that \(x\) occurs in \(s\). Let \(>\) be a precedence and \((w, w_{0})\) a weight function. We define the Knuth-Bendix order (KBO) \(>_{\text{kbo}}\) on terms inductively as follows: \(s >_{\text{kbo}} t\) if \(|s|_{x} \geq |t|_{x}\) for all variables \(x\) and either

  1. \(w(s) > w(t)\), or

  2. \(w(s) = w(t)\) and one of the following alternatives holds

    1. \(t\) is a variable and \(s = f^{n}(t)\) for some unary function symbol \(f\) and \(n > 0\),

    2. \(s = f(s_1, \dots, s_n), t = f(t_1, \dots, t_n)\) and there is \(i \in \{ 1, \dots, n \}\) such that \(s_j = t_j\) for all \(1 \leq j < i\) and \(s_i >_{\text{kbo}} t_i\), or

    3. \(s = f(s_1, \dots, s_n), t = g(t_1, \dots, t_m)\) and \(f > g\).

Using a KBO, prove the termination of:

  1. \(\{ \mathtt{l}(x) + (y + z) \to x + (\mathtt{l}(\mathtt{l}(y)) + z),\ \mathtt{l}(x) + (y + (z + w)) \to x + (z + (y + w))\ \}\)

  2. \(\{\ \mathtt{r}^n(\mathtt{l}^k(x)) \to \mathtt{l}^k(\mathtt{r}^m(x))\ \}\), where \(n,k > 0\) and \(m \geq 0\).

  1. Let \(\mathtt{l}> +\), \(w(\mathtt{l}) = 0\), \(w(+) = w(x) > 0\) for each variable \(x\). It holds that \(w\) is admissible. For both rules, it holds that the weight does not change after the rewrite step. To prove that \(\mathtt{l}(x) + (y + z) >_\text{kbo}x + (\mathtt{l}(\mathtt{l}(y)) + z)\) we therefore need to prove the third condition, which holds since \(\mathtt{l}(x) >_\text{kbo}x\). Similarly, to prove \(\mathtt{l}(x) + (y + (z + w)) >_\text{kbo}x + (z + (y + w))\), it is sufficient to show that \(\mathtt{l}(x) >_\text{kbo}x\). Notice that it does not holds \((y + (z + w) >_\text{kbo}z + (y + w)\) because of the ordering of the variables.

  2. Let \(\mathtt{r}> \mathtt{l}\), \(w(\mathtt{r}) = 0\) and \(w(\mathtt{l}) = 1\). It holds that \(w\) is admissible. Let \(s \to t\) with \(s = C[\mathtt{r}^n(\mathtt{l}^k(t^\prime))]\) and \(t= C[\mathtt{l}^k(\mathtt{r}^m(t^\prime))]\). From the definition of \(w\), it holds that \(w(s) = w(t)\) since the number of occurrences of the function symbol \(\mathtt{l}\) is the same in \(s\) and \(t\). By applying the definition of \(>_\text{kbo}\), we get that we need to show \(\mathtt{r}^n(\mathtt{l}^k(t^\prime)) >_\text{kbo} \mathtt{l}^k(\mathtt{r}^m(t^\prime))\), which holds since \(\mathtt{r}> \mathtt{l}\).