%\documentclass[compress]{beamer}  % {{{1
\documentclass[compress, handout]{beamer}
\usepackage{amsfonts, amsmath, amssymb, amsthm, mathtools}
\usepackage{enumitem, float, graphicx, hyperref, multirow, tikz}

% tikz settings
\usetikzlibrary{arrows, calc, decorations.markings, matrix, positioning}
\tikzset{>=latex}

% beamer settings
\let\emph\textbf
% enumitem/beamer compatibility
\setitemize{label=\usebeamerfont*{itemize item}
  \usebeamercolor[fg]{itemize item}
  \usebeamertemplate{itemize item}}
\setbeamertemplate{items}[circle]
% color settings
\mode<presentation>{
  \usetheme{Madrid}
  \usecolortheme{default}
  \beamertemplatenavigationsymbolsempty
}
\setbeamercolor{alerted text}{fg=blue}

% mathbb and mathcal symbols
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\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}[section]  \newtheorem*{thm*}{Theorem}
  \newtheorem{claim}[thm]{Claim}      \newtheorem*{claim*}{Claim}
  \newtheorem{conj}[thm]{Conjecture}  \newtheorem*{conj*}{Conjecture}
  \newtheorem{cor}[thm]{Corollary}    \newtheorem*{cor*}{Corollary}
  \newtheorem{lem}[thm]{Lemma}        \newtheorem*{lem*}{Lemma}
  \newtheorem{prop}[thm]{Proposition} \newtheorem*{prop*}{Proposition}
\theoremstyle{definition}
  \newtheorem{defn}[thm]{Definition} \newtheorem*{defn*}{Definition}
  \newtheorem{ex}[thm]{Example}      \newtheorem*{ex*}{Example}
\theoremstyle{remark}
  \newtheorem{rk}[thm]{Remark}  \newtheorem*{rk*}{Remark}
\newcommand{\Case}[1]{\smallskip \textbf{Case #1:}}
\newenvironment{claimproof} {
  \begin{proof}[Proof of claim]
  \renewcommand{\qedsymbol}{\ensuremath{\circ}}
  } {
  \end{proof}
  }

% custom math commands
\DeclareMathOperator{\Cg}{Cg}
\DeclareMathOperator{\Clo}{Clo}
\DeclareMathOperator{\Con}{Con}
\DeclareMathOperator{\Rel}{Rel}
\DeclareMathOperator{\Sg}{Sg}
\DeclareMathOperator{\diag}{diag}
\newcommand{\bmat}[1]{ \begin{bmatrix} #1 \end{bmatrix} }
\newcommand{\Bmat}[1]{ \begin{Bmatrix} #1 \end{Bmatrix} }
\newcommand{\pmat}[1]{ \begin{pmatrix} #1 \end{pmatrix} }
\newcommand{\mat}[1]{ \begin{matrix} #1 \end{matrix} }
\newcommand{\vect}[1]{ \left< #1 \right> }
\newcommand{\ds}[1]{ \displaystyle{#1} }
\newcommand{\stack}[2]{\genfrac{}{}{0pt}{}{#1}{#2}}

% misc
\renewcommand{\epsilon}{\varepsilon}
\renewcommand{\phi}{\varphi}
\newcommand{\slidefinish}{\hfill$\cdot$}
\newcommand{\TODO}[1]{\noindent\textbf{TODO: #1}}

% document specific stuff
% utilities
\usepackage{booktabs}
\theoremstyle{definition} \newtheorem*{prob}{Problem}
\newcommand{\Proofitem}[1]{\smallskip \textbf{#1:}}
\newcommand{\AMConfig}[1]{ \big[\!\big[\ #1\ \big]\!\big] }
\newcommand{\Row}[1]{ [\![ #1 ]\!] }
\theoremstyle{plain} \newtheorem{thmsmall}{\small Theorem} \newtheorem{lemsmall}{\small Lemma}

% A(M) and relations
\newcommand{\M}{\mathcal{M}}
\newcommand{\AM}{A(\M)}
\newcommand{\AAM}{\mathbb{\AM}}
\let\SS\relax \newcommand{\SS}{\mathbb{S}}
\DeclareMathOperator{\Config}{\tt c}

% content, state, pattern, and related
\newcommand{\StateGraph}{\Sigma}
\DeclareMathOperator{\Content}{\tt con}
\DeclareMathOperator{\State}{\tt st}
\DeclareMathOperator{\X}{\tt X}
\newcommand{\Er}{\times}
\renewcommand{\Dot}{\bullet}

% dot, approx halt, inherent non-halt
\newcommand{\D}{\mathcal{D}}
\renewcommand{\H}{\mathcal{H}}
\newcommand{\N}{\mathcal{N}}

% rel, pol, entails
\DeclareMathOperator{\Pol}{Pol}
\DeclareMathOperator{\RClo}{RClo}
\DeclareMathOperator{\RCloDual}{\RClo^{\partial}}
\newcommand{\Entails}{\models}
\newcommand{\EntailsDual}{\models_{\partial}}

% misc
\DeclareMathOperator{\maxdeg}{maxdeg}
\DeclareMathOperator{\Approx}{A}
\DeclareMathOperator{\ApproxI}{\Approx_I}
%----------------------------------------------------------------------------}}}1

\begin{document}
% title page {{{1
\title[Indecision]{Indecision: finitely generated, finitely related clones}
\subtitle{(finite degree clones are undecidable)}
\author{Matthew Moore}
\institute[KU]{The University of Kansas \\
  \tiny Department of Electrical Engineering and Computer Science}
\date[2019-03-22]{March 22, 2019}

\begin{frame}
\titlepage
\end{frame}
%----------------------------------------------------------------------------}}}1

% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{Clones}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % defn, post's lattice {{{1
\begin{columns}
  \begin{column}{0.41\textwidth}
    \vfill
    A \emph{clone} is a set of finitary operations closed under
    \begin{itemize}
      \uncover<2->{ \item composition, }
      \uncover<3->{ \item variable identification, }
      \uncover<4->{ \item variable permutation, }
      \uncover<5->{ \item introduction of extraneous variables. }
    \end{itemize}

    \bigskip

    \uncover<6->{ Emil Post in 1941 famously classified all Boolean clones. }

    \bigskip

    \uncover<7->{ Over $(\geq 3)$-element domains structure is quite complicated. }
    \vfill
  \end{column}
  \begin{column}{0.53\textwidth}
    \uncover<6->{ \includegraphics[height=21em,width=17em]{post-lattice.png} }
  \end{column}
\end{columns}
\uncover<7->{ \slidefinish }
\end{frame}  % }}}1
\begin{frame}  % pol and rel {{{1
Clones are infinite. How can they be an input to an algorithm?

\bigskip\pause

A clone on \underline{finite} domain $A$ can be \emph{finitely specified} in
essentially 2 ways.

\bigskip\pause

\emph{First way:} 
Given $\cl{F}$, a finite set of operations of $A$, define \\
$\Clo(\cl{F}) =$ ``the smallest clone containing $\cl{F}$''.
\begin{itemize}
  \pause\item $A$ with $\cl{F}$ forms a algebra, $\A = \left< A; \cl{F} \right>$.
    Define $\Clo(\A) = \Clo(\cl{F})$.
  \pause\item A \emph{relation} of $\A$ is a subpower $R\subseteq A^n$
    closed under $\cl{F}$ (hence $\Clo(\cl{F})$)
  \pause\item Define $\Rel_n(\A) = \Rel_n(\cl{F}) = $ ``all $(\leq n)$-ary
    relations of $\A$''.
  \pause\item Define $\ds{ \Rel(\A) = \Rel_n(\cl{F}) = \bigcup_{n<\infty}
    \Rel_n(\A) }$
\end{itemize}
\pause These are the \emph{finitely generated} clones

\bigskip\pause

\emph{Second way:} Given $\cl{R}$, a finite set of subpowers of $A$, define \\
$\Pol(\cl{R}) =$ ``the set of all operations of $A$ preserving all subpowers
in $\cl{R}$''.

\medskip\pause

These are the \emph{finitely related}/\emph{finite degree} clones.
\slidefinish
\end{frame}  % }}}1
\begin{frame}  % galois connection {{{1
\vspace{-1.5em}
\begin{align*}
  \Rel(\mathcal{F}) 
  & = \big\{ R\subseteq A^n \mid R \text{ is preserved by all operations 
    in } \mathcal{F} \big\} \\
  \Pol(\mathcal{R}) 
  & = \big\{ f: A^n\to A \mid f \text{ preserves all subpowers in }
    \mathcal{R} \big\} \\
\end{align*}
\vspace{-2.5em}

\pause

These two operators form a \emph{Galois connection}.
\vspace{-1em}
\begin{columns}
\begin{column}{0.3\textwidth}
  \vfill
  \begin{gather*}
    \cl{R} \subseteq \Rel(\cl{F}) \\[1ex]
    \Longleftrightarrow \\[1ex]
    \cl{F} \subseteq \Pol(\cl{R})
  \end{gather*}
  \vfill
\end{column}
\begin{column}{0.7\textwidth}
  \begin{center} \begin{tikzpicture}[font=\scriptsize,scale=1.2]
    \path   (0,0)     node (RelF) {$\Rel(\cl{F})$}
           +(0,-0.75) node (R)    {$\cl{R}$}
          ++(4,0)     node (F)    {$\cl{F}$}
           +(0,-0.75) node (PolR) {$\Pol(\cl{R})$};

    \draw ($(RelF)+(0,-0.25)$) circle (1)
      ($(PolR)+(0,0.5)$) circle (1)
      ($(R)+(0.25,0.25)$) rectangle ++(-0.5,-0.5)
      ($(F)+(0.25,0.25)$) rectangle ++(-0.5,-0.5);

    \draw[->] (R) to node[auto,swap]{$\Pol$} (PolR);
    \draw[->] (F) to node[auto,swap]{$\Rel$} (RelF);
  \end{tikzpicture} \end{center}
\end{column}
\end{columns}

\pause

Every Galois connection defines two closure operators. Here, they are
\[
  \Clo = \Pol\circ\Rel
  \qquad \text{and} \qquad
  \RClo = \Rel\circ\Pol.
\]

\pause

If $\RR\in \RClo(\cl{S})$, then we say ``$\cl{S}$ entails $\RR$'' and write
$\cl{S} \Entails \RR$

\bigskip\pause

If $f\in \Pol(\cl{S})$, then we say ``$\cl{S}$ entails $f$'' and write
$\cl{S} \Entails f$.
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{The finite degree problem}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % statement of problem {{{1
For a set of relations $\cl{S}$, define
\[
  \deg(\cl{S}) = \sup \big\{ \text{arity}(\RR) \mid \RR\in \cl{S} \big\}.
\]

\pause

For a clone $\cl{C}$, define
\[
  \deg(\cl{C})
  = \inf \big\{ \deg(\cl{S}) \mid \Pol(\cl{S}) = \cl{C} \big\}.
\]

\pause

For an algebra $\A$, define
\[
  \deg(\A) = \deg(\Clo(\A)).
\]

\pause\bigskip

\emph{The Finite Degree Problem}
\begin{itemize}[leftmargin=6em]
  \item[\texttt{Input:}] $\cl{F}$, a finite set of operations on a finite
    domain.
  \item[\texttt{Output:}] whether $\deg(\Clo(\cl{F})) < \infty$.
\end{itemize}

\pause\bigskip

(Seems to originate in the 70s with the study of lattices of clones over
more than $2$ element domains.)
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % thm statement, history {{{1
\emph{The Finite Degree Problem}
\begin{itemize}[leftmargin=6em]
  \item[\texttt{Input:}] $\cl{F}$, a finite set of operations on a finite
    domain.
  \item[\texttt{Output:}] whether $\deg(\Clo(F)) < \infty$.
\end{itemize}

\pause\bigskip

Given a Minsky machine $\M$, we encode it into a finite algebra $\AAM$.

\pause

\begin{thm*}
The following are equivalent.
\begin{itemize}
  \item $\M$ halts,
  \item $\deg(\AAM) < \infty$ (i.e.\ $\AAM$ is finitely related),
\end{itemize}
\end{thm*}

\pause\bigskip

Similar approaches have proved the following are undecidable:
\begin{itemize}
  \pause\item finite residual bound (McKenzie)
  \pause\item finite axiomatizability/Tarski's problem (McKenzie)
  \pause\item existence of a term op.\ that is NU on all but 2 elements (Maroti)
  \pause\item DPSC, leading to another solution to Tarski's problem (M)
  \pause\item profiniteness (Nurakunov and Stronkowski)
  \slidefinish
\end{itemize}
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{The encoding of computation}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % Minsky machines {{{1
A Minsky machine has...
\medskip
\begin{itemize}[itemsep=1em]
  \pause\item states $0, 1, \ldots, N$ ($1$ is the starting state, $0$ is
    the halting state),
  \pause\item registers $A$ and $B$ that have integer values $\geq 0$,
  \pause\item instructions of the form $(i,R,j)$, meaning \\
    ``in state $i$, increase register $R$ by 1 and enter $j$''.
  \pause\item instructions of the form $(i,R,j,k)$, meaning \\
    ``in state $i$, if $R$ is $0$ enter $j$, otherwise decrease $R$ by $1$
    and enter $k$''.
\end{itemize}

\pause\medskip

In this talk, $\M$ is some fixed Minsky machine.
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % Minsky machines {{{1
Let $\mathcal{M}$ have instructions
\vspace{-0.5em} \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} \vspace{-0.5em} 
\pause Start the machine with register contents $A = 3$, $B = 2$. 
\pause\smallskip
\begin{columns} \small
\begin{column}{0.4\textwidth}
  \begin{tabular}{cccc}
    \textbf{Step}   & \textbf{State}                                          & \textbf{A }                             & \textbf{B } \\ \midrule
    \uncover<8-> {0 & \uncover<25->{(}1\uncover<25->{,}                       & 3\uncover<25->{,}                       & 2\uncover<25->{)}} \\
    \uncover<10->{1 & \uncover<25->{(}\alert<10|handout:0>{2\uncover<25->{,}} & 3\uncover<25->{,}                       & \alert<10|handout:0>{1}\uncover<25->{)}} \\
    \uncover<12->{2 & \uncover<25->{(}\alert<12|handout:0>{1\uncover<25->{,}} & \alert<12|handout:0>{4}\uncover<25->{,} & 1\uncover<25->{)}} \\
    \uncover<14->{3 & \uncover<25->{(}\alert<14|handout:0>{2\uncover<25->{,}} & 4\uncover<25->{,}                       & \alert<14|handout:0>{0}\uncover<25->{)}}
  \end{tabular}
\end{column} 
\begin{column}{0.4\textwidth}
  \begin{tabular}{cccc}
    \textbf{Step}   & \textbf{State}                                          & \textbf{A }                             & \textbf{B } \\ \midrule
    \uncover<16->{4 & \uncover<25->{(}\alert<16|handout:0>{1}\uncover<25->{,} & \alert<16|handout:0>{5}\uncover<25->{,} & 0\uncover<25->{)}} \\
    \uncover<18->{5 & \uncover<25->{(}\alert<18|handout:0>{3}\uncover<25->{,} & 5\uncover<25->{,}                       & 0\uncover<25->{)}} \\
    \uncover<20->{6 & \uncover<25->{(}\alert<20|handout:0>{4}\uncover<25->{,} & \alert<20|handout:0>{6}\uncover<25->{,} & 0\uncover<25->{)}} \\
    \uncover<22->{7 & \uncover<25->{(}\alert<22|handout:0>{0}\uncover<25->{,} & \alert<22|handout:0>{7}\uncover<25->{,} & 0\uncover<25->{)}}
  \end{tabular}
\end{column} 
\end{columns}

\smallskip

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

\medskip

\uncover<24->{ A \emph{configuration} $(i,\alpha,\beta)$ represents each stage of computation. }

\medskip

\uncover<26->{ Consider $\cl{M}$ as a function, and write
\vspace{-0.5em} \[
  \M(i,\alpha,\beta) = (j,\alpha',\beta') 
  \qquad\text{or}\qquad
  \M^n(i,\alpha,\beta) = (j,\alpha',\beta')
\vspace{-0.5em} \] 
(single step of computation or multiple). }

\medskip

\uncover<27->{ The \emph{capacity} of $\M$ is the max sum of the registers. }
\uncover<27->{ \slidefinish }
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % Minsky machines {{{1
The algebra $\AAM$ has set
\[
  \AM
  = \big\{ \vect{i,0}, \vect{i,A}, \vect{i,B}, \vect{i,\Dot}, \vect{i,\Er} 
    \mid i \text{ a state of } \M \big\}
\]

\pause

The algebra is \quad
$\ds{ \AAM = \big< \AM\;;\; \wedge, M, M', I, H, N_0, S, N_\Dot, P \big> }$.

\pause\bigskip

\begin{scriptsize} \begin{columns}
  \begin{column}{0.57\textwidth}
    $\scriptsize \displaystyle{
      M(x,y) = \begin{cases}
        \vect{j,R}   & \text{if } (i,R,j)\in \M, \\ 
                     &   \qquad x=\vect{i,\Dot}, y=\vect{i,0}; \\
        \vect{j,0}   & \text{if } (i,R,k,j)\in \M, \\ 
                     &   \qquad x=\vect{i,\Dot}, y=\vect{i,R}; \\
        \vect{j,c}   & \text{if } \big[ (i,R,j) \text{ or } (i,R,k,j)\in \M \big], \\
                     &   \qquad x=y=\vect{i,c}; \\
        \vect{j,c}   & \text{if } y=\vect{i,c}, M(y,x) = \vect{j,d}, \\
                     &   \qquad d\neq \Er, \text{ by above rules}; \\
        \vect{j,\Er} & \text{otherwise}^*
      \end{cases}
    }$
  \end{column} \pause
  \begin{column}{0.46\textwidth}
    $\scriptsize \displaystyle{
      M'(x) = \begin{cases}
        \vect{k,c} & \text{if } (i,R,k,j)\in \M, \\
                          & \qquad     x=\vect{i,c}, c\neq R; \\
        \vect{k,\Er} & \text{otherwise}^*
      \end{cases}
    } $
  \end{column}
\end{columns} \end{scriptsize}

\bigskip

\begin{itemize} \small
  \pause\item $M$ encodes addition and subtraction operations.
  \pause\item $M'$ encodes testing for $0$ in a register.
  \pause\item $M(x,y) \neq \vect{*,\Er}$ implies $x=y$ modulo a single coordinate
    transposition. 
  \slidefinish
\end{itemize}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}[t]  % A(M) calculation {{{1
\small
\begin{columns}
\begin{column}{0.57\textwidth}
  $\scriptsize \displaystyle{
    M(x,y) = \begin{cases}
      \vect{j,R}  & \text{if } (i,R,j)\in \M, \\ 
                  &   \qquad x=\vect{i,\Dot}, y=\vect{i,0}; \\
      \vect{j,0}  & \text{if } (i,R,k,j)\in \M, \\ 
                  &   \qquad x=\vect{i,\Dot}, y=\vect{i,R}; \\
      \vect{j,c}  & \text{if } \big[ (i,R,j) \text{ or } (i,R,k,j)\in \M \big], \\
                  &   \qquad x=y=\vect{i,c}; \\
      \vect{j,c}  & \text{if } y=\vect{i,c}, M(y,x) = \vect{j,d}, \\
                  &   \qquad d\neq \Er, \text{ by above rules}; \\
      \ \,\cdots  & \cdots \qquad \cdots \qquad \cdots \qquad \cdots
    \end{cases}
  }$
\end{column}
\begin{column}{0.46\textwidth}
  $\scriptsize \displaystyle{
    M'(x) = \begin{cases}
      \vect{k,c} & \text{if } (i,R,k,j)\in \M, \\
                        & \qquad     x=\vect{i,c}, c\neq R; \\
    \ \,\cdots   & \cdots \qquad \cdots \qquad \cdots
    \end{cases}
  } $
\end{column}
\end{columns}

\pause \medskip

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\medskip

\begin{columns}
\begin{column}{0.72\textwidth} \begin{scriptsize}
  \arraycolsep=0.1em
  \vspace{-1em}
  \[ \hspace{-0.5em} \begin{array}{llll}
    \uncover<5->{
    \uncover<8->{\textbf{1:} & M}
      \pmat{ \vect{1,\Dot} \uncover<8->{,\vect{1,B}}    \\
             \vect{1,0}    \uncover<8->{,\vect{1,0}}    \\
             \vect{1,0}    \uncover<8->{,\vect{1,0}}    \\
             \vect{1,B}    \uncover<8->{,\vect{1,\Dot}} }
      \uncover<8->{ = \pmat{ \vect{2,0} \\
                             \vect{2,0} \\
                             \vect{2,0} \\
                             \vect{2,\Dot} } }
    }
    &
    \uncover<18->{
    \textbf{4:} & M\pmat{ \vect{3,\Dot}, \vect{3,0}    \\
                           \vect{3,0},    \vect{3,\Dot} \\
                           \vect{3,0},    \vect{3,0}    \\
                           \vect{3,A},    \vect{3,A}    }
      \uncover<19->{ = \pmat{ \vect{4,A}    \\
                              \vect{4,\Dot} \\
                              \vect{4,0}    \\
                              \vect{4,A}    } \\[5ex] }
    }
    \uncover<10->{
    \textbf{2:} & M\pmat{ \vect{2,0},    \vect{2,\Dot} \\
                           \vect{2,0},    \vect{2,0}    \\
                           \vect{2,0},    \vect{2,0}    \\
                           \vect{2,\Dot}, \vect{2,0}    }
      \uncover<11->{ = \pmat{ \vect{1,\Dot} \\
                              \vect{1,0}    \\
                              \vect{1,0}    \\
                              \vect{1,A}    } }
    }
    &
    \uncover<22->{
    \textbf{5:} & M\pmat{ \vect{4,A},    \vect{4,A}    \\
                           \vect{4,\Dot}, \vect{4,0}    \\
                           \vect{4,0},    \vect{4,\Dot} \\
                           \vect{4,A},    \vect{4,A}    }
      \uncover<23->{ = \pmat{ \vect{0,A}    \\
                              \vect{0,A}    \\
                              \vect{0,\Dot} \\
                              \vect{0,A} }  \\[5ex] }
    }
    \uncover<14->{
    \textbf{3:} & M'\pmat{ \vect{1,\Dot} \\
                            \vect{1,0}    \\
                            \vect{1,0}    \\
                            \vect{1,A}    }
      \uncover<15->{ = \pmat{ \vect{3,\Dot} \\
                              \vect{3,0}    \\
                              \vect{3,0}    \\
                              \vect{3,A}    } }
    }
  \end{array} \]
\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                       & 0                       & 1} \\
    \uncover<7->{1  & \alert<7|handout:0>{2}  & 0                       & \alert<7|handout:0>{0}} \\
    \uncover<10->{2 & \alert<10|handout:0>{1} & \alert<10|handout:0>{1} & 0} \\
    \uncover<13->{3 & \alert<13|handout:0>{3} & 1                       & 0} \\
    \uncover<17->{4 & \alert<17|handout:0>{4} & \alert<17|handout:0>{2} & 0} \\
    \uncover<21->{5 & \alert<21|handout:0>{0} & \alert<21|handout:0>{3} & 0}
  \end{tabular}
  \vspace{6em}
\end{scriptsize} \uncover<23->{ \vfill \slidefinish } \end{column}
\end{columns}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % computational relations {{{1
\emph{Takeaways:} \uncover<2->{ on a relation $\RR\leq \AAM^n$ ... }
\begin{itemize}
  \uncover<3->{ \item certain elements of $R$ encode configurations of $\M$, }
  \uncover<6->{ \item $M$ and $M'$ encode the action of $\M$ in the presence
    of certain elements of $R$. }
\end{itemize}

\medskip

\uncover<7->{ \emph{Questions} }
\begin{itemize}
  \uncover<8->{ \item What if $R$ doesn't contain these kinds of elements? }
  \uncover<9->{ \item What if $R$ contains elements that aren't
    ``computational'': \\ }
    \uncover<10->{ multiple $\Dot$'s or non-constant states. }
\end{itemize}

\medskip

\uncover<4->{ Given configuration $(k,\alpha,\beta)$, in $\AAM^n$ define
\begin{small} \[
  \Config(k,\alpha,\beta) \scriptsize
  = \uncover<5->{ \bigcup_{p\in P_n} \Big\{ p }
    \Big( \vect{k,\Dot},
          \underbrace{ \vect{k,A}, \dots, \vect{k,A} }_{\alpha},
          \underbrace{ \vect{k,B}, \dots, \vect{k,B} }_{\beta},
          \underbrace{ \vect{k,0}, \dots, \vect{k,0} }_{n-\alpha-\beta-1} \Big)
    \uncover<5->{ \Big\} }
\] \end{small} \hspace{-0.75em} }

\uncover<11->{ Call $\RR$ \emph{computational} if it doesn't contain any
elements with 2 $\Dot$'s or non-constant state.  }

\medskip

\uncover<12->{ The \emph{capacity} of computational $\RR$ is (number of
coordinates with $\Dot$)$ - 1$. \slidefinish }
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % coding theorem {{{1
Let $\SS_m = \Sg_{\AAM^m}\big( \Config(1,0,0) \big)$.

\pause

\begin{thm}[The Coding Theorem]
\begin{itemize}
  \pause\item If $\M^n(1,0,0) = (k,\alpha,\beta)$ and this computation has
  capacity $m-1$, then $\Config(k,\alpha,\beta)\subseteq S_m$.

  \pause\item If $\Config(k,\alpha,\beta)\subseteq S_m$ and $\M$ does not
  halt with capacity $m-1$ then for some $n$ we have $\M^n(1,0,0) =
  (k,\alpha,\beta)$ and this computation has capacity $m-1$.
\end{itemize}
\end{thm}

\pause \medskip

\begin{cor}
The following are equivalent.
\begin{itemize}
  \pause\item $\M$ halts with capacity $m-1$,

  \pause\item $\SS_m$ is halting,

  \pause\item every computational $\RR\leq \AAM^\ell$ with capacity $m-1$ is
  halting.
\end{itemize}
\end{cor}
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{Non-halting implies infinite degree}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % approach {{{1
\emph{Observe}
\begin{align*}
  \uncover<2->{ \deg(\cl{C}) = \infty } 
    & \uncover<3->{ \quad\text{if and only if}\quad 
        \Rel_n(\cl{C}) \not\Entails \Rel(\cl{C}) \text{ for all } n } \\
  & \uncover<4->{ \quad\text{if and only if}\quad 
      \Rel_n(\cl{C}) \not\Entails \RR \text{ for all } n \text{ and some } \RR }
\end{align*}

\bigskip

\uncover<5->{ \emph{Idea:} to show that $\deg(\AAM) = \infty$ when $\M$ does not halt, we prove the
last equivalence for $\cl{C} = \Clo(\AAM)$. }
\uncover<5->{ \slidefinish }
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % Zadori theorem {{{1
$\Rel_n(\cl{C}) \Entails \RR$ if and only if \pause $\RR$ can be built from
$\Rel_n(\cl{C})$, in finitely many steps, by applying the following
constructions:
\begin{itemize}
  \pause\item intersection of equal arity relations,
  \pause\item (cartesian) product of finitely many relations,
  \pause\item permutation of the coordinates of a relation, and
  \pause\item projection of a relation onto a subset of coordinates.
\end{itemize}

\pause\bigskip

\begin{thm}[Zadori 1995]
$\Rel_n(\A) \Entails \SS$ if and only if 
\[
  \SS
  = \pi \Bigg( \bigcap_{i\in I} \mu_i \Big( \prod_{j\in J_i} \RR_{ij} \Big) \Bigg)
\]
for some $\RR_{ij} \in \Rel_n(\A)$, some coordinate projection $\pi$, and
some coordinate permutations $\mu_i$.
\end{thm}
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % thm not fin related {{{1
\small
\begin{lemsmall}
Suppose that
\vspace{-1.25em} \[
  \Config(1,0,0)
  \subseteq \pi \Bigg( \bigcap_{i\in I} \mu_i \Big( \prod_{j\in J_i} \RR_{ij} \Big) \Bigg)
  = \SS
  \leq \AAM^m,
\vspace{-0.5em} \] 
where $\pi$ is a projection, the $\mu_i$ are permutations, and the
$\RR_{ij}$ are a finite collection of members of $\Rel_n(\AAM)$, and $n<m$.
\pause Then $\SS$ is halting.
\end{lemsmall}

\pause

\begin{thmsmall}
The following hold for any Minsky machine $\M$.
\begin{itemize}
  \pause\item If $\M$ does not halt with capacity $m$ then $m < \deg(\AAM)$.
  \pause\item If $\M$ does not halt then $\AAM$ is not finitely related.
\end{itemize}
\end{thmsmall}
\pause
\emph{Proof:}
Suppose that $\deg(\AAM) \leq m$. \pause This implies in particular that
$\Rel_m(\AAM) \Entails \SS_{m+1}$. \pause By Zadori's theorem, $\SS_{m+1}$
can be represented as in the Lemma above, \pause so by that same Lemma it is
halting. \pause By the Coding Theorem, this implies that $\M$ halts with
capacity $m$, a contradiction.
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{Halting implies finite degree}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % approach {{{1
\emph{Strategy}
\smallskip
\begin{itemize}[itemsep=0.75em]
  \pause\item The relations $\SS_m$ witnessed non-entailment when $\M$ did
  not halt. \pause When $\M$ does halt, these relations eventually witness
  the halting.

  \pause\item Show that for some suitably chosen $k$, we have $\Rel_k(\AAM)
  \Entails \Rel_n(\AAM)$ for all $n$.

  \pause\item We proceed with induction on $n$.

  \pause\item The base case of $n = k$ is trivial.

  \pause\item We thus endeavor to prove $\Rel_{n-1}(\AAM) \Entails \RR$ for
  $\RR\in \Rel_n(\AAM)$.

  \pause\item Relations in $\Rel_n(\AAM)$ can be divided into 4 different
  kinds, so we proceed by cases.

  \pause\item Recall
  $\ds{ \AAM = \big< \AM\;;\; \wedge, M, M', I, H, N_0, S, N_\Dot, P \big> }$. \\
  \smallskip\pause
  Different collections of operations handle entailment in each of the
  different cases.
  \slidefinish
\end{itemize}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % non-computational or halting {{{1
\vspace{-1em} \[
  \AAM = \big< \AM\;;\; \wedge, M, M', I, H, N_0, S, N_\Dot, P \big>
\]

\emph{Case $\RR$ is non-computational} 
\begin{itemize}
  \item There is an element with 2 $\Dot$'s or with non-constant state.

  \item 2 $\Dot$'s: operation $N_\Dot$ handles entailment.

  \item Non-constant state: operation $P$ handles entailment.
\end{itemize}

\begin{thmsmall} \small
If $m\geq 3$ and $\RR\leq \AAM^m$ is non-computational then
$\Rel_{m-1}(\AAM) \Entails \RR$.
\end{thmsmall}

\bigskip

\emph{Case $\RR$ is halting}
\begin{itemize}
  \item $R$ contains $\Config(0,0,0)$.
  \item Any element of $\Config(0,0,0)$ can be used with operations $I$,
    $H$, and $N_0$ to prove entailment.
\end{itemize}

\begin{thmsmall} \small
If $m\geq 3$ and $\RR\leq \AAM^m$ is halting then $\Rel_{m-1}(\AAM) \Entails
\RR$.
\end{thmsmall}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % inherent case {{{1
We are left to examine computational non-halting $\RR\leq \AAM^n$.

\pause\medskip

Let's say that $\M$ halts with capacity $\kappa$.

\pause\bigskip

\emph{Two metrics:} \pause (both subsets of $[n]$)
\smallskip
\begin{itemize}[itemsep=0.75em]
  \pause\item $\D(\RR) = $ ``coordinates $i$ such that $\exits r\in R$ with $r(i) = \vect{j,\Dot}$'' \\
    \pause\hspace{2.25em} $ = $ ``the $\Dot$ (dot) part of $\RR$.

  \pause\item $\N(\RR) = $ ``the inherently non-halting part of $\RR$'' ...
  \smallskip
  \begin{itemize}[itemsep=0.75em]
    \pause\item $\pi_{\N(\RR)}(\RR)$ is non-halting,

    \pause\item If $K = \big| \N(\RR)\cap \D(\RR) \big|$ then $\SS_K \leq
    \RR$.
  \end{itemize}
\end{itemize}

\pause\medskip

\emph{Case $\RR$ is computational and $|\N(\RR)\cap \D(\RR)| > \kappa$}
\begin{itemize}[itemsep=0.74em]
  \pause\item $\big| \N(\RR)\cap \D(\RR) \big| > \kappa$ then $\RR$ contains a
  halting subalgebra.

  \pause\item it follows that $\RR$ halts!
\end{itemize}

\pause\bigskip

We thus consider computational non-halting $\RR$ with $\big| \N(\RR)\cap
\D(\RR) \big| \leq \kappa$.
\slidefinish
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % last case, entailment theorem {{{1
\emph{Case computational non-halting $\RR$ with $\big| \N(\RR) \cap \D(\RR)
\big| \leq \kappa$}

\pause

\begin{thm}
Assume that $n \geq \kappa+16$ and
\smallskip
\begin{itemize}[itemsep=0.5em]
  \item $\RR \leq \AAM^n$ is computational non-halting,

  \item $\big| \N(\RR) \cap \D(\RR) \big| \leq \kappa$,

  \item \hspace{3em}$\vdots$\hspace{3em} (several technical hypotheses)
\end{itemize}
\smallskip
Then $\Rel_n(\AAM) \Entails \RR$.
\end{thm}

\pause\bigskip

This completes the case analysis!

\pause\bigskip

\begin{thm}
If $\M$ halts with capacity $\kappa$ then $\deg(\AAM)\leq \kappa+16$.
\slidefinish
\end{thm}
\end{frame}
%----------------------------------------------------------------------------}}}1

\section{Conclusion}
% TOC {{{1
\begin{frame} \frametitle{Indecision: finitely generated, finitely related clones}
\tableofcontents[currentsection]
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % final thm, observations {{{1
\begin{thm}
The following are equivalent.
\begin{itemize}
  \pause\item $\M$ halts,
  \pause\item $\deg(\AAM) < \infty$ (i.e.\ $\AAM$ is finitely related),
  \pause\item $\M$ halts with capacity $\deg(\AAM)$.
\end{itemize}
\end{thm}

\pause\bigskip

\emph{Interesting observations}
\begin{itemize}[itemsep=0.5em]
  \pause\item There are infinitely many $\M$ and $n\in \NN$ such that $\M$ halts
  in $\leq n$ steps but this is not provable in ZFC.

  \pause\item Thus, there are infinitely many $\M$ and $n\in \NN$ such that
  $\deg(\AAM)\leq n$ is true but not provable in ZFC.

  \pause\item There are finite algebras $\A$ that are finitely related but for
  which a bound on $\deg(\A)$ cannot be proven.

  \pause\item \begin{small} 
  $\ds{ 
    \text{maxdeg}_{\sigma}(n)
    = \text{sup}\Bigg\{ \deg(\A) \hspace{0.5em}\mid\hspace{0.5em}
      \begin{gathered}
        \A \text{ has signature } \sigma, \\
        \deg(\A)<\infty, \text{ and } |A|\leq n
      \end{gathered}
      \Bigg\}
    }$ \end{small} \\[1ex]
  \pauseis not computable. 
  \slidefinish
\end{itemize}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % open problems {{{1
\begin{prob}[Finite Generation Problem]
Given relations $\cl{R}$, decide if $\cl{C} = \Pol(\cl{R})$ is finitely
generated. 
\pause
That is, whether $\cl{C} = \Clo(\cl{F})$ for some finite set of operations
$\cl{F}$.
\end{prob}

\pause\bigskip

The theory of Natural Dualities for algebras has a very similar notion of
relational entailment. 

\pause\medskip

We can modify the definition of $\deg(\cdot)$ to obtain a duality degree:
$\deg_{\partial}(\cdot)$.

\pause\smallskip

\begin{prob}[Finite Duality Degree]
Decide whether $\deg_{\partial}(\A)<\infty$ for finite $\A$.
\end{prob}

\pause

Duality entailment implies usual entailment, so we already have that
$\AAM$ is not finitely duality related when $\M$ does not halt.

\pause

\begin{prob}
If $\M$ halts, is $\deg_{\partial}(\AAM)<\infty$? \slidefinish
\end{prob}
\end{frame}
%----------------------------------------------------------------------------}}}1
\begin{frame}  % thanks! {{{1
\begin{thm}
The following are equivalent.
\begin{itemize}
  \item $\M$ halts,
  \item $\deg(\AAM) < \infty$ (i.e.\ $\AAM$ is finitely related),
  \item $\M$ halts with capacity $\deg(\AAM)$.
\end{itemize}
\end{thm}

\bigskip

\begin{center}
``Finite Degree Clones are Undecidable''
\end{center}

\pause\vspace{4em}

\centering Thank you for your attention.
\end{frame}
%----------------------------------------------------------------------------}}}1
\end{document}
