TRIPARTITE UNIONS

NACHUM DERSHOWITZ

This note concerns conditions under which the union of several wellfounded (binary) relations is also well-founded.^{1}

To garner insight, we tackle just three relations, A, B, and C, over some underlying set V. Let

{A|B}

denote A ∪ B, and so on for other unions of relations. And let juxtaposition indicate composition of relations and superscript ∗ signify transitive closure. We’ll refer to the relations as “colors”.

Theorem 1 (Ramsey). The union {A|B|C} is well-founded if

(1)  {A|B|C}{A|B|C} ⊆ {A|B|C}

Proof. The infinite version of Ramsey’s Theorem applies when the union is transitive, so that every two (distinct) nodes within an infinite chain in the union of the colors has a colored (directed) edge. Then, there must lie an infinite monochrome subchain within any infinite chain, contradicting the well-foundedness of each color alone.^{2} □

Only three of the nine cases are actually needed for the limited outcome that we are seeking (an infinite monochromic path, rather than a clique—as in Ramsey’s Theorem), as we observe next.

Theorem 2. The union {A|B|C} is well-founded if

(2)  BA ∪ CA ∪ CB ⊆ {A|B|C} .

Date: December 19, 2017.

1By well-founded, we mean the absence of infinite forward-pointing paths.

For some of the history of well-foundedness based on Ramsey’s Theorem, see Pierre Lescanne’s Rewriting List, contributions 38–41 at http://www.ens-lyon.

fr/LIP/REWRITING/CONTRIBUTIONS and Andreas Blass and Yuri Gurevich, “Program Termination and Well Partial Orderings”, ACM Transactions on Computational Logic 9(3), 2008 (available at http://research.microsoft.com/en-us/um/ people/gurevich/Opera/178.pdf).

2See Alfons Geser, Relative Termination, Ph.D. dissertation, Fakultät fur̈ Mathematik und Informatik, Universität Passau, Germany, 1990 (Report 91-03, Ulmer Informatik-Berichte, Universität Ulm, 1991; available at http://homepage.cs.

uiowa.edu/~astump/papers/geser_dissertation.pdf).

Proof. When the union is not well-founded, there is an infinite path X = {x_{i}}_{i} with each edge from x_{i} to X_{i+1} one of A, B, or C. Extract a maximal subsequence {x_{i_{j}}}_{j} of X such that x_{i_{j}} A x_{i_{j+1}} for each j. If it’s finite, then repeat at the first opportunity in the tail. If any is infinite, we have our contradiction. If they’re all finite, then consider the first occurrence of x {B|C} y A z. Since we could not take an Astep from x, or we would have, the conditions tell us that x {B|C} z. Swallowing up all such (non-initial) A-steps in this way, we are left with an infinite chain in B ∪C, for which we also know that no A-steps are possible anywhere. Now extract maximal B-chains and then erase them, replacing x C y B z with x C z (A- and B-steps having been precluded), leaving an infinite chain colored purely C. □

Corollary 1. If A, B, and C are transitive and

BA ∪ CA ∪ CB ⊆ {A|B|C} ,

then, whenever there is an infinite path in the union {A|B|C}, there is an infinite monochromatic clique.

We can do considerably better than the previous theorem:

Theorem 3 (Tripartite). The union {A|B|C} is well-founded if

(3)  {B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C
CB ⊆ A{A|B|C}^{∗} ∪ BB^{∗} ∪ C .

Let’s call the existence of an infinite outgoing chain in the union {A|B|C} immortality.

Proof. We first construct an infinite chain X = {x_{i}}_{i}, in which an A-step is always preferred over B or C, as long as immortality is maintained. To do this, we start with an immortal element x_{0} ∈ V. At each stage in the construction, if the chain so far ends in x_{i}, we look to see if there is any y such that x_{i} A y and from which proceeds some infinite chain in the union, in which case y is chosen to be x_{i+1}. Otherwise, x_{i+1} is any immortal element z such that x_{i} B z or x_{i} C z.

If there are infinitely many B’s and/or C’s in X, use them—by means of the first condition—to remove all subsequent A-steps, leaving only B- and C-steps going out of points from which A leads of necessity to mortality. From what remains, if there is any C-step at a point where one could take one or more B-steps to anyplace later in the chain, take the latter route instead. What remains now are C-steps at points where BB^{∗} detours are also precluded. If there are infinitely many such C-steps, then applying the condition for CB will result in a pure C-chain, because neither A{A|B|C}^{∗} nor BB^{∗} are options. □

Dropping C from the conditions of the previous theorem, one gets the jumping criterion for well-foundedness of the union of two well-founded relations A and B:^{3}

BA ⊆ A{A|B}^{∗} ∪ B .

Applying this criterion twice, one gets somewhat different (incomparable) conditions for well-foundedness.

Theorem 4 (Jumping). The union {A|B|C} is well-founded if

(4)  BA ⊆ A{A|B}^{∗} ∪ B
C{A|B} ⊆ {A|B}{A|B|C}^{∗} ∪ C .

Proof. The first inequality is the jumping criterion. The second is the same with C for B and {A|B} in place of A. □

For two relations, jumping provides a substantially weaker criterion for well-foundedness than does the appeal to Ramsey. But for three, whereas jumping allows more than one step for BA (in essence, AA^{∗}B^{∗}), it doesn’t allow for C, which Ramsey does.

Switching rôles, start with jumping for {B|C} before combining with A, we get slightly different conditions yet:

Theorem 5 (Jumping). The union {A|B|C} is well-founded if

(5)  CB ⊆ B{B|C}^{∗} ∪ C
{B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C .

Both this version of jumping and our tripartite condition allow

{B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C
CB ⊆ BB^{∗} ∪ C .

They differ in that jumping also allows

CB ⊆ B{B|C}^{∗} ,

whereas tripartite has

CB ⊆ A{A|B|C}^{∗}

instead.

3See Henk Doornbos and Burghard von Karger, “On the Union of Well-Founded Relations”, Logic Journal of the IGPL 6(2), pp. 195–201, 1998 (available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.

28.8953&rep=rep1&type=pdf). The property is called “jumping” in Nachum Dershowitz, “Jumping and Escaping: Modular Termination and the Abstract Path Ordering”, Theoretical Computer Science 464, pp. 35–47, 2012 (available at http:// nachum.org/papers/Toyama.pdf).

Sadly, we cannot have the best of both worlds. Let’s color edges A, B, and C with (solid) azure, (dotted) black, and (dashed) crimson ink, respectively. The graph

\begin{matrix}• \\ • \\ • \\ • \end{matrix}

only has multicolored loops despite satisfying

\begin{aligned}\{B|C\}A & ⊆ & C \\ CB & ⊆ & A ∪ B\{B|C\}^{∗} . \end{aligned}

Even

\begin{aligned}\{B|C\}A & ⊆ & C \\ CB & ⊆ & B\{A|B\}^{∗} \end{aligned}

doesn’t work. To wit, the double loop in

\begin{matrix}• \\ • \\ • \end{matrix}

harbors no monochrome subchain. By the same token,

\begin{matrix}• \\ • \\ • \end{matrix}

counters the putative hypothesis

\begin{aligned}BA ∪ CB & ⊆ & C \\ CA & ⊆ & BA^{∗} . \end{aligned}