
\documentclass{beamer}

\usepackage{latexsym,amssymb,mathdots}

\usepackage{verbatim}

\usepackage[dvipsnames,svgnames,xcolor=pst]{pstricks}

\newcommand{\olive}{\color{green}}
\newcommand{\azure}{\color{blue}}
\newcommand{\purple}{\color{violet}}
\newcommand{\bordeaux}{\color{red}}

\usepackage{pst-node,pst-tree}

\newcommand{\bA}{{\blue A}}
\newcommand{\rB}{{\red B}}
\newcommand{\pE}{{\purple E}}
\newcommand{\dn}[2]{\dotnode[dotscale=2,linecolor=yellow](#1){#2}}
\newcommand{\aA}[2]{\nccurve[linewidth=2pt,linecolor=red,linestyle=solid,angleA=0,angleB=180]{->}{#1}{#2}
} %\naput*[npos=0.5]{\red$A$}}
\newcommand{\aB}[2]{\nccurve[linewidth=2pt,linecolor=blue,linestyle=dashed,angleA=0,angleB=180]{->}{#1}{#2}
} %\nbput*[npos=0.5]{\blue$B$}}
\newcommand{\cA}{\pscircle[linecolor=red,fillcolor=red,fillstyle=solid]{0.3}}
%{\white$A$}}
\newcommand{\cB}{\pscircle[linecolor=blue,fillstyle=crosshatch*,fillcolor=blue]{0.5}}
%{\white$B$}}
\newcommand{\cC}{\pscircle[linecolor=green,fillstyle=hlines*,hatchsep=2pt,fillcolor=green]{0.7}}
%{\white$C$}}
\newcommand{\cD}{\pscircle[linecolor=violet,fillstyle=vlines*,fillcolor=violet]{0.9}}
%{\white$D$}}

