\documentclass[serif,xcolor=pdftex,dvipsnames,table]{beamer}
\usetheme{Boadilla}
\usepackage{fourier}
\usepackage{stmaryrd,mathdots,mathtools}
\usepackage{tikz}
\usetikzlibrary{shapes.misc,decorations.pathmorphing,backgrounds,fit,chains,positioning}
\newcommand{\logtrue}{\mathbf 1}
\newcommand{\bigO}{\mathbf{O}}
\newcommand{\tell}{\mathrm{tell}}
\newcommand{\bigTheta}{\text{\boldmath$\Theta$}}
\newcommand{\Agent}{\mathcal A}
\newcommand{\Cstr}{\mathcal C}
\newcommand{\varset}{\mathcal V}
\newcommand{\Formul}{\mathcal F}
\newcommand{\Prg}{\mathcal P}
\newcommand{\Part}{\mathfrak P}
\newcommand{\powerset}[1]{2^{#1}}
\newcommand{\partset}[1]{\mathrm{Partition}\br{#1}}
\newcommand{\gramOr}{~ | ~}
\DeclareMathOperator{\definedas}{\hat =}
\DeclareMathOperator{\seteq}{\dot =}
\DeclareMathOperator{\askeq}{\stackrel{?}{=}}
\newcommand{\br}[1]{\left(#1\right)}
\newcommand{\cbr}[1]{\left\{#1\right\}}
\newcommand{\bbr}[1]{\left\llbracket#1\right\rrbracket}
\newcommand{\card}[1]{\#\br{#1}}
\newcommand{\st}{|}
\newcommand{\fv}{\mathrm{fv}}
\newcommand{\bv}{\mathrm{bv}}
\theoremstyle{proposition}
\newtheorem{proposition}{Proposition}
\mode<presentation>
\title{Disjoint-set Data Structure for Equality Theory}
\author{Thierry Martinez}
\institute{Équipe--Projet Contraintes}
\date[2008-05-26]{Contraintes' Lab talk, 26 May 2008}
\begin{document}
\begin{frame}
  \titlepage
\end{frame}
\begin{frame}
  \frametitle{Outline}
  \tableofcontents
\end{frame}
\section{Introduction}
\begin{frame}
  \frametitle{Constraint System for the Equality Theory.}
  Let $\varset$ be a set of variables.

  For every term $\phi$:
  \begin{itemize}
  \item $\fv(\phi)$ denotes the set of free variables
    of $\phi$;
  \item $\bv(\phi)$ denotes the set of bound variables
    of $\phi$.
  \end{itemize}

  \begin{description}
  \item[Constraints]
    $\Cstr \Coloneqq \underbrace{\logtrue \gramOr \Cstr \wedge \Cstr
      \gramOr \exists x (\Cstr)}_{\substack{\text{common to
          all}\\\text{constraint systems}}} \gramOr x = y$

    For $\phi \in \Cstr$, we can always suppose that:
    \begin{itemize}
    \item $\fv(\phi) \cap \bv(\phi) = \emptyset$;
    \item each variable is bound at most one time.
    \end{itemize}
  \item[Axioms] In addition to logical axioms for $\logtrue$ and
    $\wedge$ and $\exists$:
    \begin{itemize}
    \item $\vdash_{\Cstr} x = x$;
    \item $x = y \vdash_{\Cstr} y = x$;
    \item $x = y, y = z \vdash_{\Cstr} x = z$.
    \end{itemize}
  \end{description}
  For every variable $\phi$, let $\overrightarrow{x}$ enumerate
  $\fv(\phi)$.  We always have $\vdash_{\Cstr} \exists
  \overrightarrow{x} (\phi)$.
\end{frame}
\begin{frame}
  \frametitle{Equality Theory and Disjoint-sets.}
  \color{black}
  For every constraint $c$, we denote $x \leadsto_c y$ when $x = y$ is
  a sub-term of $c$.

  \[
  \exists x y z t(a = x \wedge b = y \wedge x = y \wedge c = d \wedge
  z = t)
  \]

\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$}; \\
\node (x) [boundvar] {$x$}; \& \node (y) [boundvar] {$y$}; \&
\node (z) [boundvar] {$z$}; \& \node (t) [boundvar] {$t$}; \\
};
\path (a) edge [to] node[auto]{$_c$} (x);
\path (x) edge [to] node[auto]{$_c$} (y);
\path (b) edge [to] node[auto]{$_c$} (y);
\path (c) edge [to] node[auto]{$_c$} (d);
\path (z) edge [to] node[auto]{$_c$} (t);
\begin{pgfonlayer}{background}
\node [fill=blue!30,rounded rectangle,fit=(a) (x) (y) (b)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(c) (d)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(z) (t)] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}

  \begin{definition}
    A partition $\Part$ of $\fv(c)$ is a model for a constraint $c$ if
    for every $x, y \in \fv(c)$ such that $x \leadsto_c \dots
    \leadsto_c y$, we have $x$ and $y$ in the same equivalence class
    of $\Part$.
  \end{definition}
\end{frame}
\begin{frame}
  \frametitle{Model Ordering.}


\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$}; \\
\node (x) [boundvar] {$x$}; \& \node (y) [boundvar] {$y$}; \&
\node (z) [boundvar] {$z$}; \& \node (t) [boundvar] {$t$}; \\
};
\path (a) edge [to] node[auto]{$_c$} (x);
\path (x) edge [to] node[auto]{$_c$} (y);
\path (b) edge [to] node[auto]{$_c$} (y);
\path (c) edge [to] node[auto]{$_c$} (d);
\path (z) edge [to] node[auto]{$_c$} (t);
\begin{pgfonlayer}{background}
\node [scale=1.6,fill=yellow!30,rounded rectangle,fit=(a) (c) (d) (z) (t),opacity=0.8] {}; 
\node [scale=1.5,fill=green!30,rounded rectangle,fit=(c) (d) (z) (t),opacity=0.8] {}; 
\node [scale=1.4,fill=red!30,rounded rectangle,fit=(a) (x) (y) (b),opacity=0.8] {}; 
\node [scale=1.4,fill=red!30,rounded rectangle,fit=(y) (z) (t),opacity=0.8] {}; 
\node [scale=1.2,fill=red!50,rounded rectangle,fit=(a) (x) (y) (b),opacity=0.8] {}; 
\node [scale=1.2,fill=red!50,rounded rectangle,fit=(b) (c) (d),opacity=0.8] {}; 
\node [fill=blue!30,rounded rectangle,fit=(a) (x) (y) (b),opacity=0.8] {}; 
\node [fill=blue!30,rounded rectangle,fit=(c) (d),opacity=0.8] {}; 
\node [fill=blue!30,rounded rectangle,fit=(z) (t),opacity=0.8] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}

  \begin{definition}
    $\Part_1 \sqsubseteq \Part_2$ when for every $x$ and $y$ belonging
    to the same equivalence class of $\Part_1$, we have $x$ and $y$ in
    the same equivalence class of $\Part_2$.
  \end{definition}
\end{frame}
\begin{frame}
  \frametitle{Smallest Model.}

  \color{black} For every constraint $c$, we denote $x \approx_c y$
  when there exists $z$ such that $x \leadsto_c \dots \leadsto_c z$
  and $y \leadsto_c \dots \leadsto_c z$.

\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$}; \\
\node (x) [boundvar] {$x$}; \& \node (y) [boundvar] {$y$}; \&
\node (z) [boundvar] {$z$}; \& \node (t) [boundvar] {$t$}; \\
};
\path (a) edge [to] node[auto]{$_c$} (x);
\path (x) edge [to] node[auto]{$_c$} (y);
\path (b) edge [to] node[auto]{$_c$} (y);
\path (c) edge [to] node[auto]{$_c$} (d);
\path (z) edge [to] node[auto]{$_c$} (t);
\path (a) edge [<->,draw=red] (x);
\path (a) edge [<->,draw=red] (y);
\path (a) edge [<->,draw=red] (b);
\path (b) edge [<->,draw=red] (x);
\path (b) edge [<->,draw=red] (y);
\path (x) edge [<->,draw=red] (y);
\path (c) edge [<->,draw=red] (d);
\path (z) edge [<->,draw=red] (t);
\begin{pgfonlayer}{background}
\node [fill=blue!30,rounded rectangle,fit=(a) (x) (y) (b)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(c) (d)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(z) (t)] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}

  \begin{proposition}
    For every constraint $c$, $\approx_c$ is an equivalence relation
    and the induced partition is the smallest model of $c$.
  \end{proposition}
  \begin{proposition}
    For every $x, y \in \fv(c)$, $c \vdash_{\Cstr} x = y$ if and only
    if $x \approx_c y$.
  \end{proposition}
\end{frame}
\begin{frame}
  \frametitle{Constraint Entailment.}
  \color{black}
  \begin{center}
    $\exists x y z t(a = x \wedge b = y \wedge x = y \wedge c = d \wedge
    z = t)$\\
    $\stackrel{?}{\vdash_{\Cstr}}$\\
    $\exists u v (a = u \wedge b = u \wedge c = v \wedge
    d = v)$
  \end{center}

\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=5mm,column sep=5mm]{
\& \node (u) [boundvar,opacity=0.5] {$u$}; \& \& \& \& \node (v)
[boundvar,opacity=0.5] {$v$}; \& \\
\node (a) [freevar] {$a$}; \& \& \node (b) [freevar] {$b$};
\& \& \node (c) [freevar] {$c$}; \& \& \node (d) [freevar] {$d$}; \\
\node (x) [boundvar,opacity=0.5] {$x$}; \& \& \node (y)
[boundvar,opacity=0.5] {$y$}; \& \&
\node (z) [boundvar,opacity=0.5] {$z$}; \& \& \node (t) [boundvar,opacity=0.5] {$t$}; \\
};
\path (a) edge [to] node[auto]{$_{c_1}$} (x);
\path (x) edge [to] node[auto,swap]{$_{c_1}$} (y);
\path (b) edge [to] node[auto,swap]{$_{c_1}$} (y);
\path (c) edge [to] node[auto,swap]{$_{c_1}$} (d);
\path (z) edge [to] node[auto,swap]{$_{c_1}$} (t);
\path (a) edge [->] node[auto]{$_{c_2}$} (u);
\path (b) edge [->] node[auto,swap]{$_{c_2}$} (u);
\path (c) edge [->] node[auto]{$_{c_2}$} (v);
\path (d) edge [->] node[auto,swap]{$_{c_2}$} (v);
\begin{pgfonlayer}{background}
\node [fill=orange!30,rounded rectangle,fit=(a) (b) (u),opacity=0.5] {}; 
\node [fill=orange!30,rounded rectangle,fit=(c) (d) (v),opacity=0.5] {}; 
\node [fill=blue!30,rounded rectangle,fit=(a) (x) (y) (b),opacity=0.5] {}; 
\node [fill=blue!30,rounded rectangle,fit=(a) (b)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(c) (d)] {}; 
\node [fill=blue!30,rounded rectangle,fit=(z) (t),opacity=0.5] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}
  \begin{proposition}
    $c_1 \vdash c_2$ if and only if, for every $x, y \in \fv(c_2)$
    such that $x \approx_{c_2} y$, we have $x$ and $y$ in the same
    equivalence class in every model of $c_1$.
  \end{proposition}
  \color{black} It suffices to check in the inclusion between smallest
  models restricted to free variables.
