# If I naively generalize the homeomorphic embedding relation for labeled finite trees in this way, do I still have a wqo?

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.

• It might be easier to answer your question, if you sketch what you mean by homeomorphic embedding over tree. – Martin Berger Jul 7 '18 at 9:53
• 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 Jul 7 '18 at 17:04

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.
• Well, $S$ should be assumed transitive. – Emil Jeřábek supports Monica Aug 16 '18 at 15:00
{"ft_lang_label":"__label__en","ft_lang_prob":0.87989116,"math_prob":0.9893762,"size":1858,"snap":"2019-51-2020-05","text_gpt3_token_len":539,"char_repetition_ratio":0.13268608,"word_repetition_ratio":0.08588957,"special_character_ratio":0.27825618,"punctuation_ratio":0.04481793,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9992205,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-01-19T18:10:38Z\",\"WARC-Record-ID\":\"<urn:uuid:73e4600f-6a45-44c6-9508-9f46b6859899>\",\"Content-Length\":\"138342\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:b016da03-9fb6-4b6c-9f5f-f2d95d49898f>\",\"WARC-Concurrent-To\":\"<urn:uuid:938e134f-1481-4787-869a-216286fe148c>\",\"WARC-IP-Address\":\"151.101.1.69\",\"WARC-Target-URI\":\"https://cstheory.stackexchange.com/questions/41166/if-i-naively-generalize-the-homeomorphic-embedding-relation-for-labeled-finite-t\",\"WARC-Payload-Digest\":\"sha1:QM4IHGKADFG6AVDKZJBR53PLQNI7TXYB\",\"WARC-Block-Digest\":\"sha1:NOXHDVZJRRIXMB3QQUUM6H7UL62XSVVN\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-05/CC-MAIN-2020-05_segments_1579250594705.17_warc_CC-MAIN-20200119180644-20200119204644-00297.warc.gz\"}"}