<p>Here's a nice property of WQOs:</p>

<blockquote>
  <p>If $R$ is a WQO on terms, and $S$ is another transitive relation such that
  $$ R\ \subseteq\ S$$
  Then $S$ is a WQO</p>
</blockquote>

<p><strong>Proof</strong>: Let $t_1,\ldots, t_n,\ldots$ be an infinite sequence of terms. Because $R$ is a WQO, there are $i, j$ with $i&lt;j$ such that $t_i\ R\ t_j$. But this implies $t_i\ S\ t_j$, so $S$ is a WQO as well.</p>

<p>This (somewhat counter-intuitive) result means you can always make your relation <strong>more</strong> permissive while preserving the WQO property.</p>

CC BY-SA 4.0
2018-08-16T15:00:25.817Z
Well, $S$ should be assumed transitive.
Emil Jeřábek
CC BY-SA 4.0
2018-08-16T15:22:34.950Z
@EmilJeřábek you are correct, good catch.
cody
CC BY-SA 4.0
2018-08-16T14:34:31.120Z
2018-08-16T15:23:13.993Z
2018-08-16T15:23:13.993Z
cody
<p>The homeomorphic embedding relation for trees as I understand it is a well-quasi-order (wqo) on trees when the label of a node determines the number of children of that node, and there are a finite number of such labels. A description of what (I hope) I'm referring to is in section 5.1 of <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/termination-combinators.pdf" rel="noreferrer">this article</a>.</p>

<p>I want to naively generalize this wqo to trees wherein the labels do not determine the number of children, for the purpose of runtime termination checking with states being said ill-behaved trees.</p>

<p>Assuming that I'm testing the homeomorphic embedding relation $\leq$ according to the rules (if something looks wrong here, then trust the linked the paper and correct me instead):</p>

<p>$l \leq r = \begin{array}\\
c(s_1 \ldots s_n) \leq c(t_1 \ldots t_n) &amp; \text{if} &amp; l = c(s_1 \ldots s_n) \text{ and } r = c(t_1 \ldots t_n) \text{ and } s_1 \leq t_1 \ldots s_1 \leq t_n \\
s \leq c(t_1 \ldots t_n) &amp; \text{if} &amp; l = x(s_1 \ldots s_n) \text{ and } r = c(t_1 \ldots t_n) \text{ and } \exists i.s\leq t_i \\
false &amp;&amp; \text{otherwise}
\end{array}$</p>

<p>where $c$ is a label, $x$ is some other label, and $s_i$ and $t_i$ are subtrees (and the $c(\ldots)$ notation is a tree construction with $c$ as the root of a (sub)tree and $\ldots$ that (sub)tree's children).</p>

<p>Would I still have a wqo if I simply said the relation <strong>holds</strong> if I <em>ever</em> encounter (in the course of checking membership in the relation) a scenario where I'm checking $c(\ldots s_m) \leq c(\ldots t_n)$ and $m \neq n$?</p>

<p>My gut says that I still would have a wqo (the 'dives in' rule should force me to make the arity check and blow the whistle whenever the vanilla homeomorphic embedding would be too lenient on labels-with-inconsistent-children-counts, and catch the case of an infinite sequence of widening trees), but as with any procedural hack on a mathematical relation I feel a bit too dumb to be sure.</p>

CC BY-SA 4.0
2018-07-07T09:53:39.207Z
It might be easier to answer your question, if you sketch what you mean by *homeomorphic embedding over tree*.
Martin Berger
CC BY-SA 4.0
2018-07-07T17:04:00.353Z
I think I shouldn't have used the word 'over' (sorry!). I just mean the test given in the rules; I've also added a link to an article that describes it in a section. EDIT: just realized that the rules I wrote are really, really opaque...
user
<tree><order-theory>
If I naively generalize the homeomorphic embedding relation for labeled finite trees in this way, do I still have a wqo?
user
# If I naively generalize the homeomorphic embedding relation for labeled finite trees in this way, do I still have a wqo?

(Asked by: username_0 on 2018-07-07)

The homeomorphic embedding relation for trees as I understand it is a well-quasi-order (wqo) on trees when the label of a node determines the number of children of that node, and there are a finite number of such labels. A description of what (I hope) I'm referring to is in section 5.1 of [this article](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/termination-combinators.pdf).

I want to naively generalize this wqo to trees wherein the labels do not determine the number of children, for the purpose of runtime termination checking with states being said ill-behaved trees.

Assuming that I'm testing the homeomorphic embedding relation $\leq$ according to the rules (if something looks wrong here, then trust the linked the paper and correct me instead):

$l \leq r = \begin{array}\\
c(s\_1 \ldots s\_n) \leq c(t\_1 \ldots t\_n) & \text{if} & l = c(s\_1 \ldots s\_n) \text{ and } r = c(t\_1 \ldots t\_n) \text{ and } s\_1 \leq t\_1 \ldots s\_1 \leq t\_n \\
s \leq c(t\_1 \ldots t\_n) & \text{if} & l = x(s\_1 \ldots s\_n) \text{ and } r = c(t\_1 \ldots t\_n) \text{ and } \exists i.s\leq t\_i \\
false && \text{otherwise}
\end{array}$

where $c$ is a label, $x$ is some other label, and $s\_i$ and $t\_i$ are subtrees (and the $c(\ldots)$ notation is a tree construction with $c$ as the root of a (sub)tree and $\ldots$ that (sub)tree's children).

Would I still have a wqo if I simply said the relation **holds** if I *ever* encounter (in the course of checking membership in the relation) a scenario where I'm checking $c(\ldots s\_m) \leq c(\ldots t\_n)$ and $m \neq n$?

My gut says that I still would have a wqo (the 'dives in' rule should force me to make the arity check and blow the whistle whenever the vanilla homeomorphic embedding would be too lenient on labels-with-inconsistent-children-counts, and catch the case of an infinite sequence of widening trees), but as with any procedural hack on a mathematical relation I feel a bit too dumb to be sure.

**Tags:** tree, order-theory
> **Comments:**
> **username_1**: It might be easier to answer your question, if you sketch what you mean by *homeomorphic embedding over tree*.  
> **username_0**: I think I shouldn't have used the word 'over' (sorry!). I just mean the test given in the rules; I've also added a link to an article that describes it in a section. EDIT: just realized that the rules I wrote are really, really opaque...  

---

## 1 answers

### Answer by username_2 on 2018-08-16. Score: 5 | Accepted answer

Here's a nice property of WQOs:

> If $R$ is a WQO on terms, and $S$ is another transitive relation such that
> $$ R\ \subseteq\ S$$
> Then $S$ is a WQO

**Proof**: Let $t\_1,\ldots, t\_n,\ldots$ be an infinite sequence of terms. Because $R$ is a WQO, there are $i, j$ with $i

This (somewhat counter-intuitive) result means you can always make your relation **more** permissive while preserving the WQO property.

> **Comments:**
> **username_3**: Well, $S$ should be assumed transitive.  
> **username_2**: @EmilJeřábek you are correct, good catch.  

---