\end{frame}
\section{Disjoint-sets Abstract Machine}
\begin{frame}
  \frametitle{A Very Simple Logic Language.}
  \begin{block}{Program}
    \[\Prg \Coloneqq \overbrace{\forall \overrightarrow{x} (\underbrace{\Cstr}_{\text{hypotheses}} \Rightarrow
      \underbrace{\Cstr}_{\text{query}})}^{\text{closed term}}? \]
  \end{block}
  \begin{block}{Execution Scheme}
    \begin{enumerate}
    \item Build the smallest model associated to the hypotheses.
    \item Read the model to check whether the query is entailed.
    \end{enumerate}
  \end{block}
\end{frame}
\begin{frame}
  \frametitle{Build the Smallest Model Associated to a Constraint.}
  \color{black}
  \[
  C \definedas \exists g ({\color<2>{red}g = a} \wedge
{\color<3>{red}a = b}) \wedge \exists i j (
{\color<4>{red}d = i} \wedge
{\color<5>{red}e = j} \wedge \exists h k l (
{\color<6>{red}i = h} \wedge
{\color<7>{red}j = k} \wedge
{\color<8>{red}f = l}
  \wedge
{\color<9>{red}c = h})) \wedge
{\color<10>{red}d = e}
  \]

\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=5mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$};
 \& \node (e) [freevar] {$e$}; \&\& \node (f) [freevar] {$f$}; \\
