28-11-2019

Let \(A\) and \(B\) be two terminating relations on the same set of terms. Show that if \(AB \subseteq BA\) then \(A \cup B\) is a terminating relation. Use well-founded induction.

We prove that \((A \cup B)^* \subseteq B^*A^*\) by well-founded induction on steps of \((A \cup B)^*\). The induction hypothesis is: \(t (\to_{A\cup B})^n t' \implies t \to_B^*\to_A^* t^\prime\). Without loss of generality suppose \(t \to_{A\cup B}^{n+1} t^\prime\) such that \(t \to_A t^{\prime\prime} \to_B (\to_{A \cup B})^{n-1} t^\prime\) for some \(n \in \mathbb{N}\). Then by hypothesis \(AB \subseteq BA\) it holds that there exists \(t^{\prime\prime\prime}\) such that \(t \to_B t^{\prime\prime\prime} \to_A (\to_{A \cup B})^{n-1} t^\prime\). By inductive hypothesis, since \(t^{\prime\prime\prime} (\to_{A \cup B})^n t^\prime\), \(t^{\prime\prime\prime} \to_B^* \to_A^* t^\prime\) and therefore \(t \to_B^* \to_A^* t^\prime\). Since \(A\) and \(B\) are terminating relations, \(B^*A^*\) is a terminating relation. It follows that \(A \cup B\) is terminating.

Given a strict order \(>\) on a set \(A\), we define the corresponding **multiset order** \(>_\text{mul}\) on \(\mathtt{Mult}(A)\) as follows: \(M >_\text{mul}N\) if and only if there exist \(X,Y \in \mathtt{Mult}(A)\) such that

\(\emptyset \not= X \subseteq M\);

\(N = (M \setminus X) \cup Y\);

\(\forall y \in Y\ \exists x \in X\ x > y\).

Order the multisets \(\{\!|\ 2 \ |\!\}\), \(\{\!|\ 1, 3 \ |\!\}\), \(\{\!|\ 1, 1, 1, 2 \ |\!\}\), \(\{\!|\ 2, 2, 2, 2 \ |\!\}\), \(\{\!|\ 1, 2 \ |\!\}\).

\[\begin{gathered} \{\!|\ 1, 3 \ |\!\}> \{\!|\ 2, 2, 2, 2 \ |\!\}> \{\!|\ 1, 1, 1, 2 \ |\!\}> \{\!|\ 1, 2 \ |\!\}> \{\!|\ 2 \ |\!\} \end{gathered}\]

Given a strict order \((A, >)\), define the following single-step relation on \(\mathtt{Mult}(A)\): \[\begin{gathered}
M >_{\text{mul}}^{1} N \Leftrightarrow \exists x \in M, Y \in \mathtt{Mult}(A). N = (M - \{
x \}) \cup Y \land \\
\forall y \in Y. x > y\end{gathered}\] Show that \(>_{\text{mul}}\) is the same as the transitive closure of \(>_{\text{mul}}^{1}\) (*hint:* show that each relation is included in the other using appropriate inductions). Conclude that \(>_{\text{mul}}\) is transitive.

By induction on the \({(>_{\text{mul}}^{1})}^{*}\) relation,

\(>_{\text{mul}}^{1} \subseteq >_{\text{mul}}\), take –in the definition of \(>_{\text{mul}}\)– \(X = \{\!|\ x \ |\!\}\).

\[\exists n. \forall m \leq n. >_{\text{mul}}^{m} \subseteq >_{\text{mul}}\] Assuming that we have \(M_{1}, M_{2}\) and \(M_{3}\) such that \[M_{1} <_{\text{mul}}^{n} M_{2} <_{\text{mul}}^{1} M_{3}\] we must show that \[M_{1} <_{\text{mul}} M_{3}\]

Applying definitions, we obtain, using induction hypothesis: \[\begin{aligned} M_{1} <_{\text{mul}} M_{2} \Rightarrow &\exists X_{1}, Y_{1} \\ &X_{1} \ne \emptyset, X_{1} \subseteq M_{2} \\ &M_{1} = (M_{2} - X_{1}) \cup Y_{1} \\ &\forall y_{1} \in Y_{1}. \exists x_{1} \in X_{1}. y_{1} < x_{1} \end{aligned}\] and \[\begin{aligned} M_{2} <_{\text{mul}}^{1} M_{3} \Rightarrow &\exists x_{2} \in M_{3}, Y_{2} \in \mathtt{Mult}(A) \\ &M_{2} = (M_{3} - \{ x_{2} \}) \cup Y_{2} \\ &\forall y_{2} \in Y_{2}. y_{2} < x_{2} \end{aligned}\] The objective is now to build \(X_{3}, Y_{3}\) such that \[\begin{aligned} X_{3} \ne \emptyset, X_{3} \subseteq M_{3}, \\ M_{1} = (M_{3} - X_{3}) \cup Y_{3} \\ \forall y_{3} \in Y_{3}. \exists x_{3} \in X_{3}. y_{3} < x_{3} \end{aligned}\]

The two equalities on \(M_{2}\) and \(M_{1}\) provide easily \[M_{1} = \left( (M_{3} - \{ x_{2} \}) \cup Y_{2} - X_{1} \right) \cup Y_{1}\]

Let \(X_{3} = \{\!|\ x_{2} \ |\!\}\cup (X_{1} - Y_{2})\) and \(Y_{3} = Y_{1} \cup Y_{2}\). We can verify that \[M_{3} = (M_{3} - X_{3}) \cup Y_{3}\] and we must verify that

\(\{\!|\ x_{2} \ |\!\}\cup (X_{1} - Y_{2}) \subseteq M_{3}\) which is true since, for any \(x\) in the multiset,

either \(x = x_{2}\), and \(x_{2} \in M_{3}\),

or \(x \in X_{1} - Y_{2}\); in that case, since \(X_{1} \subseteq M_{2}\), \(x \in M_{3}\) by definition of \(M_{3}\) and because \(x \ne \{ x_{2} \}\).

\(\forall y \in Y_{1} \cup Y_{2}. \exists x \in \{x_{2}\} \cup (X_{1} - Y_{2}). y < x\), if \(y \in Y_{2}\), then \(y < \{x_{2}\}\) and if \(y \in (X_{1} - Y_{2})\), then either \(\exists x \in X_{1} - Y_{2}. y < x\), or \(y < \{x_{2}\}\).

by induction on the size of multisets.

For the base case, it seems clear that for all \(a, N\), \(\{\!|\ a \ |\!\}>_{\text{mul}} N \Rightarrow \{\!|\ a \ |\!\}>_{\text{mul}}^{1} N\) (taking \(X = \{a\}\) in the definition).

let \(M >_{\text{mul}} N\) then by definition \(\exists X, Y\) such that \(N = (M - X) \cup Y\), \(X \ne \emptyset\), \(X \subseteq M\), and for all \(y\) in \(Y\), there is \(x\) such that \(y < x\). Let \(x_{m} = \max X\) in \(N' = M - \{\!|\ x_{m} \ |\!\}\). Clearly, \(M >_{\text{mul}}^{1} N'\).

If \(N = N'\), then \(M >_{\text{mul}}^{1} N\) and we have nothing to prove. Otherwise, \(N' >_{\text{mul}} N\). Therefore, \(x_{m} \in X\), and \(N = (N' - X') \cup Y\) i.e. \(N' >_{\text{mul}} N\). By induction hypothesis, we have \(N' {(>_{\text{mul}})}^{1} N\) and therefore \(M {(>_{\text{mul}}^{1})}^{*} N\).

In the following, let \(\Sigma\) be a finite signature, \(V\) a set of variables and \(T(\Sigma,V)\) the terms built from those sets.

Show that is not possible to prove termination using lexicographic path ordering of the following term rewrite system: \[\{\ \mathtt{a}(\mathtt{a}(x)) \to \mathtt{s}(x),\ \mathtt{s}(\mathtt{s}(x)) \to \mathtt{a}(x)\ \}\]

Suppose \(\mathtt{a}> \mathtt{s}\). Let \(s \to t\) with \(s = C[\mathtt{s}(\mathtt{s}(t^\prime)]\) and \(t=C[\mathtt{a}(t^\prime)]\). Then we need to prove that \(\mathtt{s}(\mathtt{s}(t^\prime)) >_\text{rpo}\mathtt{a}(t^\prime)\), which does not hold. If instead \(\mathtt{s}> \mathtt{a}\), then from the first rule we get \(\mathtt{a}(\mathtt{a}(t^\prime)) >_\text{rpo}\mathtt{s}(t^\prime)\) which, again, does not hold.

Show that the termination of the following rewriting system cannot be proven with lexicographic path order but can be proven with multiset path order. \[\begin{aligned} \mathtt{0}+ x &\to \mathtt{0}& \mathtt{0}\times x &\to x\\ \mathtt{s}(x) + y &\to \mathtt{s}(x + y) & \mathtt{s}(x) \times y &\to (y \times x) + y\end{aligned}\]

We need to impose the precedence \(\times > + > \mathtt{s}\). With this, the lexicographic path order cannot orient the last rule as it does not hold that \((\mathtt{s}(x),y) >_{\text{lex}} (y,x)\). Instead, it holds \(\{\!|\ \mathtt{s}(x), y\ |\!\} >_{\text{mul}} \{\!|\ y, x\ |\!\}\) since \(\mathtt{s}(x)\) dominates \(x\).

*For next week: simple termination, dependency pairs*

Questions 1 is independant from 2, 3 and 4.

Show that a transitive relation \(\rightslice\) on terms has the subterm property if and only if \[f(t_{1}, \dots, t_{n}) \rightslice t_{i}\] for all function symbols \(f\) of arity \(n \geq 1\), terms \(t_{1}, \dots, t_{n}\) and \(i \in \{1, \dots, n\}\).

Let \((w, w_{0})\) be an admissible weight function. Assume that \(f\) is of arity \(1\), \(w(f) = 0\) and that there is \(g\) such that \(f \not> g\). Prove that under this conditions \(>_\text{kbo}\) does not satisfy the subterm property.

Let \(>\) be a precedence and \((w, w_{0})\) an admissible weight function, show that \(t \in \mathsf{Var}(s)\) and \(s \ne t\) then \(s >_{\text{kbo}} t\).

Let \(>\) be a precedence and \((w, w_{0})\) an admissible weight function. Show that the Knuth-Bendix order \(>_{\text{kbo}}\) has the subterm property.

immediate, take, for any \(i\), \(C = f(t_{1}, \dots, \boxdot_{i}, \dots, t_{n})\).

by induction on the context \(C\). For initialisation, take \(C = f(t_{1}, \dots, \boxdot, \dots, t_{n})\). By assumption, \(C[t] \rightslice t\). Now assume \(C[t] = f(c_{1}, \dots, c_{n})\) and that there is \(i\) such that \(c_{i}[t] \rightslice t\). Then by assumption, \(C[t] \rightslice c_{i}[t]\). By induction hypothesis and transitivity of \(\rightslice\), \(C[t] \rightslice t\).

Let \(t = g(t_1,\dots,t_n)\) be an arbitrary term with root symbol \(g\), define \(s = f(t)\) and let \(s \to t\). Since \(w(f) = 0\) we have \(w(s) = w(t)\). Obviously, the first and third condition of KBO cannot hold, so \(>_\text{kbo}\) holds if and only if the second condition holds. But this cannot happen since \(f \not> g\). As \(t\) is a subterm of \(s\), the subterm property is therefore violated.

Because \(t \in \mathsf{Var}(s)\), the variable condition is clearly satisfied. Furthermore, \(w(s) \geq w(t)\). If \(w(s) = w(t)\) then there must be a unary function symbol \(f\) with \(w(f) = 0\) such that \(s = f^{n}(t)\) for some \(n > 0\). Hence \(s >_{\text{kbo}} t\) by definition of kbo. If \(w(s) > w(t)\), then \(s >_{\text{kbo}} t\).

We consider the following TRS: \[\begin{aligned} \mathtt{m}(x,\mathtt{0}) &\to 0 &&& \mathtt{m}(\mathtt{s}(x),\mathtt{s}(y)) &\to \mathtt{m}(x,y)\\ \mathtt{q}(\mathtt{0},\mathtt{s}(y)) &\to 0 &&& \mathtt{q}(\mathtt{s}(x),\mathtt{s}(y)) &\to \mathtt{s}(\mathtt{q}(\mathtt{m}(x,y), \mathtt{s}(y)))\\ \mathtt{p}(\mathtt{0},y) &\to y &&& \mathtt{p}(x,\mathtt{s}(y)) &\to \mathtt{s}(\mathtt{p}(x,y))\\ \mathtt{m}(\mathtt{m}(x,y),z) &\to \mathtt{m}(x,\mathtt{p}(y,z))\end{aligned}\]

Which rule makes the termination of this TRS not provable with KBO or RPO?

What are the defined symbols?

Compute the marked dependency pairs.

Draw the dependency graph approximation.

What are the inequalities that are enough to consider? What can instead be ignored?

Find a weakly monotonic polynomial interpretation on integers satisfying those inequalities.

\(\mathtt{q}(\mathtt{s}(x),\mathtt{s}(y)) \to \mathtt{s}(\mathtt{q}(\mathtt{m}(x,y), \mathtt{s}(y)))\), since the left-hand side of this rule is embedded in its right-hand side if \(y\) is instantiated with \(\mathtt{s}(x)\).

The set of defined symbols is \(\{\mathtt{m}, \mathtt{q}, \mathtt{p}\}\).

The marked dependency pairs are: \[\begin{aligned} 1:\ &(\mathtt{m}^\#(\mathtt{s}(x),\mathtt{s}(y)),\ \mathtt{m}^\#(x,y))\\ 2:\ &(\mathtt{q}^\#(\mathtt{s}(x),\mathtt{s}(y)),\ \mathtt{q}^\#(\mathtt{m}(x,y),\mathtt{s}(y)))\\ 3:\ &(\mathtt{q}^\#(\mathtt{s}(x),\mathtt{s}(y)),\ \mathtt{m}^\#(x,y))\\ 4:\ &(\mathtt{p}^\#(x,\mathtt{s}(y)),\ \mathtt{p}^\#(x,y))\\ 5:\ &(\mathtt{m}^\#(\mathtt{m}(x,y),z),\ \mathtt{m}^\#(x,\mathtt{p}(y,z)))\\ 6:\ &(\mathtt{m}^\#(\mathtt{m}(x,y),z),\ \mathtt{p}^\#(y,z)) \end{aligned}\]

Dependency graph approximation:

We need to consider the inequalities: \[\begin{aligned} \mathtt{m}(x,0) &\geq x\\ \mathtt{m}(\mathtt{s}(x),\mathtt{s}(y)) &\geq \mathtt{m}(x,y)\\ \mathtt{q}(0,\mathtt{s}(y)) &\geq 0\\ \mathtt{q}(\mathtt{s}(x),\mathtt{s}(y)) &\geq \mathtt{s}(\mathtt{q}(\mathtt{m}(x,y),\mathtt{s}(y)))\\ \mathtt{p}(0,y)&\geq y\\ \mathtt{p}(x,\mathtt{s}(y)) &\geq \mathtt{s}(\mathtt{p}(x,y))\\ \mathtt{m}(\mathtt{m}(x,y),z) &\geq \mathtt{m}(x,\mathtt{p}(y,z))\\\\ \mathtt{m}^\#(\mathtt{s}(x),\mathtt{s}(y)) &> \mathtt{m}^\#(x,y)\\ \mathtt{q}^\#(\mathtt{s}(x),\mathtt{s}(y)) &> \mathtt{q}^\#(\mathtt{m}(x,y),\mathtt{s}(y))\\ \mathtt{p}^\#(x,\mathtt{s}(y)) &> \mathtt{p}^\#(x,y)\\ \mathtt{m}^\#(\mathtt{m}(x,y),z) &> \mathtt{m}^\#(x,\mathtt{p}(y,z)) \end{aligned}\] Whereas the two inequalities that can be ignored are \(\mathtt{q}^\#(\mathtt{s}(x),\mathtt{s}(y)) > \mathtt{m}^\#(x,y)\) and \(\mathtt{m}^\#(\mathtt{m}(x,y),z) > \mathtt{p}^\#(y,z)\), that can be ignored since, looking at the dependency graph approximation, they correspond to nodes that don’t belongs to any loops. In fact, we just need to consider, for each strongly connected component, the \(\geq\) inequalities plus the \(>\) inequalities of that strongly connected component.

In this case, it’s easy to find a weakly polynomial interpretation over integers that satisfied all the inequalities, instead of considering separately each strongly connected component: \(\mathtt{P}_0 = 0\), \(\mathtt{P}_{\mathtt{s}}(X) = X + 2\), \(\mathtt{P}_{\mathtt{m}}(X,Y) = X + 1\), \(\mathtt{P}_\mathtt{q}(X,Y) = 2X\), \(\mathtt{P}_{\mathtt{m}^\#}(X,Y) = \mathtt{P}_{\mathtt{q}^\#}(X,Y) = X\), \(\mathtt{P}_{\mathtt{p}}(X,Y) = \mathtt{P}_{\mathtt{p}^\#}(X,Y) = X + Y\).

Consider the following TRS \[f\ 0 \to s\ 0 \quad f\ (s\ 0) \to s\ 0 \quad f\ (s\ (s\ x)) \to f\ (f\ (s\ x))\]

Compute the dependency pairs.

Prove the termination by constructing a suitable reduction pair based on a weakly monotone interpretation in \(\mathbb{N}\).

Is the system simply terminating?