%\documentclass[compress]{beamer}   % {{{
\documentclass[handout,compress]{beamer}
\usepackage{amsfonts, amsmath, amssymb, amsthm, mathtools}
\usepackage{tikz, float, tabu, multirow}
\usetikzlibrary{calc,decorations.markings,matrix,arrows,positioning}

% color settings
\mode<presentation>{
\usetheme{Madrid}
\usecolortheme{default}
\beamertemplatenavigationsymbolsempty
}
\setbeamercolor{alerted text}{fg=blue}
\setbeamertemplate{items}[circle]

% mathbb and mathcal symbols
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\A}{\mathbb{A}}
\newcommand{\m}[1]{\mathbb{#1}}    % for models
\newcommand{\cl}[1]{\mathcal{#1}}  % for classes

% theorems and similar environments
\theoremstyle{plain} \newtheorem{thm}{Theorem}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{cor}[thm]{Corollary}
\theoremstyle{definition} \newtheorem{defn}[thm]{Definition}
\theoremstyle{remark} \newtheorem*{rk}{Remark}
\theoremstyle{plain} \newtheorem*{Q}{Question}
\newcommand{\Case}[1]{\smallskip \textbf{Case #1:}}

% custom commands
\DeclareMathOperator{\Cg}{Cg}
\DeclareMathOperator{\Sg}{Sg}
\DeclareMathOperator{\Con}{Con}
\DeclareMathOperator{\Clo}{Clo}
\DeclareMathOperator{\Rel}{Rel}
\DeclareMathOperator{\diag}{diag}
\newcommand{\pmat}[1]{\ensuremath{ \begin{pmatrix} #1 \end{pmatrix} }}
\newcommand{\bmat}[1]{\ensuremath{ \begin{bmatrix} #1 \end{bmatrix} }}

% symbol overrides
\let\emph\textbf
\renewcommand{\phi}{\varphi}
\renewcommand{\epsilon}{\varepsilon}

% document specific stuff
\usepackage{enumitem}
\setitemize{label=\usebeamerfont*{itemize item}
  \usebeamercolor[fg]{itemize item}
  \usebeamertemplate{itemize item}}
\theoremstyle{plain} \newtheorem*{prob}{Problem}
\theoremstyle{plain} \newtheorem*{conj}{Conjecture}
\theoremstyle{remark} \newtheorem*{ex}{Example}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\1}{\textbf{1}}
\newcommand{\2}{\textbf{2}}
\newcommand{\3}{\textbf{3}}
\newcommand{\4}{\textbf{4}}
\newcommand{\5}{\textbf{5}}
%============================================================================}}}

\begin{document}
% title page {{{
\title{Decidability in Universal Algebra}
\author{Matthew Moore}
\institute[McMaster]{McMaster University}
\date[2017-03-10]{March 10, 2017}

\begin{frame}
\titlepage
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Decidability in universal algebra}   % TOC {{{
\tableofcontents
\end{frame}
%============================================================================}}}

\section{Introduction}
% TOC {{{
\begin{frame} \frametitle{Decidability in universal algebra}
\tableofcontents[currentsection]
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Decidability}   % {{{
\pause
\begin{defn}
The \emph{decision problem} for property $P(\cdot)$ is the computational
problem \\
\begin{itemize}[leftmargin=5em]
  \pause\item[\emph{Input:}] some finite object $A$.
  \pause\item[\emph{Output:}] whether $P(A)$ is true.
\end{itemize}
\pause If there is an algorithm which solves this problem, then $P(\cdot)$
is \emph{decidable}.

\pause\smallskip

Otherwise $P(\cdot)$ is otherwise is \emph{undecidable}.
\end{defn}

\pause\smallskip

\begin{ex}
The \emph{halting problem} is the decision problem
\begin{itemize}[leftmargin=5em]
  \pause\item[\emph{Input:}] a program $P$.
  \item[\emph{Output:}] whether $P$ eventually halts.
\end{itemize}
\pause The halting problem is famously undecidable.
\end{ex}

\pause\smallskip

\textbf{General strategy:} encode the halting problem into $P(\cdot)$.
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Known results (in Universal Algebra)}   % {{{
The following are known to be undecidable for finite algebra $\A$:
\medskip\pause
\begin{itemize}
  \item Whether $\A$ has a finite residual bound [McKenzie].
    \begin{itemize}
      \uncover<8->{\item strategy: encode Turing machine $\T$ into special
        $\A(\T)$.}
    \end{itemize}

  \medskip\pause

  \item Whether $\A$ has a finite equational base [McKenzie; Willard].
    \begin{itemize}
      \uncover<9->{\item McKenzie: new algebra $\m{F}(\T)$.}
      \uncover<10->{\item Willard: $\A(\T)$ above works!}
    \end{itemize}

  \medskip\pause

  \item Whether $\A$ has definable principal subcongruences [M].
    \begin{itemize}
      \uncover<11->{\item variation on McKenzie's $\A(\T)$.}
    \end{itemize}

  \medskip\pause

  \item Whether $\text{typ}(\V(\A))$ contains $i$ for $i\in \{
    \mathbf{2}, \mathbf{3}, \mathbf{4}, \mathbf{5} \}$ [Wood, McKenzie].
    \begin{itemize}
      \uncover<12->{\item variation on McKenzie's $\A(\T)$.}
    \end{itemize}

  \medskip\pause

  \item Whether $\A$ has an NU term on $A-\{p,q\}$ [Maroti].
    \begin{itemize}
      \uncover<13->{\item encode Minsky machine into a special $\m{B}(\M)$.}
    \end{itemize}

  \medskip
\end{itemize}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Conjectures}   % {{{
The following are \emph{conjectured} to be undecidable for finite $\A$:
\begin{itemize}
  \medskip
  \pause\item \textbf{(1)} Whether $\A$ is finitely related.
  \medskip
  \pause\item \textbf{(2)} Whether $\A$ is naturally dualizable.
  \medskip
  \pause\item + \emph{many} more problems from clone theory.
\end{itemize}

\pause\vfill

If $\V(\A)$...
\begin{itemize}
  \pause\item is congruence distributive, then we can decide \textbf{(1)}
    and \textbf{(2)}.
  \pause\item is congruence modular, then we can decide \textbf{(1)} and
    (sort of) \textbf{(2)}.
  \pause\item is congruence SD$(\wedge)$, we have no strong results.
  \pause\item has a compatible semilattice term, then we can decide both
    (`yes').
\end{itemize}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Entailment}   % {{{
Let...
\begin{itemize}
  \pause\item $\A$ be a finite algebra,
  \pause\item $\m{R}$ an $m$-ary relation of $\A$
    \pause
    $\big( \m{R}\leq\A^m \big)$,
  \pause\item $\mathcal{R}$ be a set of finite arity relations of $\A$
    \pause
    $\Big( \mathcal{R} \subseteq \bigcup_{n=1}^N \S(\A^n) \Big)$,
\end{itemize}

\pause\bigskip

$\mathcal{R}$ \emph{entails} $\m{R}$ $\big( \mathcal{R}\models \m{R} \big)$
if $\m{R}$ is obtained by applying the operations below to members
of $\mathcal{R}\cup \{=\}$.
\vspace{-0.5em}
\begin{columns}
\begin{column}{0.3\textwidth}
  \begin{itemize}
    \pause\item intersection
    \pause\item product
  \end{itemize}
\end{column}
\begin{column}{0.65\textwidth}
  \begin{itemize}
    \pause\item permutation of coordinates
    \pause\item projection onto a subset of coordinates
  \end{itemize}
\end{column}
\end{columns}

\pause\vfill

$\mathcal{R}$ \emph{duality entails} $\m{R}$ $\big( \mathcal{R}\models_d
\m{R} \big)$ if $\m{R}$ is obtained by applying the operations below to
members of $\mathcal{R}\cup \{=\}$.
\vspace{-0.5em}
\begin{columns}
\begin{column}{0.3\textwidth}
  \begin{itemize}
    \pause\item intersection
    \pause\item product
  \end{itemize}
\end{column}
\begin{column}{0.65\textwidth}
  \begin{itemize}
    \pause\item permutation of coordinates
    \pause\item bijective projection onto coordinates
  \end{itemize}
\end{column}
\end{columns}

\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Entailment}   % {{{
\begin{defn}
Let $\A$ be a finite algebra, and let $\mathcal{R}_n = \bigcup_{k\leq n}
\S(\A^k)$.
\begin{itemize}
  \pause\item $\A$ is \emph{finitely related} if $\mathcal{R}_n \models
  \mathcal{R}_{\omega}$ for some $n$.

  \pause\item $\A$ is \emph{finitely duality related} if $\mathcal{R}_n
  \models_d \mathcal{R}_{\omega}$ for some $n$.
\end{itemize}
\end{defn}

\pause\bigskip

\begin{prob}[Relational entailment]
\begin{itemize}[leftmargin=5em]
  \pause\item[\emph{Input:}] finite algebra $\A$.
  \pause\item[\emph{Output:}] whether $\A$ is finitely related.
\end{itemize}
\end{prob}

\pause

\begin{prob}[Relational duality entailment]
\begin{itemize}[leftmargin=5em]
  \pause\item[\emph{Input:}] finite algebra $\A$.
  \pause\item[\emph{Output:}] whether $\A$ is finitely duality related.
\end{itemize}
\end{prob}
\end{frame}
%============================================================================}}}

\section{Computational models}
% TOC {{{
\begin{frame} \frametitle{Decidability in universal algebra}
\tableofcontents[currentsection]
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Minsky machines}   % {{{
The Minsky machine is a simple model of computation.

\pause\vfill

A Minsky machine has...
\begin{itemize}
  \pause\medskip
  \item states $0, 1, \ldots, N$ (state $1$ is starting state, $0$ is
    halting),
  \pause\medskip
  \item registers $A$ and $B$ that have integer values $\geq 0$,
  \pause\medskip
  \item instructions of the form $(i,R,j)$, \pause meaning \\ ``in state
    $i$, increase register $R$ by 1 and enter $j$''.
  \pause\medskip
  \item instructions of the form $(i,R,j,k)$, \pause meaning \\ ``in state
    $i$, if $R$ is $0$ enter $j$, otherwise decrease $R$ by $1$ and enter
    $k$''.
\end{itemize}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{A Minsky machine}   % {{{
Let $\mathcal{M}$ have instructions
\begin{center}
  \pause \alert<9,13,17|handout:0>{(1,B,3,2)},
  \qquad\pause \alert<11,15|handout:0>{(2,A,1)},
  \qquad\pause \alert<19|handout:0>{(3,A,4)},
  \qquad\pause \alert<21|handout:0>{(4,A,0)}.
\end{center}
\pause Start the machine with register contents $A = 3$, $B = 2$. 
\pause\medskip
\begin{columns}
\begin{column}{0.4\textwidth}
  \begin{tabular}{cccc}
    \textbf{Step} & \textbf{State} & \textbf{A} & \textbf{B} \\ \hline
    \uncover<8-> {0 & 1 & 3 & 2} \\
    \uncover<10->{1 & \alert<10|handout:0>{2} & 3 & \alert<10|handout:0>{1}} \\
    \uncover<12->{2 & \alert<12|handout:0>{1} & 4 & \alert<12|handout:0>{1}} \\
    \uncover<14->{3 & \alert<14|handout:0>{2} & 4 & \alert<14|handout:0>{0}}
  \end{tabular}
\end{column} 
\begin{column}{0.4\textwidth}
  \begin{tabular}{cccc}
    \textbf{Step} & \textbf{State} & \textbf{A} & \textbf{B} \\ \hline
    \uncover<16->{4 & \alert<16|handout:0>{1} & 5 & 0} \\
    \uncover<18->{5 & \alert<18|handout:0>{3} & 5 & 0} \\
    \uncover<20->{6 & \alert<20|handout:0>{4} & \alert<20|handout:0>{6} & 0} \\
    \uncover<22->{7 & \alert<22|handout:0>{0} & \alert<22|handout:0>{7} & 0}
  \end{tabular}
\end{column} 
\end{columns}

\medskip

\uncover<23->{$\mathcal{M}$ computes $A+B+2$ and stores the result in $A$.}

\bigskip

\uncover<24->{Minsky machines more useful for us than Turing machines:}
\begin{columns}
\begin{column}{0.5\textwidth}
  \begin{itemize}
    \uncover<25->{\item no tape,}
    \uncover<26->{\item no machine head,}
    \uncover<27->{\item instructions are more condensed,}
  \end{itemize}
\end{column}
\begin{column}{0.55\textwidth}
  \begin{itemize}
    \uncover<28->{\item ``equivalent'' to Turing machines,}
    \uncover<29->{\item the Halting Problem for Minsky machines is
      undecidable.}
  \end{itemize}
\end{column}
\end{columns}
\end{frame}
%============================================================================}}}

\section{The algebra $\A(\M)$}
% TOC {{{
\begin{frame} \frametitle{Decidability in universal algebra}
\tableofcontents[currentsection]
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{$A(\M)$}   % {{{
Let $\M$ be a Minsky machine with states $0, 1, \ldots, N$. \pause Let
\begin{itemize}
  \pause\item $\Sigma = \{ \circ, \bullet, \times \}$,
  \pause\item for each state $i$, 
    $M_i = \Big\{ \left<i, c\right> \mid c\in \{0,A,B,\times\} \Big\}$.
\end{itemize}
\pause $\m{A}(\M)$ has underlying set $A(\M) = \Sigma \cup \bigcup_{i=0}^N
M_i$.

\pause\bigskip

$\A(\M)$ has the following operations, plus some more:
\begin{itemize}
  \pause\item a semilattice operation $\wedge$: \hspace{1em}
  \begin{tikzpicture}[font=\small, node distance=0.5em, baseline=(ix)]
    \node (circle) {$\circ$};
    \node [right=of circle] (dot) {$\bullet$};
    \coordinate (temp) at ($(circle)!0.5!(dot)$);
    \node [below=1em of temp] (X) {$\times$};

    \node [right=2em of dot] (ix) {\scriptsize$\left<i,\times\right>$};
    \node [above=of ix] (i0) {\scriptsize$\left<i,0\right>$};
    \node [left=of i0] (iA) {\scriptsize$\left<i,A\right>$};
    \node [right=of i0] (iB) {\scriptsize$\left<i,B\right>$};

    \draw (circle) -- (X) -- (dot) (iA) -- (ix) -- (X) (i0) -- (ix) (iB) -- (ix);
  \end{tikzpicture}

  \pause

  \item $\left<1,0\right>$ as a constant

  \pause\bigskip

  \item machine operations $M(x,y)$, $M'(x)$
\end{itemize}
\end{frame}
%============================================================================}}}
\begin{frame}[t]  % A(M) calculation {{{
\begin{columns}
\begin{column}{0.57\textwidth}
  $\scriptsize \displaystyle{
    M(x,y) = \begin{cases}
      \left<j,R\right>  & \text{if } (i,R,j)\in \M, \\ 
                        & \quad      y = \bullet, x=\left<i,0\right>; \\ 
      \left<j,0\right>  & \text{if } (i,R,k,j)\in \M, \\ 
                        & \quad      y = \bullet, x=\left<i,R\right>; \\
      \left<j,c\right>  & \text{if } (i,R,j)\text{ or } (i,R,k,j)\in \M, \\ 
                        & \quad      y = \circ, x = \left<i,c\right>; \\
      \quad \vdots
    \end{cases}
  }$
\end{column}
\begin{column}{0.45\textwidth}
  $\scriptsize \displaystyle{
    M'(x) = \begin{cases}
      \left<k,c\right>  &\text{if } (i,R,k,j)\in \M, \\
                        & \quad     x=\left<i,c\right>, c\neq R; \\
      \quad \vdots
    \end{cases}
  } $
\end{column}
\end{columns}

\pause\bigskip

Let $\M = \big\{ 
  \alert<6,12|handout:0>{(1,B,3,2)}, 
  \alert<9|handout:0>{(2,A,1)},
  \alert<16|handout:0>{(3,A,4)},
  \alert<20|handout:0>{(4,A,0)}
\big\}$. (\small $A+B+2$ from before)

\pause\bigskip

\begin{columns}
\begin{column}{0.72\textwidth}\begin{scriptsize}
  \vspace{-1em}
  \begin{align*}
    \uncover<5->{
    \uncover<8->{\textbf{1: } & M}
      \pmat{ \left<1,0\right> \uncover<8->{,\circ} \\
             \left<1,A\right> \uncover<8->{,\circ} \\
             \left<1,B\right> \uncover<8->{,\bullet} \\
             \left<1,0\right> \uncover<8->{,\circ} }
      \uncover<8->{ = \pmat{ \left<2,0\right> \\
                       \left<2,A\right> \\
                       \left<2,0\right> \\
                       \left<2,0\right> } }
    }
    &
    \uncover<18->{
    \textbf{4: } & M\pmat{ \left<3,0\right>, \bullet \\
                           \left<3,A\right>, \circ \\
                           \left<3,0\right>, \circ \\
                           \left<3,A\right>, \circ }
      \uncover<19->{ = \pmat{ \left<4,A\right> \\
                              \left<4,A\right> \\
                              \left<4,0\right> \\
                              \left<4,A\right> } \\ }
    }
    \uncover<10->{
    \textbf{2: } & M\pmat{ \left<2,0\right>, \circ \\
                           \left<2,A\right>, \circ \\
                           \left<2,0\right>, \circ \\
                           \left<2,0\right>, \bullet }
      \uncover<11->{ = \pmat{ \left<1,0\right> \\
                              \left<1,A\right> \\
                              \left<1,0\right> \\
                              \left<1,A\right> } }
    }
    &
    \uncover<22->{
    \textbf{5: } & M\pmat{ \left<4,A\right>, \circ \\
                           \left<4,A\right>, \circ \\
                           \left<4,0\right>, \bullet \\
                           \left<4,A\right>, \circ }
      \uncover<23->{ = \pmat{ \left<0,A\right> \\
                              \left<0,A\right> \\
                              \left<0,A\right> \\
                              \left<0,A\right> } \\ }
    }
    \uncover<14->{
    \textbf{3: } & M'\pmat{ \left<1,0\right> \\
                            \left<1,A\right> \\
                            \left<1,0\right> \\
                            \left<1,A\right> }
      \uncover<15->{ = \pmat{ \left<3,0\right> \\
                              \left<3,A\right> \\
                              \left<3,0\right> \\
                              \left<3,A\right> } }
    }
  \end{align*}
\end{scriptsize} \end{column}
\begin{column}{0.28\textwidth}\begin{scriptsize}
  \begin{tabular}{cccc}
    \textbf{Step} & \textbf{State} & \textbf{A} & \textbf{B} \\ \hline
    \uncover<4->{0 & 1 & 1 & 1} \\
    \uncover<7->{1 & \alert<7|handout:0>{2} & 1 & \alert<7|handout:0>{0}} \\
    \uncover<10->{2 & \alert<10|handout:0>{1} & \alert<10|handout:0>{2} & 0} \\
    \uncover<13->{3 & \alert<13|handout:0>{3} & 2 & 0} \\
    \uncover<17->{4 & \alert<17|handout:0>{4} & \alert<17|handout:0>{3} & 0} \\
    \uncover<21->{5 & \alert<21|handout:0>{0} & \alert<21|handout:0>{4} & 0}
  \end{tabular}
  \vspace{6em}
\end{scriptsize} \end{column}
\end{columns}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Computational relations}   % {{{
Let $\m{S}_n = \Sg_{\A(\M)^n}\left\{ \scriptsize
      \pmat{ \bullet \\ \circ \\ \vdots \\ \circ },
      \pmat{ \circ \\ \bullet \\ \vdots \\ \circ },
      \ldots,
      \pmat{ \circ \\ \circ \\ \vdots \\ \bullet } \right\}.$

\pause\medskip

\begin{itemize}
  \item $\left<1,0\right>$ is a constant, so every relation of $\A(\M)$
    contains
    $\scriptsize\displaystyle{ \pmat{ \left<1,0\right> \\ \vdots \\ \left<1,0\right> } }$.

  \pause\medskip

  \item This represents a configuration in state 1, with A and B registers 0.

  \pause\medskip

  \item The generators allow for simulated computation inside the relation.
\end{itemize}

\pause\medskip

\begin{thm}
$\M$ halts if and only if eventually
$( M_0\setminus \{\left<0,\times\right>\} )^n \cap S_n \neq\emptyset$.
\end{thm}
\end{frame}
%============================================================================}}}

\section{Main results, elements of the proof}
% TOC {{{
\begin{frame} \frametitle{Decidability in universal algebra}
\tableofcontents[currentsection]
\end{frame}
%============================================================================}}}
\begin{frame}  % Theorem statements {{{
\begin{thm}
\pause Let $\M$ be a Minksky machine, 
$\mathcal{R}_n = \bigcup\limits_{k=1}^n \S(\A(\M)^k)$, and $\m{S}_m$ be as
before.
\pause The following are equivalent:
\begin{columns} 
\begin{column}{0.25\textwidth} 
  \begin{itemize}
    \pause\item $\M$ halts, \vspace{1.5em}
  \end{itemize}
\end{column}
\begin{column}{0.65\textwidth} 
  \begin{itemize}
    \pause\item eventually $\mathcal{R}_n \models \m{S}_m$ for all $m\geq n$,
    \pause\item eventually $\mathcal{R}_n \models_d \m{S}_m$ for all $m\geq n$.
  \end{itemize}
\end{column}
\end{columns}
\end{thm}

\pause\medskip

$\A(\M)$ is not finitely (duality) related if $\M$ does not halt.

\pause\medskip 

Make $\A(\M)$ into a partial algebra (call it $\A^*(\M)$) \\
\pause \qquad \qquad $\rightsquigarrow$ fewer relations
\pause $\rightsquigarrow$ finitely (duality) related?

\pause\medskip

\begin{thm}
Let $\mathcal{R}^*_n = \bigcup\limits_{k=1}^n \S(\A^*(\M)^k)$.
\pause The following are equivalent:
\begin{columns}
\begin{column}{0.25\textwidth} 
  \begin{itemize}
    \pause\item $\M$ halts, \vspace{1.5em}
  \end{itemize}
\end{column}
\begin{column}{0.65\textwidth} 
  \begin{itemize}
    \pause\item eventually $\mathcal{R}^*_n \models \mathcal{R}^*_{\omega}$,
    \pause\item eventually $\mathcal{R}^*_n \models_d \mathcal{R}^*_{\omega}$.
  \end{itemize}
\end{column}
\end{columns}
\end{thm}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Coding theorem}   % {{{
\begin{thm}
$\M$ halts if and only if eventually
$( M_0\setminus \{\left<0,\times\right>\} )^n \cap S_n \neq\emptyset$.
\end{thm}

\pause

Define another operation of $\A(\M)$:
\[ \scriptsize
  N(u,x,y,z) = \begin{cases}
    m   & \text{if } u \in M_0\setminus \{\left<0,\times\right>\}, \\
        & \quad (x,y,z) \text{ is NU with majority}=m; \\
    (x\wedge y) \vee (x\wedge z) & \text{elif } u \in M_0\setminus \{\left<0,\times\right>\}; \\
    w   & \text{else, where } w = \left<i,\times\right> \text{ if } x\in M_i \\
        & \qquad \text{and } w = \times \text{ otherwise}.
  \end{cases}
\]

\pause

It follows that if 
$( M_0\setminus \{\left<0,\times\right>\} )^n \cap S_n \neq\emptyset$,
then $\m{S}_n$ has an NU polynomial.

\pause\bigskip

\begin{thm}
Let $\M$ be a Minsky machine. The following are equivalent:
\begin{columns}
\begin{column}{0.23\textwidth}
  \begin{itemize}[leftmargin=*]
    \pause\item $\M$ halts, \vspace{1.5em}
  \end{itemize}
\end{column}
\begin{column}{0.57\textwidth}
  \begin{itemize}[leftmargin=*]
    \pause\item eventually $\m{S}_n$ has an NU polynomial,
    \pause\item eventually $\left(\circ, \circ, \ldots, \circ\right) \in S_n$,
  \end{itemize}
\end{column}
\end{columns}
\end{thm}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{If $\M$ does not halt}   % {{{
If $\mathcal{R}_n \models \m{R}$, then \pause
$\displaystyle{
  \m{R} = \pi\left( \; 
    \bigcap_{i\in I} \mu_i\Big( \; 
    \textstyle{\prod\limits_{j\in J}} \; \m{R}_{ij} 
    \Big) \right)
}$

\pause

for some $\m{R}_{ij}\in \mathcal{R}_n$, finite sets $I, J$, permutations
$\mu_i$, and projection $\pi$.

\pause

\begin{lem}
If
\[
  m\left\{ 
    \pmat{ \bullet \\ \circ \\ \vdots \\ \circ },
    \pmat{ \circ \\ \bullet \\ \vdots \\ \circ },
    \ldots,
    \pmat{ \circ \\ \circ \\ \vdots \\ \bullet } \right.
  \uncover<5->{\in 
  \pi\left( \; 
    \bigcap_{i\in I} \mu_i\Big( \; 
    \textstyle{\prod\limits_{j\in J}} \; \m{R}_{ij} 
    \Big) \right)
  }
  \uncover<6->{ = \m{T} }
\]

\uncover<7->{where $m>n$ and $\m{R}_{ij}\in \mathcal{R}_n$,}
\uncover<8->{then $(\circ, \circ, \ldots, \circ) \in T$.}
\end{lem}

\medskip\uncover<9->{
In particular, if $\mathcal{R}_n\models \m{S}_m$ for some $m>n$, then
$(\circ,\ldots,\circ)\in S_m$.}

\medskip\uncover<10->{
From the coding theorem, this holds if and only if $\M$ halts.}

\medskip\uncover<11->{
$\M$ does not halt 
\uncover<12->{$\Rightarrow$ $\mathcal{R}_n\not\models \m{S}_m$}
\uncover<13->{$\Rightarrow$ $\A(\M)$ is not finitely (duality) related.}
}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{If $\M$ halts}   % {{{
\textbf{The coding theorem:} \\
if $\M$ halts, then eventually $\m{S}_n$ has a 3-ary NU polynomial.

\pause\medskip

Let $m(x,y,z)$ be the NU polynomial and define

\pause\vspace{-1.5em}

\[
  \m{S}_n^i = \Big\{ (s_1,\ldots,\stackrel{i}{\hat{a_i}},\ldots,s_n) \mid
    \exists s_i (s_1,\ldots,\stackrel{i}{\hat{s_i}},\ldots,s_n)\in S_n \Big\},
  \qquad\uncover<4->{\hat{\m{S}}_n = \bigcap_{i=1}^n \m{S}_n^i.}
\]

\vspace{-0.5em}

\uncover<5->{Each $\m{S}_n^i$ is a permutation of 
$\A(\M)\times \m{S}_{n-1}$.}
\uncover<6->{Thus, $\mathcal{R}_{n-1} \models_d \hat{\m{S}}_n$.}

\medskip

\uncover<7->{$S_n\subseteq S_n^i$, so $S_n\subseteq \hat{S}_n$.}
\uncover<8->{If $(a_1,\ldots,a_n)\in \hat{S}_n\setminus S_n$, then there are
$b_i$ such that}

\vspace{-0.5em}

\uncover<9->{ \[
  \pmat{ b_1 \\ a_2 \\ \vdots \\ a_n},
  \pmat{ a_1 \\ b_2 \\ \vdots \\ a_n},
  \ldots,
  \pmat{ a_1 \\ a_2 \\ \vdots \\ b_n}
  \in S_n.
\] }

\vspace{-0.5em}

\uncover<10->{Since $m(x,y,z)$ is a polynomial of $\m{S}_n$, applying
$m(x,y,z)$ to any 3 yields $(a_1,\ldots,a_n)\in S_n$.}
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{If $\M$ halts}   % {{{
\begin{itemize}
  \item We have that eventually $\mathcal{R}_n\models \m{S}_m$, $m>n$.

    \pause\medskip

    What about other relations $\m{R}\leq \A(\M)^m$?

  \pause\medskip

  \item If $\m{R}$ contains a member of
    $(M_0\setminus\{\left<0,\times\right>\})^m$ then it has an NU polynomial
    (call $\m{R}$ \emph{halting}).

  \pause\medskip

  \item $\m{A}(\M)$ has operation
  \vspace{-0.5em}
  \[
    P(u,v,x,y) = \begin{cases}
      x & \text{if } u,v\in M_i \text{ or } u,v\in \Sigma, \\
      y & \text{otherwise}.
    \end{cases}
  \]

  \pause

  If $\m{R}$ is not a subset of $\Sigma^m \cup M_0^m \cup \cdots \cup
  M_N^m$, then $\m{R}$ directly decomposes (call $\m{R}$
  \emph{non-synchronized}).

  \pause\medskip

  \item Thus, the problematic relations are the non-halting, synchronized,
    $\cap$-irreducible relations.

  \pause\medskip

  In the partial algebra construction, these are very easy to understand.
\end{itemize}
\end{frame}
%============================================================================}}}

\section{Conclusion}
% TOC {{{
\begin{frame} \frametitle{Decidability in universal algebra}
\tableofcontents[currentsection]
\end{frame}
%============================================================================}}}
\begin{frame} \frametitle{Other directions}   % {{{
\begin{Q}
If $\M$ halts, is $\A(\M)$ finitely related?
\end{Q}

\pause

(tentative yes, but \emph{very} complicated)

\pause\vfill

$\A(\M)$ has a semilattice operation, so it is SD$(\wedge)$.
\pause
\begin{Q}
What are the connections between SD$(\wedge)$, residual size, finite
axiomatizability, and dualizability?

\pause\medskip

Is $\A(\M)$ finitely axiomatizable? Is $\A(\M)$ residually small?
\end{Q}
\end{frame}
%============================================================================}}}
\begin{frame}[t] \frametitle{Conclusion}   % {{{
\begin{thm}
\pause Let $\M$ be a Minsky machine.

Let $\mathcal{R}_n = \bigcup\limits_{k=1}^n \S(\A(\M)^k)$, and $\m{S}_m$ be as before.


Let $\mathcal{R}^*_n = \bigcup\limits_{k=1}^n \S(\A^*(\M)^k)$. ($\A^*(\M)$
is the partial algebra)

\pause\medskip

The following are equivalent:
\begin{itemize}
  \pause\item $\M$ halts,
  \pause\item for some $n$, $\mathcal{R}_n \models \m{S}_m$ for all $m\geq n$,
  \pause\item for some $n$, $\mathcal{R}_n \models_d \m{S}_m$ for all $m\geq n$,
  \pause\item for some $n$, $\mathcal{R}^*_n \models \mathcal{R}^*_{\omega}$,
  \pause\item for some $n$, $\mathcal{R}^*_n \models_d \mathcal{R}^*_{\omega}$.
\end{itemize}
\end{thm}

\pause\vfill

\begin{center}
  \textbf{Thank you.}
\end{center}
\end{frame}
%============================================================================}}}
\end{document}