\node (g) [boundvar] {$g$}; \& \node (h) [boundvar] {$h$}; \&
\& \node (i) [boundvar] {$i$}; \& \node (j) [boundvar] {$j$}; \&
\node (k) [boundvar] {$k$}; \& \node (l) [boundvar] {$l$}; \\
};
\begin{pgfonlayer}{background}
\only<2->{\node [fill=blue!30,rounded rectangle,fit=(g) (a),opacity=0.7] {}}; 
\only<3->{\node [fill=blue!30,rounded rectangle,fit=(a) (b),opacity=0.7] {}};
\only<4-9>{\node [fill=orange!30,rounded rectangle,fit=(d) (i),opacity=0.7] {}};
\only<10>{\node [fill=orange!40,rounded rectangle,fit=(d) (i),opacity=0.7] {}};
\only<5-9>{\node [fill=red!30,rounded rectangle,fit=(e) (j),opacity=0.7] {}};
\only<10->{\node [fill=orange!40,rounded rectangle,fit=(e) (j),opacity=0.7] {}};
\only<6-9>{\node [fill=orange!30,rounded rectangle,fit=(i) (h),opacity=0.7] {}};
\only<10>{\node [fill=orange!40,rounded rectangle,fit=(i) (h),opacity=0.7] {}};
\only<7-9>{\node [fill=red!30,rounded rectangle,fit=(j) (k),opacity=0.7] {}};
\only<10->{\node [fill=orange!40,rounded rectangle,fit=(j) (k),opacity=0.7] {}};
\only<8->{\node [fill=green!30,rounded rectangle,fit=(f) (l),opacity=0.7] {}};
\only<9>{\node [fill=orange!30,rounded rectangle,fit=(c) (d),opacity=0.7] {}};
\only<10->{\node [fill=orange!40,rounded rectangle,fit=(c) (d),opacity=0.7] {}};
\only<10->{\node [fill=orange!40,rounded rectangle,fit=(d) (e),opacity=0.7] {}};
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}