\newcommand{\trun}[3]{(#1 \cup #2 \cup #3)} % {(#1 \!\cup\! #2 \!\cup\! #3)}
\newcommand{\trum}[3]{#1 \cup #2 \cup #3} % {#1 \!\cup\! #2 \!\cup\! #3}
\newcommand{\biun}[2]{(#1 \cup #2)} % {(#1 \!\cup\! #2)}

\newcommand{\plus}{{\scriptscriptstyle +}}

\newcommand{\removed}[1]{}

\title{Well-Founded Unions}
\author{Jeremy Dawson \and Nachum Dershowitz \and Rajeev Gor\'e}

\begin{document}
\maketitle

\begin{frame}{Problem}
Under what ``combinatorial'' conditions
is the union of \emph{well-founded relations} sure to be well-founded?

\bigskip
\begin{itemize}
\item\emph{Well-founded (the paper)}: No infinite forward chains
($x_0 > x_1 > x_2 > \ldots$, $(x_0, x_1), (x_1, x_2), \ldots \in R$)

\item\emph{Well-founded (Isabelle)}: No infinite backward chains
($\ldots < x_2 < x_1 < x_0$), $(x_1, x_0), (x_2, x_1), \ldots \in R$)

\item\emph{Well-founded (both)}: No infinite \emph{descending} chains

\item\emph{relation composition (the paper)} \\
($x BA z$ iff there's a $y$ such that $xBy$ and $yAz$)

\item\emph{relation composition (Isabelle)} 
($(x, z) \in B \circ A$ iff \\
there's a $y$ such that $(x, y) \in A$ and $(y, z) \in B$)
\end{itemize}
\end{frame}

\begin{frame}{Two Lines}
\begin{figure}[t]
\begin{pspicture}(-1,-0.5)(10,3)
\psset{origin={0,0},linewidth=1.5pt,linecolor=red,linearc=0.85}
\psline{->}(2.1,-0)(3.9,-0)
\psline{->}(4.1,0)(5.9,0)
\psline{->}(6.1,-0)(7.9,-0)
\psline{->}(2.1,0.1)(2.9,0.8)
\psline{->}(3.1,1.0)(3.9,1.7)
\psline{->}(4.1,1.9)(4.9,2.6)
\psline{->}(4.1,0.1)(4.9,0.8)
\psline{->}(5.1,1.0)(5.9,1.7)
\psline{->}(6.1,0.1)(6.9,0.8)
\rput(8.5,0){$\cdots$}\rput(7,1.5){$\cdots$}\rput(5.3,3.1){$\iddots$}
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed}
\psline{->}(3.1,0.8)(3.9,0.1)
\psline{->}(4.1,1.7)(4.9,1.0)
\psline{->}(5.1,0.8)(5.9,0.1)
\psline{->}(6.1,1.7)(6.9,1.0)
\psline{->}(7.1,0.8)(7.9,0.1)
\psline{->}(5.1,2.6)(5.9,1.9)
\rput(2,0){$\olive\bullet$}\rput(4,0){$\olive\bullet$}\rput(6,0){$\olive\bullet$}\rput(8,0){$\olive\bullet$}
\rput(3,0.9){$\olive\bullet$}\rput(5,0.9){$\olive\bullet$}\rput(7,0.9){$\olive\bullet$}
\rput(4,1.8){$\olive\bullet$}\rput(6,1.8){$\olive\bullet$}\rput(5,2.7){$\olive\bullet$}
\end{pspicture}
\end{figure}
\end{frame}

\begin{frame}{Immortality}
\begin{itemize}
\item {\red Have pass for unlimited  Red travel}
\item {\blue Have pass for unlimited Blue travel}
\item Can't ride forever on just one
\item Want to ride forever on the combination
\end{itemize}
\end{frame}

\begin{frame}{Mortal Union}
\begin{center}
\begin{pspicture}(0,-0.8)(10,0.7)
\dn{0,0}{x}
\dn{2,0}{y}
\dn{4,0}{z}
\dn{6,0}{a}
\dn{8,0}{b}
\aA x y \aB y z \aA z a \aB a b
\end{pspicture}
\end{center}
\end{frame}

\begin{frame}{Immortal Union}

\begin{figure}[t]
\begin{pspicture}(0,-0.5)(10,1.0)
\psset{origin={0,0},linewidth=1.5pt,linecolor=red,linearc=0.85}
\psline{->}(2.1,-0.1)(3,-0.5)(3.9,-0.1)
\psline{->}(6.1,-0.1)(7,-0.5)(7.9,-0.1)
\rput(10.5,0){$\cdots$}
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed}
\psline{->}(4.1,0)(5.9,0)
\psline{->}(8.1,0)(9.9,0)
\psline{<-}(2.1,0.1)(3,0.5)(3.9,0.1)
\psline{<-}(6.1,0.1)(7,0.5)(7.9,0.1)
\rput(2,0){$\olive\bullet$}\rput(4,0){$\olive\bullet$}\rput(6,0){$\olive\bullet$}\rput(8,0){$\olive\bullet$}\rput(10,0){$\olive\bullet$}
\end{pspicture}
\end{figure}
\end{frame}

\begin{frame}{Previous result --- Jumping}

(Always assuming $A,B,C,\ldots$ each individually well-founded).

The union $A\cup B$ is well-founded if
the following relatively powerful condition, called \emph{Jumping}, holds.
\begin{align}\label{jump}
BA & \subseteq A (A\cup B)^\ast \cup B \;. \tag{$\ast$}
\end{align}
% Juxtaposition is being used for composition 
% ($x BA z$ iff there's a $y$ such that $xBy$ and $yAz$)
% and the asterisk for the reflexive-transitive closure
% ($x B^\ast z$ iff there are $y_0,y_1,\ldots,y_n$, $n\geq 0$,
% such that $x = y_0 B y_1 B \cdots B y_n = z$).

\end{frame}

\begin{frame}{Proof --- first approach (Dershowitz)}
If the union is not well-founded, construct an infinite chain which
\begin{itemize}
\item[(1)] always prefers an $A$-step to a $B$-step, and
\item[(2)] when there is no choice of an $A$-step,
choose a $B$-step to an $A$-minimal endpoint
(exists as $A$ is well-founded)
\end{itemize}

Then, as both $A$ and $B$ are both well-founded, 
an $A$-step must eventually be followed by a $B$-step, and vice-versa.

So we have a $B$-step followed immediately by an $A$-step.
$$x \stackrel B \longrightarrow y \stackrel A \longrightarrow z 
  \longrightarrow \cdots$$
But since $BA \subseteq A (A\cup B)^\ast \cup B$
we could replace this by 
$$x \stackrel A \longrightarrow y' \stackrel {(A \cup B)^*} \longrightarrow z
  \longrightarrow \cdots$$
(contradicting (1) above)
or by 
$$x \stackrel B \longrightarrow z \longrightarrow \cdots$$
(contradicting (2) above)

\end{frame}

\begin{frame}{Proof --- second approach (suits Isabelle)}

Define an \emph{immortal} point to be one from which there is an infinite
descending chain. 

Choose an immortal point $x$ which is
\begin{itemize}
\item[(1)] $A$-minimal (as $A$ is well-founded), and
\item[(2)] $B$-minimal (among $A$-minimal points) (as $B$ is well-founded)
\end{itemize}

Consider an infinite descending chain from $x$.
By (1), its first step must be in $B$.  Choose it so that its endpoint $y$
is $A$-minimal (among points in the chain).
By (2), $y$, though immortal, is not $A$-minimal immortal.
So we have $z$, such that 
$$x \stackrel B \longrightarrow y \stackrel A \longrightarrow z 
  \longrightarrow \cdots$$

From here, argument as before.

\end{frame}

\begin{frame}{The extended Jumping Theorem}

Define $B^\sharp$ to be $B$, \emph{excepting} instances like 
$x \stackrel B \longrightarrow y$ \\
where $x$ permits $A$, then immortality
$$x \stackrel A \longrightarrow z 
  \stackrel {(A \cup B)^\infty} \longrightarrow \ldots$$

Then if $A$ and $B^\sharp$ are well-founded, and (as before)
$$BA \subseteq A (A\cup B)^\ast \cup B$$
then $A\cup B$ is well-founded.

Proof: similar to above, except choose $x$ which is
\begin{itemize}
\item[(1)] $A$-minimal (as before), and
\item[(2)] $B^\sharp$-minimal (among $A$-minimal points)
\end{itemize}
Then it turns out that first step of infinite descending chain from $x$,
which must be in $B$ (as above) is in fact in $B^\sharp$, so (as in proof above)
is not $A$-minimal immortal --- proof continues as above.
\end{frame}

\begin{frame}{A weaker condition not enough}
How about if 
$$BA \subseteq A (A\cup B)^\ast \cup B^+$$

{\Huge \color{red} A \color{blue} B}

\begin{center}
\scalebox{2}{
\begin{pspicture}(-1,-0.8)(5,0.5)
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed,
  linearc=0.85,origin={-2.5,0}}
\dn{2,0}{x}
\dn{4,0}{x}
\dn{6,0}{x}
\psline{->}(2.1,-0.1)(3,-0.5)(3.9,-0.1)
\psline{->}(4.1,-0.1)(5,-0.5)(5.9,-0.1)
\psset{linecolor=red,linestyle=solid}
\psline{<-}(2.1,0.1)(4,0.5)(5.9,0.1)
\psline{->}(4.1,0)(5.9,0)\end{pspicture}
}
\end{center}

\end{frame}

\begin{comment}{How about 3 well-founded relations?}

Clearly we can iterate this result (in two ways, here is one)
If $$CB \subseteq B (B\cup C)^\ast \cup C$$
then $B \cup C$ is well-founded.
And if $$(B \cup C)A \subseteq A (A\cup (B \cup C))^\ast \cup (B \cup C)$$
then $A \cup (B \cup C)$ is well-founded.

\end{comment}

\begin{frame}{New result for 3 well-founded relations}
Clearly we can iterate this result (in two ways, here is one)
If $$CB \subseteq B (B\cup C)^\ast \cup C$$
then $B \cup C$ is well-founded.
And if $$(B \cup C)A \subseteq A (A\cup (B \cup C))^\ast \cup (B \cup C)$$
then $A \cup (B \cup C)$ is well-founded.

\begin{theorem}[Tripartite, Dershowitz]\label{thm:tripartite}
The union $\trum{A}{B}{C}$ {of well-founded relations $A$, $B$, and $C$} is well-founded if
\begin{align}
\biun{B}{C} A & \subseteq A\trun{A}{B}{C}^\ast \cup B \cup C \notag \\
CB & \subseteq A\trun{A}{B}{C}^\ast \cup B^\plus \cup C \notag
\end{align}
\end{theorem}

% Compare the conditions of previous slide
% \begin{align}
% \biun{B}{C} A & \subseteq A(A\cup (B \cup C))^\ast \cup (B \cup C) \notag \\
% CB & \subseteq B (B\cup C)^\ast \cup C \notag
% \end{align}

\end{frame}

\begin{frame}{Can we get the result stronger than both?}

\begin{align}
\biun{B}{C} A & \subseteq A\trun{A}{B}{C}^\ast \cup B \cup C \notag \\
CB & \subseteq A\trun{A}{B}{C}^\ast \cup B (B\cup C)^\ast \cup C \notag
\end{align}

% Dershowitz's example
{\Huge NO! \color{red} A \color{blue} B \color{green} C}

\begin{center}
\psset{arrowsize=1pt 3}
\begin{pspicture}(-4,0)(4,2)
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=3pt,linecolor=red,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=2]{->}(-0.9,0.1)(1.4,0.9) % x->y
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,linearc=2]{->}(1.6,0.9)(3.9,0) % y->z
\rput(-4,0){$\bullet$}\rput(-1,0){$\bullet$}\rput(1.5,1){$\bullet$}\rput(4,0){$\bullet$} % vxyz
\end{pspicture}
\end{center}

\end{frame}

\begin{frame}{Can we get the result stronger than both?}

\begin{align}
\biun{B}{C} A & \subseteq A\trun{A}{B}{C}^\ast \cup B \cup C \notag \\
CB & \subseteq A\trun{A}{B}{C}^\ast \cup B (B\cup C)^\ast \cup C \notag
\end{align}

% my example
{\Huge NO! \color{red} A \color{blue} B \color{green} C}

\begin{center}
\psset{arrowsize=1pt 3}
\begin{pspicture}(-4,0)(4,2)
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=red,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=2]{->}(-0.9,0)(1.5,+0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\rput(-4,0){$\bullet$}\rput(-1,0){$\bullet$}\rput(4,0){$\bullet$} % vxyz
\end{pspicture}
\end{center}

\end{frame}

\begin{frame}{Proofs for 3 well-founded relations}
\begin{theorem}[Tripartite, Dershowitz]\label{thm:tripartite}
The union $\trum{A}{B}{C}$ {of well-founded relations $A$, $B$, and $C$} is well-founded if
\begin{align}
\biun{B}{C} A & \subseteq A\trun{A}{B}{C}^\ast \cup B \cup C \notag \\
CB & \subseteq A\trun{A}{B}{C}^\ast \cup B^\plus \cup C \notag
\end{align}
\end{theorem}

Original proof (Dershowitz): 
construct an infinite chain, preferring $A$ at each step.
Then, can use first condition to absorb any
$A$-step following a $B$- or $C$-step.
(Only finitely many consecutive $A$-step s as $A$ is well-founded).
So we have infinitely many $B$- or $C$-steps, from points where $A$ cannot lead
to an infinite chain.  

If any $C$-step can be avoided by taking a sequence of
$B$-steps to a later point in the chain, take that route instead. 
Then the chain, if infinite, as $B$, $C$ are well-founded,
has occurrences of $CB$, which can be replaced by $C$,
% as we have excluded $A\trun{A}{B}{C}^\ast$ and $B^\plus$.
as $A\trun{A}{B}{C}^\ast$ and $B^\plus$ are not possible.

\end{frame}

\begin{frame}{Splitting up the proof}
% wf_tri_lem_BCmn, wfp_BC_alt
\begin{lemma}[Tripartite Step]
Let $C^\flat$ be $C$, \emph{excepting} instances like 
$x \stackrel C \longrightarrow y$ \\
where $x$ permits $A$, then $X \cup B \cup C$-immortality
$$x \stackrel A \longrightarrow z 
  \stackrel {(X \cup B \cup C)^\infty} \longrightarrow \ldots$$
(At present, $X$ is $A$)

Then, if $B$ and $C^\flat$ are well-founded, and 
$$CB \subseteq A\trun{X}{B}{C}^\ast \cup B^\plus \cup C$$
then $B \cup C^\flat$ is well-founded.
\end{lemma}

Proof: similar to extended Jumping Theorem.

Our original formulation of this had $X = A$ and assumed $C$ rather than
$C^\flat$ is well-founded.  
Generalising it to $X$ (not necessarily equal to $A$) is absolutely trivial;
generalising it from $C$ to $C^\flat$ being well-founded is similar to 
extending the Jumping Lemma to require only that $B^\sharp$ (rather than $B$)
is well-founded.

\end{frame}

\begin{frame}{Proof of Tripartite Theorem}
As $B$, $C$ and so $C^\flat$ are well-founded,
the Tripartite Step lemma gives $B \cup C^\flat$ is well-founded.

Then, extended Jumping Theorem applied to $B \cup C$ instead of $B$ says: \\
if $A$ and $(B \cup C)^\sharp$ are well-founded, and (as before)
$$(B \cup C)A \subseteq A (A\cup (B \cup C))^\ast \cup (B \cup C)$$
then $A\cup (B \cup C)$ is well-founded.

So all we need to show is that if $B \cup C^\flat$ is well-founded then
$(B \cup C)^\sharp$ --- this follows from the definition

\end{frame}

\begin{frame}{Quadripartite Theorem}
\begin{theorem}[Quadripartite]
The union $A\cup B\cup C\cup D$
{of well-founded relations $A$, $B$, $C$ and $D$} is well-founded if
\begin{align}\nonumber
(B \cup C \cup D) A &\subseteq A (A \cup B \cup C \cup D)^\ast \cup B \cup C \cup D\\
(C \cup D) B &\subseteq A (A \cup B \cup C \cup D)^\ast \cup B^\plus \cup C \cup D\\
D C &\subseteq A (A \cup B \cup C \cup D)^\ast \cup C^\plus \cup D\;.
\end{align}
\end{theorem}

This can be extended to any number of relations.

This was discovered only because we had to reformulate the proof of the
Tripartite Theorem (splitting it up into separate lemmas) to enable us
to formulate it in Isabelle.

\end{frame}

\begin{frame}{Proof of Quadripartite Theorem}

We need to generalise the earlier definitions $C^\flat$ and $B^\sharp$.

Let $B^{Q\sharp S}$ be $B$, \emph{excepting} instances like 
$x \stackrel B \longrightarrow y$ \\
where $x$ permits $Q$, then $S$-immortality
$$x \stackrel Q \longrightarrow z \stackrel {S^\infty} \longrightarrow \ldots$$

So, of our earlier definitions,
$B^\sharp = B^{A\sharp A\cup B}$ and
$C^{\flat} = C^{A\sharp X\cup B\cup C}$.

Now, since $D$ is well-founded, so is $D^{A\sharp (A \cup B) \cup C \cup D}$,
and $C$ is well-founded,
so, by the Tripartite Step lemma (with $X := A \cup B, B := C, C := D$),
$C \cup D^{A\sharp (A \cup B) \cup C \cup D}$ is well-founded.
Therefore 
$(C \cup D)^{A\sharp (A \cup B) \cup C \cup D}$ is well-founded.

As $B$ is well-founded, by the Tripartite Step lemma 
(with $X := A, B := B, C := C \cup D$), 
$B \cup (C \cup D)^{A\sharp A \cup B \cup (C \cup D)}$ is well-founded
and so 
$(B \cup C \cup D)^{A\sharp A \cup B \cup (C \cup D)}$ is well-founded.

That is, $(B \cup C \cup D)^\sharp$ is well-founded,
so by the extended Jumping Theorem, 
$A \cup (B \cup C \cup D)$ is well-founded, as required.

\end{frame}

\begin{frame}{Further Conjectures}

The answer to the question whether the following conditions suffice in the quadripartite case has so far eluded us:
\begin{align*}
(B \cup C \cup D) A &\subseteq A (A \cup B \cup C \cup D)^\ast \cup B \cup C \cup D \\
(C \cup D) B &\subseteq A (A \cup B \cup C \cup D)^\ast \cup B^\plus \cup C \cup D \\
D C &\subseteq B (B \cup C \cup D)^\ast \cup C^\plus \cup D \;.
\end{align*}

We have the following about any counterexample
(ie, where these conditions hold, $A,B,C,D$ are well-founded,
but not their union):
\begin{itemize}
\item $A \cup B$ is not well-founded; for, if it were,
then the Tripartite Theorem (for relations $A \cup B$, $C$ and
$D$) would give us well-foundedness of the union.
\item % suphash (C Un D) A (A Un (B Un (C Un D)))
  $(C \cup D) ^ {A \sharp A \cup B \cup (C \cup D)}$
  is not well-founded;
  for, if it were, then
  $(B \cup (C \cup D)) ^ {A \sharp A \cup B \cup (C \cup D)}=(B \cup C \cup D)^\sharp$
  would also be well-founded by the Tripartite Step Lemma, whence
  the union would also be by the extended Jumping Theorem.
\end{itemize}
Sadly, these facts haven't helped us find a counterexample.

\end{frame}




\end{document}

