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.

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.

  • $\begingroup$ It might be easier to answer your question, if you sketch what you mean by homeomorphic embedding over tree. $\endgroup$ Commented Jul 7, 2018 at 9:53
  • $\begingroup$ 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... $\endgroup$
    – user
    Commented Jul 7, 2018 at 17:04

1 Answer 1


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<j$ such that $t_i\ R\ t_j$. But this implies $t_i\ S\ t_j$, so $S$ is a WQO as well.

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

  • $\begingroup$ Well, $S$ should be assumed transitive. $\endgroup$ Commented Aug 16, 2018 at 15:00
  • $\begingroup$ @EmilJeřábek you are correct, good catch. $\endgroup$
    – cody
    Commented Aug 16, 2018 at 15:22

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.