\begin{alertblock}{Two op-codes}<10->
\begin{center}
$x \seteq y$ and $x \askeq y$
\end{center}
\end{alertblock}
\end{frame}
\begin{frame}
  \frametitle{Compiling Queries.}
  \color{black}
  \[
  \Cstr_0 \Coloneqq \logtrue \gramOr \Cstr_0 \wedge \Cstr_0 \gramOr x = y
  \]
  \begin{proposition}
    For every $c \in \Cstr$, there is a computable $\bbr{c} \in
    \Cstr_0$ such that $c \dashv \vdash \bbr{c}$.
  \end{proposition}
  \begin{proof}
    \begin{description}
    \item[Computation.]
\only<1>{ $c \dashv \vdash a = b \wedge c = d \wedge c = e$
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=5mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$};
 \& \node (e) [freevar] {$e$}; \&\& \node (f) [freevar] {$f$}; \\
\node (g) [boundvar,opacity=0.5] {$g$}; \& \node (h) [boundvar,opacity=0.5] {$h$}; \&
\& \node (i) [boundvar,opacity=0.5] {$i$}; \& \node (j) [boundvar,opacity=0.5] {$j$}; \&
\node (k) [boundvar,opacity=0.5] {$k$}; \& \node (l) [boundvar,opacity=0.5] {$l$}; \\
};
\draw [->] (a) to (b);
\draw [->] (c) to (d);
\draw [->] (c) to [bend left=30] (e);
\begin{pgfonlayer}{background}
\node [fill=blue!30,rounded rectangle,fit=(g) (a),opacity=0.7] {}; 
\node [fill=blue!30,rounded rectangle,fit=(a) (b),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(d) (i),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(e) (j),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(i) (h),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(j) (k),opacity=0.7] {};
\node [fill=green!30,rounded rectangle,fit=(f) (l),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(c) (d),opacity=0.7] {};
\node [fill=orange!40,rounded rectangle,fit=(d) (e),opacity=0.7] {};
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}
}
\only<2>{
      Let $\Part$ be the smallest model of $c$.
      \[\bbr{c} \definedas
      \bigwedge_{
        \substack{
          P \in \Part\\
          \card{P \cap \fv(c)} \geqslant 2\\
          \cbr{x} \uplus V \definedas P \cap \fv(c)
        }}
      \bigwedge_{y \in V} x = y\]
}
    \item[$c \dashv \vdash \bbr{c}$.] $c$ and $\bbr{c}$ have the same
      models.
    \end{description}
  \end{proof}
\end{frame}
\begin{frame}
  \frametitle{Extension to Rational Terms.}
  \color{black}
  \begin{description}
  \item[Constraints]
    $\Cstr \Coloneqq \underbrace{\logtrue \gramOr \Cstr \wedge \Cstr
      \gramOr \exists x (\Cstr)}_{\substack{\text{common to
          all}\\\text{constraint systems}}} \gramOr x = y \gramOr x =
    f(\overrightarrow{y})$
  \item[New Op-codes] Labelled equivalence classes.
    \begin{itemize}
    \item $\mathrm{struct}(x, f(\overrightarrow{y}))$ to label an
      equivalence class, possible previous label must match and
      equality constraints on arguments are added.
    \item $\overrightarrow{y} \leftarrow \mathrm{struct}_?(x, f)$ to
      check that $x$ has the functor $f$, then extract arguments.
    \end{itemize}
  \end{description}
\end{frame}
\begin{frame}
  \frametitle{Build the Code Associated to a Rational Tree Query.}
  \color{black}
  \[
  C \definedas \exists x y z(a = f(x, y) \wedge x = f(z, y) \wedge z = f(x, y))
  \]
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (x) [boundvar] {$x$};
 \& \node (y) [boundvar] {$y$};  \& \node (z) [boundvar] {$z$}; \\
\begin{scope}[start chain,node distance=0mm]
\node (af1) [on chain] {f(};
\node (afx) [on chain,boundvar,opacity=0.7mm] {x};
\node [on chain] {,};
\node (afy) [on chain,boundvar,opacity=0.7mm] {y};
\node (af2) [on chain] {)};
\end{scope} \&
\begin{scope}[start chain,node distance=0mm]
\node (xf1) [on chain] {f(};
\node (xfz) [on chain,boundvar,opacity=0.7mm] {z};
\node [on chain] {,};
\node (xfy) [on chain,boundvar,opacity=0.7mm] {y};
\node (xf2) [on chain] {)};
\end{scope} \& \&
\begin{scope}[start chain,node distance=0mm]
\node (zf1) [on chain] {f(};
\node (zfx) [on chain,boundvar,opacity=0.7mm] {x};
\node [on chain] {,};
\node (zfy) [on chain,boundvar,opacity=0.7mm] {y};
\node (zf2) [on chain] {)};
\end{scope}\\
};
\draw[->] (afx) to [bend left=30] (x);
\draw[->] (afy) to [bend left=20] (y);
\draw[->] (xfz) to [bend right=40] (z);
\draw[->] (xfy) to [bend right=30] (y);
\draw[->] (zfx) to [bend right=50] (x);
\draw[->] (zfy) to [bend right=50] (y);
\begin{pgfonlayer}{background}
\node [fill=blue!30,rounded rectangle,fit=(a) (af1) (af2)] {}; 
\node [fill=green!30,rounded rectangle,fit=(x) (xf1) (xf2)] {}; 
\node [fill=yellow!30,rounded rectangle,fit=(y)] {}; 
\node [fill=orange!30,rounded rectangle,fit=(z) (zf1) (zf2)] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}
\begin{enumerate}
\item $(x, y) \leftarrow \mathrm{struct}_?(a, f)$
\item $(z, y_1) \leftarrow \mathrm{struct}_?(x, f)$
\item $y_1 \askeq y$
\item $(x_1, y_2) \leftarrow \mathrm{struct}_?(z, f)$
\item $x_1 \askeq x$
\item $y_2 \askeq y$
\end{enumerate}
\end{frame}
\begin{frame}
  \frametitle{State Minimization.}
  \color{black}
  \[
  C \definedas \exists x y z(a = f(x, y) \wedge x = f(z, y) \wedge z = f(x, y))
  \]
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (y) [boundvar] {$y$}; \\
\begin{scope}[start chain,node distance=0mm]
\node (af1) [on chain] {f(};
\node (afx) [on chain,boundvar,opacity=0.7mm] {a};
\node [on chain] {,};
\node (afy) [on chain,boundvar,opacity=0.7mm] {y};
\node (af2) [on chain] {)};
\end{scope} \\
};
\draw[->] (afx) to [bend left=30] (a);
\draw[->] (afy) to [bend left=20] (y);
\begin{pgfonlayer}{background}
\node [fill=blue!30,rounded rectangle,fit=(a) (af1) (af2)] {};  
\node [fill=yellow!30,rounded rectangle,fit=(y)] {}; 
\end{pgfonlayer} 
\end{tikzpicture}
\end{center}
\begin{enumerate}
\item $(a_1, y) \leftarrow \mathrm{struct}_?(a, f)$
\item $a_1 \askeq a$
\end{enumerate}
\end{frame}
\section{Data Structure}
\begin{frame}
  \frametitle{Equivalence Classes as Variable Trees.}
  \color{black}
  Op-codes implementation:
  \begin{description}
  \item[$x \seteq y$] ``$\mathrm{link}(\mathrm{find}(x), \mathrm{find}(y))$''
  \item[$x \askeq y$] check whether ``$\mathrm{find}(x) = \mathrm{find}(y)$''
  \end{description}
  where:
  \begin{description}
  \item[$\mathrm{find}(x)$] Follows the arcs from $x$ up to find the
    root.  Root is returned.
  \item[$\mathrm{link}(x, y)$] Adds an arc from $x$ to $y$.
    Prerequisite: $x$ former root, $y$ root.
  \end{description}
\only<-10>{
  \[
  C \definedas \exists g ({\color<2>{red}g = a} \wedge
{\color<3>{red}b = g}) \wedge \exists i j (
{\color<4>{red}d = i} \wedge
{\color<5>{red}e = j} \wedge \exists h k l (
{\color<6>{red}i = h} \wedge
{\color<7>{red}j = k} \wedge
{\color<8>{red}f = l}
  \wedge
{\color<9>{red}c = h})) \wedge
{\color<10>{red}d = e}
  \]
}
\only<11>{
  \[
  C \definedas \exists g ({\color<2>{red}g = a} \wedge
{\color<3>{red}g = b}) \wedge \exists i j (
{\color<4>{red}d = i} \wedge
{\color<5>{red}e = j} \wedge \exists h k l (
{\color<6>{red}i = h} \wedge
{\color<7>{red}j = k} \wedge
{\color<8>{red}f = l}
  \wedge
{\color<9>{red}h = c})) \wedge
{\color<10>{red}d = e}
  \]
}
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=2mm,column sep=2mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$};
 \& \node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$};
 \& \node (e) [freevar] {$e$}; \&\& \node (f) [freevar] {$f$}; \\
\node (g) [boundvar] {$g$}; \& \node (h) [boundvar] {$h$}; \&
\& \node (i) [boundvar] {$i$}; \& \node (j) [boundvar] {$j$}; \&
\node (k) [boundvar] {$k$}; \& \node (l) [boundvar] {$l$}; \\
};
\only<2-10>{\draw [->] (a) to [bend left=10] (g);}
\only<3-10>{\draw [->] (g) to [bend left=10] (b);}
\only<4-10>{\draw [->] (i) to [bend left=10] (d);}
\only<5-10>{\draw [->] (j) to [bend left=10] (e);}
\only<6-10>{\draw [->] (h) to [bend right=20] (d);}
\only<7-10>{\draw [->] (k) to [bend right=20] (e);}
\only<8-10>{\draw [->] (l) to [bend left=10] (f);}
\only<9-10>{\draw [->] (d) to [bend left=10] (c);}
\only<10-10>{\draw [->] (e) to [bend left=10] (d);}
\only<11>{\draw [->] (a) to [bend left=10] (g);}
\only<11>{\draw [->] (b) to [bend left=10] (g);}
\only<11>{\draw [->] (i) to [bend left=10] (d);}
\only<11>{\draw [->] (j) to [bend left=10] (e);}
\only<11>{\draw [->] (h) to [bend right=20] (d);}
\only<11>{\draw [->] (k) to [bend right=20] (e);}
\only<11>{\draw [->] (l) to [bend left=10] (f);}
\only<11>{\draw [->] (c) to [bend left=10] (d);}
\only<11>{\draw [->] (e) to [bend left=10] (d);}
\end{tikzpicture}
\end{center}
  \begin{proposition}
    For a sequence of $m$ operations, among which $n$ are
    ``$\mathrm{link}$'' operations, the total complexity is
    $\bigTheta(m n)$.
  \end{proposition}
\end{frame}
\begin{frame}
  \frametitle{Heuristic 1: Union by Rank.}
  \color{black}
  Roots keep track (of an upper-bound) of tree heights.
  \[
C \definedas
{\color<2>{red}{a = e}} \wedge
{\color<3>{red}{b = e}} \wedge
{\color<4>{red}{c = f}} \wedge
{\color<5>{red}{d = f}} \wedge
{\color<6>{red}{f = e}}
  \]
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
 \& \node (e) [freevar] {$e$}; \& \& \& \node (f) [freevar] {$f$};\\
\node (a) [freevar] {$a$}; \& \& \node (b) [freevar] {$b$}; \&
\node (c) [freevar] {$c$}; \& \& \node (d) [freevar] {$d$}; \\
};
\only<2-6>{\draw [->] (a) to [bend left=10] (e);}
\only<3-6>{\draw [->] (b) to [bend right=10] (e);}
\only<4-6>{\draw [->] (c) to [bend left=10] (f);}
\only<5-6>{\draw [->] (d) to [bend right=10] (f);}
\only<6-6>{\draw [->] (f) to [bend right=10] (e);}
\end{tikzpicture}
\end{center}
  \begin{proposition}
    For a sequence of $m$ operations, among which $n$ are
    ``$\mathrm{link}$'' operations, the total complexity is
    $\bigTheta(m \log n)$.
  \end{proposition}
\end{frame}
\begin{frame}
  \frametitle{Heuristic 2: Path Compression.}
  \color{black}
  Once ``$\mathrm{find}$'' obtains the actual root, update the arc to
  directly point to it.
  \[
C \definedas
{\color<2>{red}{b = a}} \wedge
{\color<3>{red}{c = a}} \wedge
{\color<4>{red}{d = a}} \wedge
{\color<5>{red}{e = a}} \wedge
{\color<6>{red}{f = a}}
  \]
\begin{center}
\begin{tikzpicture}[ 
freevar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The border: 
very thick, 
draw=red!50!black!50, % 50% red and 50% black, 
% and that mixed with 50% white 
% The filling: 
top color=white, % a shading that is white at the top... 
bottom color=red!50!black!20, % and something else at the bottom 
},
boundvar/.style={ 
% The shape: 
rounded rectangle, 
minimum size=6mm, 
% The rest 
very thick,draw=black!50, 
top color=white,bottom color=black!20},
to/.style={->,decorate,decoration=snake}
] 
\matrix[ampersand replacement=\&,row sep=10mm,column sep=10mm]{
\node (a) [freevar] {$a$}; \& \node (b) [freevar] {$b$}; \&
\node (c) [freevar] {$c$}; \& \node (d) [freevar] {$d$}; \&
\node (e) [freevar] {$e$}; \& \node (f) [freevar] {$f$};\\
};
\only<2-3>{\draw [->] (a) to [bend left=10] (b);}
\only<4>{\draw [->] (a) to [bend left=20] (c);}
\only<5>{\draw [->] (a) to [bend left=30] (d);}
\only<6>{\draw [->] (a) to [bend left=40] (e);}
\only<3-4>{\draw [->] (b) to [bend left=10] (c);}
\only<5>{\draw [->] (b) to [bend left=20] (d);}
\only<6>{\draw [->] (b) to [bend left=30] (e);}
\only<4-5>{\draw [->] (c) to [bend left=10] (d);}
\only<6>{\draw [->] (c) to [bend left=10] (e);}
\only<5->{\draw [->] (d) to [bend left=10] (e);}
\only<6->{\draw [->] (e) to [bend right=10] (f);}
\end{tikzpicture}
\end{center}

  \begin{proposition}
    For a sequence of $f$ ``$\mathrm{find}$'' operations and $n$
    ``$\mathrm{link}$'' operations, the total complexity is
    $\bigO(n + f \cdot (1 + \log_{2 + f/n} n))$.
  \end{proposition}
\end{frame}
\begin{frame}
  \frametitle{A very quickly growing function\dots}
  \begin{definition}
    For integers $m, n \geq 0$:
    \[
    A(m, n) =
    \begin{cases}
      n + 1 & \text{if $m = 0$,}\\
      A(m - 1, 1) & \text{if $m > 0$ and $n = 0$,} \\
      A(m - 1, A(m, n - 1)) & \text{if $m > 0$ and $n > 0$.}
    \end{cases}
    \]
  \end{definition}
\color{black}
    \[
\rowcolors{1}{RoyalBlue!20}{RoyalBlue!5}
\begin{array}{|c|cccccc|}
\hline
m & 0 & 1 & 2 & 3 & 4 & 5\\
\hline
A(m, 1) & 2 & 3 & 5 & 13 & 65533 &
\underbrace{2^{2^{\iddots^2}}}_{65536} - 3 \gg 10^{80}\\
\hline
\end{array}
    \]
\end{frame}
\begin{frame}
  \frametitle{\dots and its very slowly growing inverse.}
  \color{black}
\begin{definition}
  For $n \geqslant 0$:
  \[
  \alpha(n) = \min \cbr{k \st A(k, 1) \geq 1}
  \]
\end{definition}
\begin{exampleblock}{For all practical purposes}
\[
    \alpha(n) \leqslant 5
\]
\end{exampleblock}
\end{frame}
\begin{frame}
  \frametitle{Quasi-linear complexity.}
  \begin{proposition}
    For a sequence of $m$ operations, among which $n$ are
    ``$\mathrm{link}$'' operations, the total complexity is
    $\bigO(m \alpha(n))$.
  \end{proposition}
\end{frame}
\section{Concurrent Constraints}
\begin{frame}
  \frametitle{$\mathrm{cc}(=)$}
  \begin{block}{Program}
    \begin{align*}
      \Prg & \Coloneqq \epsilon \gramOr p(\overrightarrow{x}) \coloneq
      \Agent. ~ \Prg\\
      \Agent & \Coloneqq \br{\Agent \Vert \Agent} \gramOr \exists
      x(\Agent) \gramOr p(\overrightarrow{x}) \gramOr \tell(\Cstr)
      \gramOr \underbrace{{\color{gray} \forall
          \overrightarrow{x}}(\Cstr \rightarrow \Agent)}_{(\exists
        \overrightarrow{x} (c) \rightarrow \exists \overrightarrow{x}
        (\tell(c) \Vert a)}
    \end{align*}
  \end{block}
\end{frame}
\begin{frame}
  \frametitle{New Op-codes for Translating $\mathrm{cc}(=)$}
  \color{black}
  \begin{description}
  \item[$\mathrm{call}~p(\overrightarrow{x})$ / $\mathrm{return}$]
    Flow-control operations.
  \item[$\mathrm{freeze}(x \askeq y, \mathrm{Code})$] Ask on atomic constraints.
    \begin{align*}
    (a = b \wedge b = c \rightarrow A) &
    \equiv (a = b \rightarrow (b = c \rightarrow A))\\
    & \leadsto
    \mathrm{freeze}(a \askeq b, \mathrm{freeze}(b \askeq c, \bbr{A}))
    \end{align*}
  \end{description}
\end{frame}
\section{Conclusion}
\begin{frame}
  \frametitle{Conclusion}
  \color{black}
  \begin{description}
  \item[Good things]~\\
  \begin{itemize}
  \item The entailment checker can be deduced from the smallest model
    of the constraint.
  \item Computing the smallest model offline allows to produce optimal
    code for the virtual machine (when used with minimization for
    rational terms).
  \end{itemize}
  \item[Open questions]~\\
  \begin{itemize}
  \item Better representation for the freeze on equalities.
  \item Extension with linear tokens.

    Let $f_1, \dots, f_n$ be closures in a $\mathrm{lcc/RH}$ program
    (with asks $(\mathrm{do}(f_1) \rightarrow a_1) \Vert \dots \Vert
    (\mathrm{do}(f_n) \rightarrow a_n)$).  If implemented naively,
    $\mathrm{tell}(\mathrm{do}(x))$ leads to freezes on $x \askeq f_1,
    \dots, x \askeq f_n$.
  \end{itemize}
  \end{description}
\end{frame}
\end{document}