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

% beamer settings
\usetheme{Madrid}
\setbeamercolor{alerted text}{fg=blue}
\beamertemplatenavigationsymbolsempty
\let\emph\textbf
\setitemize{label=\usebeamerfont*{itemize item}
  \usebeamercolor[fg]{itemize item}
  \usebeamertemplate{itemize item}
}
\setbeamertemplate{items}[circle]
\setbeamertemplate{section in toc}[circle]
\definecolor{beamerblue}{RGB}{51,51,179}
\newcommand{\slidefinish}{\hfill$\cdot$}
\tikzset{alert/.style = {color=blue, thick}}

% 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}}

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

% misc
\renewcommand{\epsilon}{\varepsilon}
\renewcommand{\phi}{\varphi}
\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 conf}

% 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}

\tikzset{state/.style = {draw, rounded corners, rectangle}}
\newcommand{\inlinestate}[1]{
  \begin{tikzpicture}[font=\scriptsize, baseline=(s.base)] 
    \node[state] (s) {#1}; 
  \end{tikzpicture}
}
%----------------------------------------------------------------------------}}}1

\begin{document}
% title page {{{1
\title{Finite Degree Clones Are Undecidable}
\author{Matthew Moore}
\institute[KU]{The University of Kansas \\
  \tiny Department of Electrical Engineering and Computer Science}
\date[2019-05-20]{May 20, 2019}

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

% TOC {{{1
\begin{frame} \frametitle{\inserttitle}
\tableofcontents
\end{frame}  % }}}1

\section{Clones and The Finite Degree Problem}
% TOC {{{1
\begin{frame} \frametitle{\inserttitle}
\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
\begin{frame}  % finite degree 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:}] finite algebra 
    $\A = \left< A; f_1,\dots,f_n \right>$ generating clone $\cl{C}$
  \item[\texttt{Output:}] whether $\deg(\cl{C}) < \infty$
\end{itemize}

\pause\bigskip

(seems to originate in the 70s with the study of lattices of clones over
domains of more than $2$ elements)
\slidefinish
\end{frame}  % }}}1
\begin{frame}  % thm statement, history {{{1
\emph{The Finite Degree Problem}
\begin{itemize}[leftmargin=6em]
  \item[\texttt{Input:}] finite algebra 
    $\A = \left< A; f_1,\dots,f_n \right>$ generating clone $\cl{C}$
  \item[\texttt{Output:}] whether $\deg(\cl{C}) < \infty$
\end{itemize}

\pause\smallskip

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

\pause\smallskip

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

Similar approaches have proved the following are undecidable:
\begin{itemize} \small
  \pause\item finite residual bound (McKenzie)
  \pause\item finite axiomatizability/Tarski's problem (McKenzie)
  \pause\item certain omitting types (McKenzie, Wood)
  \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{\inserttitle}
\tableofcontents[currentsection]
\end{frame}  % }}}1
\begin{frame}  % Minsky machines {{{1
\vspace{0.5em}
\emph{A Minsky machine has}
\vspace{0.5em}
\begin{itemize}[itemsep=1em]
  \pause\item registers $A$ and $B$ that have integer values $\geq 0$,
  \pause\item instructions to add $1$ to a register,

  \bigskip

    % addition pictures {{{
    \uncover<6->{ \begin{center}
    \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(A.base)]
      \path (0,0) node (start) {}
          ++(0.75,0) node[state] (A) {$A+$}
          ++(0.75,0) node (end) {};
      \draw[->] (start) edge (A)
                (A)     edge (end);
    \end{tikzpicture}
    \qquad or \qquad
    \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(B.base)]
      \path (0,0) node (start) {}
          ++(0.75,0) node[state] (B) {$B+$}
          ++(0.75,0) node (end) {};
      \draw[->] (start) edge (B)
                (B)     edge (end);
    \end{tikzpicture}
    \end{center} }   % }}}

  \pause\item instructions to test if a register is $0$ and otherwise
  subtract $1$ from it.

  \bigskip

    % subtraction pictures {{{
    \uncover<7->{ \begin{center}
    \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(A.base)]
      \path (0,0) node (start) {}
          ++(0.75,0) node[state] (A) {$A-$}
           +(0.75,-0.35) node (end1) {}
           +(0.75,0.35) node (end2) {};
      \draw[->] (start) edge (A)
                (A)     edge (end1)
                (A) edge node[auto,yshift=-0.3em,xshift=0.2em] {$0$} (end2);
    \end{tikzpicture}
    \qquad or \qquad
    \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(B.base)]
      \path (0,0) node (start) {}
          ++(0.75,0) node[state] (B) {$B-$}
           +(0.75,-0.35) node (end1) {}
           +(0.75,0.35) node (end2) {};
      \draw[->] (start) edge (B)
                (B)     edge (end1)
                (B) edge node[auto,yshift=-0.3em,xshift=0.2em] {$0$} (end2);
    \end{tikzpicture}
    \end{center} }  % }}}
\end{itemize}

\pause\vspace{1em}

We can represent a Minsky machine as a finite flow graph.

\vspace{0.25em}

% example machine {{{
\uncover<8->{ \begin{center} 
\uncover<9->{ $\M \quad = \quad$ }
\begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(end.base)]
  \path (0,0) node[inner sep=0.1em] (start) {start}
      ++(0.75,0) node[state] (Am1) {$A-$}
      ++(1,0) node[state]    (Bm2) {$B-$}
      ++(1,0) node[state]    (Ap)  {$A+$}
        (Am1)
      ++(0,-1) node[state]   (Bm1) {$B-$}
      ++(1,0) node[state]    (Am2) {$A-$}
      ++(1,0) node[state]    (Bp)  {$B+$}
      ++(0.7,0.5) node[inner sep=0.25em] (end) {end};

  \draw[->] (start) edge                       (Am1)
            (Am1)   edge node[auto] {$0$}      (Bm2)
            (Bm2)   edge node[auto] {$0$}      (Ap)
            (Ap)    edge                       (end)
            (Bm1)   edge node[auto,swap] {$0$} (Am2)
            (Am2)   edge node[auto,swap] {$0$} (Bp)
            (Bp)    edge                       (end)
            (Am1)   edge[bend right]           (Bm1)
            (Bm1)   edge[bend right]           (Am1)
            (Bm2) edge[out=270-30,in=270+30,looseness=5] (Bm2)
            (Am2) edge[out=90-30,in=90+30,looseness=5] (Am2);
\end{tikzpicture} \end{center} }   % }}}
\uncover<9>{ \slidefinish }
\end{frame}  % }}}1
\begin{frame}  % Minsky machine example {{{1
\begin{columns}
  \begin{column}{0.51\textwidth}
  % example machine {{{
  \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(end.base)]
    \path (0,0) node[inner sep=0.1em] (start) {start}
        ++(0.75,0) node[state] (Am1) {\phantom{1:}$A-$}
        ++(1,0) node[state]    (Bm2) {\phantom{2:}$B-$}
        ++(1,0) node[state]    (Ap)  {\phantom{3:}$A+$}
          (Am1)
        ++(0,-1) node[state]   (Bm1) {\phantom{4:}$B-$}
        ++(1,0) node[state]    (Am2) {\phantom{5:}$A-$}
        ++(1,0) node[state]    (Bp)  {\phantom{6:}$B+$}
        ++(0.7,0.5) node[inner sep=0.25em] (end) {\phantom{0:}end};

    \draw[->] (start) edge                       (Am1)
              (Am1)   edge node[auto] {$0$}      (Bm2)
              (Bm2)   edge node[auto] {$0$}      (Ap)
              (Ap)    edge                       (end)
              (Bm1)   edge node[auto,swap] {$0$} (Am2)
              (Am2)   edge node[auto,swap] {$0$} (Bp)
              (Bp)    edge                       (end)
              (Am1)   edge[bend right]           (Bm1)
              (Bm1)   edge[bend right]           (Am1)
              (Bm2) edge[out=270-30,in=270+30,looseness=5] (Bm2)
              (Am2) edge[out=90-30,in=90+30,looseness=5] (Am2);

    \uncover<3|handout:0>{ \node[alert] at (start) {start}; }

    \uncover<4-5,8-9,12-13|handout:0>{ \node[state, alert] at (Am1) {\phantom{1:}$A-$}; }
    \uncover<5,9|handout:0>{ \draw[->, alert] (Am1) edge[bend right] (Bm1); }
    \uncover<13|handout:0>{ \draw[->, alert] (Am1) edge node[auto] {$0$} (Bm2); }

    \uncover<6-7,10-11|handout:0>{ \node[state, alert] at (Bm1) {\phantom{4:}$B-$}; }
    \uncover<7,11|handout:0>{ \draw[->, alert] (Bm1) edge[bend right] (Am1); }

    \uncover<14-17|handout:0>{ \node[state, alert] at (Bm2) {\phantom{2:}$B-$}; }
    \uncover<15|handout:0>{ \draw[->, alert] (Bm2) edge[out=270-30,in=270+30,looseness=5] (Bm2); }
    \uncover<17|handout:0>{ \draw[->, alert] (Bm2) edge node[auto] {$0$} (Ap); }

    \uncover<18-19|handout:0>{ \node[state, alert] at (Ap) {\phantom{3:}$A+$}; }
    \uncover<19|handout:0>{ \draw[->, alert] (Ap) edge (end); }

    \uncover<20|handout:0>{ \node[alert] at (end) {\phantom{0:}end}; }


    \uncover<23->{
      \node at (Am1) {\alert<23-25|handout:0>{1}:$A-$};
      \node at (Bm2) {\alert<23-25|handout:0>{2}:$B-$};
      \node at (Ap)  {\alert<23-25|handout:0>{3}:$A+$};
      \node at (Bm1) {\alert<23-25|handout:0>{4}:$B-$};
      \node at (Am2) {\alert<23-25|handout:0>{5}:$A-$};
      \node at (Bp)  {\alert<23-25|handout:0>{6}:$B+$};
      \node at (end) {\alert<23-25|handout:0>{0}:end};
    }
  \end{tikzpicture} % }}}

  \vspace{3em}

  \uncover<21->{\emph{How to represent intermediate computations?}}

  \vspace{0.5em}

  \end{column}
  \begin{column}{0.44\textwidth} \small
    \pause
    % table {{{
    \begin{tabular}{cccc}
      \textbf{Step}   & \uncover<24->{\textbf{State}}                                                                                  & \textbf{A\phantom{$,$}}                   & \textbf{B\phantom{$)$}} \\ \midrule
      \uncover<3->{0  & \only<3-24|handout:0>{\alert<3>{start}}\only<25->{\uncover<27->{$($}\alert<25|handout:0>{1}\uncover<27->{$,$}} & 2\uncover<27->{$,$}                       & 3\uncover<27->{$)$}} \\
      \uncover<5->{1  & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{4}\uncover<27->{$,$}}                                     & \alert<5|handout:0>{1}\uncover<27->{$,$}  & 3\uncover<27->{$)$}} \\
      \uncover<7->{2  & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{1}\uncover<27->{$,$}}                                     & 1\uncover<27->{$,$}                       & \alert<7|handout:0>{2}\uncover<27->{$)$}} \\
      \uncover<9->{3  & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{4}\uncover<27->{$,$}}                                     & \alert<9|handout:0>{0}\uncover<27->{$,$}  & 2\uncover<27->{$)$}} \\
      \uncover<11->{4 & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{1}\uncover<27->{$,$}}                                     & 0\uncover<27->{$,$}                       & \alert<11|handout:0>{1}\uncover<27->{$)$}} \\
      \uncover<13->{5 & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{2}\uncover<27->{$,$}}                                     & \alert<13|handout:0>{0}\uncover<27->{$,$} & 1\uncover<27->{$)$}} \\
      \uncover<15->{6 & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{2}\uncover<27->{$,$}}                                     & 0\uncover<27->{$,$}                       & \alert<15|handout:0>{0}\uncover<27->{$)$}} \\
      \uncover<17->{7 & \uncover<25->{\uncover<27->{$($}\alert<25|handout:0>{3}\uncover<27->{$,$}}                                     & 0\uncover<27->{$,$}                       & \alert<17|handout:0>{0}\uncover<27->{$)$}} \\
      \uncover<19->{8 & \only<20-24|handout:0>{\alert<20>{end}}\only<25->{\uncover<27->{$($}\alert<25|handout:0>{0}\uncover<27->{$,$}} & \alert<19|handout:0>{1}\uncover<27->{$,$} & 0\uncover<27->{$)$}}
    \end{tabular}  % }}}
  \end{column}
\end{columns}

\begin{itemize}[itemsep=0.5em] \small
  \item<22-> Assign a \emph{state} to each node.
  \item<26-> A \emph{configuration} $(i,\alpha,\beta)$ represents each stage
    of computation.
  \item<28-> 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).
  \item<29-> On $(\alpha,\beta)$, $\M$ halts with registers $(1,0)$ if
    $\alpha\leq \beta$ and $(0,1)$ otherwise.
  \uncover<29->{\slidefinish}
\end{itemize} \vspace{-2em}
\end{frame}  % }}}1
\begin{frame}[t]  % A(M) motivation {{{1
\emph{The encoding of computation}
\begin{itemize}[itemsep=0.5em]
  \item<2-> let $\AAM$ be the algebra we intend to build
  \item<3-> \makebox[12.6em][l]{configurations $(i,\alpha,\beta)$}
    \quad $\leftrightsquigarrow$ \quad
    special elements of $\AM^n$
  \item<11-> term operations should simulate the action of $\M$
    \uncover<13->{({\scriptsize need placemarker, $\Dot$})}
  \item<12-> \makebox[12.6em][l]{computation on configurations}
    \quad $\leftrightsquigarrow$ \quad
    subalgebra generation
\end{itemize}

\small \vspace{2em}

\uncover<4-8|handout:0>{ $\ds{
  \text{Config } (i,2,1) \leftrightsquigarrow
  \only<4-6|handout:0>{ \big( \vect{i,A}, \vect{i,A}, \vect{i,B} \big) \in \AM^3 }
  \only<7->{
    \left\{ \begin{gathered}
      \big( \vect{i,A}, \vect{i,A}, \vect{i,B} \big),
      \big( \vect{i,A}, \vect{i,B}, \vect{i,A} \big), \\
      \big( \vect{i,B}, \vect{i,A}, \vect{i,A} \big)
    \end{gathered} \right\} \subseteq \AM^3 
  }
}$ }

\vspace{2em}

\uncover<5->{ $\AAM$ has universe... \quad
$\ds{
  A(\M) = \Big\{ \vect{i,c} \mid i \text{ a state of } \M,\ 
    c\in \{A,B\only<10->{,0}\only<14->{,\Dot}\only<17->{,\Er}\} \Big\} 
}$ \hfill {\scriptsize \only<5-9|handout:0>{(\alert{v1})}\only<10-13|handout:0>{(\alert{v2})}\only<14-16|handout:0>{(\alert{v3})}}}

\vspace{2em}

\uncover<6->{ 
  \only<6-15|handout:0>{Config $(k,\alpha,\beta)$ \\[0.75em]}
  \only<16->{Given configuration $(k,\alpha,\beta)$ and $n\in \NN$ define a
    subset of $\AAM^n$, \\[0.75em]}
$\ds{
  \only<16->{\Config(k,\alpha,\beta) =}
  \only<6-15|handout:0>{\qquad \leftrightsquigarrow}
  \uncover<8->{ \bigcup_{p\in P_n} \Big\{ p } { \scriptsize
    \Big( \underbrace{ \vect{k,A}, \dots, \vect{k,A} }_{\alpha},
          \underbrace{ \vect{k,B}, \dots, \vect{k,B} }_{\beta} 
    \only<9->{, \underbrace{ \vect{k,0}, \dots, \vect{k,0} }_{n-\alpha-\beta\only<15->{-1}}}
    \only<15->{, \vect{k,\Dot}}
    \Big)
  }
  \uncover<8->{ \Big\} }
}$ \hfill {\scriptsize \only<6-7|handout:0>{(\alert{v1})}\only<8|handout:0>{(\alert{v2})}\only<9-14|handout:0>{(\alert{v3})}\only<15|handout:0>{(\alert{v4})}}}
\uncover<17>{ \slidefinish }
\end{frame}  % }}}1
\begin{frame}  % M, M' motivation {{{1
\emph{The encoding of computation}
\begin{itemize}[itemsep=0.5em]
  \item term operations should simulate the action of $\M$
  \item \makebox[12.6em][l]{computation on configurations}
    \quad $\leftrightsquigarrow$ \quad
    subalgebra generation
\end{itemize}

\pause \vspace{-0.25em}

\begin{columns}
  \begin{column}{0.50\textwidth}
    % example machine {{{
    \begin{center} \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(end.base)]
      \path (0,0) node[inner sep=0.1em] (start) {start}
          ++(0.75,0) node[state] (Am1) {1:$A-$}
          ++(1,0) node[state]    (Bm2) {2:$B-$}
          ++(1,0) node[state]    (Ap)  {3:$A+$}
            (Am1)
          ++(0,-1) node[state]   (Bm1) {4:$B-$}
          ++(1,0) node[state]    (Am2) {5:$A-$}
          ++(1,0) node[state]    (Bp)  {6:$B+$}
          ++(0.7,0.5) node[inner sep=0.25em] (end) {0:end};

      \draw[->] (start) edge                       (Am1)
                (Am1)   edge node[auto] {$0$}      (Bm2)
                (Bm2)   edge node[auto] {$0$}      (Ap)
                (Ap)    edge                       (end)
                (Bm1)   edge node[auto,swap] {$0$} (Am2)
                (Am2)   edge node[auto,swap] {$0$} (Bp)
                (Bp)    edge                       (end)
                (Am1)   edge[bend right]           (Bm1)
                (Bm1)   edge[bend right]           (Am1)
                (Bm2) edge[out=270-30,in=270+30,looseness=5] (Bm2)
                (Am2) edge[out=90-30,in=90+30,looseness=5] (Am2);
    \end{tikzpicture} \end{center} % }}}
  \end{column}
  \pause
  \begin{column}{0.45\textwidth}
    \emph{Term operations}
    \begin{itemize}[itemsep=0.5em]
      \pause\item $M(x,y)$ for \inlinestate{$R+$} or \inlinestate{$R-$}
      \pause\item $M'(x)$ for \inlinestate{$R-$}$\stackrel{0}{\longrightarrow}$
    \end{itemize}
  \end{column}
\end{columns}

\pause \vspace{0.5em}

\emph{Design considerations}
\vspace{-1.25em} \begin{columns}[t]
  \begin{column}{0.475\textwidth} \begin{itemize}
    \item<7-> $M(r,s) = t$ \quad \uncover<8->{if and only if...}
    \begin{itemize}[label=\textcolor{beamerblue}{$\circ$}, itemsep=0.25em]
      \item<9-> $r,s\in \Config(i,\alpha,\beta)$
      \item<10-> $r\neq s$
      \item<11-> $t\in \Config(\M(i,\alpha,\beta))$ \\[0.25em]
        \uncover<12->{ via some \inlinestate{$R+$} or \inlinestate{$R-$} }
    \end{itemize}
\end{itemize} \end{column} \uncover<13->{ \textcolor{beamerblue}{\hfill\vrule\hfill\phantom{\vrule}} }
  \begin{column}{0.475\textwidth} \begin{itemize}
    \item<13-> $M'(r) = t$ \quad if and only if...
    \begin{itemize}[label=\textcolor{beamerblue}{$\circ$}, itemsep=0.25em]
      \item<14-> $r\in \Config(i,\alpha,\beta)$
      \item<15-> $t\in \Config(\M(i,\alpha,\beta))$ \\[0.25em]
        \uncover<16->{ via some \inlinestate{$R-$}$\stackrel{0}{\longrightarrow}$ }
    \end{itemize}
  \end{itemize} \end{column}
\end{columns}

\vspace{0.5em}

\begin{itemize}[leftmargin=2.175em]
  \item<17-> otherwise introduce $\Er$ into the output $t$
  \uncover<17>{\slidefinish}
\end{itemize}
\end{frame}  % }}}1
\begin{frame}  % M, M' definition {{{1
\emph{Can we actually define $M$ and $M'$ with these features?}

\pause

\begin{scriptsize} \begin{align*}
  &M(x,y) = \begin{cases}
    \vect{j,R}    & \text{if } x = \vect{i,\Dot},\ y = \vect{i,0},\ 
      \inlinestate{$i:R+$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{j,0}    & \text{if } x = \vect{i,\Dot},\ y = \vect{i,R},\ 
      \inlinestate{$i:R-$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{j,\Dot} & \text{if } x = \vect{i,0},\ y = \vect{i,\Dot},\ 
      \inlinestate{$i:R+$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{j,\Dot} & \text{if } x = \vect{i,R},\ y = \vect{i,\Dot},\ 
      \inlinestate{$i:R-$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{j,c}    & \text{if } x = y = \vect{i,c},\ 
      \inlinestate{$i:R+$}\longrightarrow\inlinestate{$j:*$} \quad\text{or}\quad
      \inlinestate{$i:R-$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{j,\Er}  & \text{else if } x = \vect{i,c},\ y = \vect{i,d},\ 
      \inlinestate{$i:R+$}\longrightarrow\inlinestate{$j:*$} \quad\text{or}\quad
      \inlinestate{$i:R-$}\longrightarrow\inlinestate{$j:*$}, \\[0.5em]
    \vect{i,\Er} & \text{otherwise, where } y = \vect{i,c}.
  \end{cases} \\[1em]
  &M'(x) = \begin{cases}
    \vect{k,c}   & \text{if } x = \vect{i,c},\ 
      \inlinestate{$i:R+$}\stackrel{0}{\longrightarrow}\inlinestate{$k:*$},\ c\neq R, \\[0.5em]
    \vect{k,\Er} & \text{else if } x = \vect{i,R},\ 
      \inlinestate{$i:R+$}\stackrel{0}{\longrightarrow}\inlinestate{$k:*$}, \\[0.5em]
    \vect{i,\Er}        & \text{otherwise, where } x = \vect{i, c}.
  \end{cases}
\end{align*} \end{scriptsize}

\pause

Let's see an example computation...
\slidefinish
\end{frame}  % }}}1
\begin{frame}[t]  % A(M) calculation {{{1
\small
\begin{columns}
  \begin{column}{0.50\textwidth}
    \vspace{-1em}
    % example machine {{{
    \begin{tikzpicture}[font=\scriptsize, scale=1.5, baseline=(end.base)]
      \path (0,0) node[inner sep=0.1em] (start) {start}
          ++(0.75,0) node[state] (Am1) {1:$A-$}
          ++(1,0) node[state]    (Bm2) {2:$B-$}
          ++(1,0) node[state]    (Ap)  {3:$A+$}
            (Am1)
          ++(0,-1) node[state]   (Bm1) {4:$B-$}
          ++(1,0) node[state]    (Am2) {5:$A-$}
          ++(1,0) node[state]    (Bp)  {6:$B+$}
          ++(0.7,0.5) node[inner sep=0.25em] (end) {0:end};

      \draw[->] (start) edge                       (Am1)
                (Am1)   edge node[auto] {$0$}      (Bm2)
                (Bm2)   edge node[auto] {$0$}      (Ap)
                (Ap)    edge                       (end)
                (Bm1)   edge node[auto,swap] {$0$} (Am2)
                (Am2)   edge node[auto,swap] {$0$} (Bp)
                (Bp)    edge                       (end)
                (Am1)   edge[bend right]           (Bm1)
                (Bm1)   edge[bend right]           (Am1)
                (Bm2)   edge[out=270-30,in=270+30,looseness=5] (Bm2)
                (Am2)   edge[out=90-30,in=90+30,looseness=5] (Am2);

      \only<5-9,16-21|handout:0>{
        \node[state,alert] at (Am1) {1:$A-$};
        \draw[->,alert] (Am1) edge[bend right] (Bm1);
      }
      \only<10-15|handout:0>{
        \node[state,alert] at (Bm1) {4:$B-$};
        \draw[->,alert] (Bm1) edge[bend right] (Am1);
      }
      \only<22-26|handout:0>{
        \node[state,alert] at (Bm1) {4:$B-$};
        \draw[->,alert] (Bm1) edge node[auto,swap] {$0$} (Am2);
      }
      \only<27-31|handout:0>{
        \node[state,alert] at (Am2) {5:$A-$};
        \draw[->,alert] (Am2) edge node[auto,swap] {$0$} (Bp);
      }
      \only<32-36|handout:0>{
        \node[state,alert] at (Bp) {6:$B+$};
        \draw[->,alert] (Bp) edge (end);
      }
      \only<37-|handout:0>{ \node[state,alert] at (end) {0:end}; }
    \end{tikzpicture} % }}}
  \end{column}
  \begin{column}{0.45\textwidth} \scriptsize
    % table {{{
    \pause 
    \centering \begin{tabular}{cccc}
      \textbf{Step}                            & \textbf{State}             & \textbf{A}                 & \textbf{B} \\ \midrule
      \uncover<3->{\alert<3-9|handout:0>{0}    & \alert<3-9|handout:0>{1}   & \alert<3-9|handout:0>{2}   & \alert<3-9|handout:0>{1}} \\
      \uncover<8->{\alert<10-15|handout:0>{1}  & \alert<10-15|handout:0>{4} & \alert<10-15|handout:0>{1} & \alert<10-15|handout:0>{1}} \\
      \uncover<14->{\alert<16-21|handout:0>{2} & \alert<16-21|handout:0>{1} & \alert<16-21|handout:0>{1} & \alert<16-21|handout:0>{0}} \\
      \uncover<20->{\alert<22-26|handout:0>{3} & \alert<22-26|handout:0>{4} & \alert<22-26|handout:0>{0} & \alert<22-26|handout:0>{0}} \\
      \uncover<25->{\alert<27-31|handout:0>{4} & \alert<27-31|handout:0>{5} & \alert<27-31|handout:0>{0} & \alert<27-31|handout:0>{0}} \\
      \uncover<30->{\alert<32-36|handout:0>{5} & \alert<32-36|handout:0>{6} & \alert<32-36|handout:0>{0} & \alert<32-36|handout:0>{0}} \\
      \uncover<35->{\alert<37-|handout:0>{6}   & \alert<37-|handout:0>{0}   & \alert<37-|handout:0>{0}   & \alert<37-|handout:0>{1}} \\
    \end{tabular} % }}}
  \end{column}
\end{columns}

\vspace{-0.75em}

% M, M' calculation {{{
\begin{columns}
  \begin{column}{0.45\textwidth} \begin{align*}
    \uncover<4->{\emph{1: }} & \uncover<6->{M\left(} \mat{
      \uncover<4->{\vect{1,\Dot}} & \hspace{-1.1em} \uncover<7->{, \vect{1,A}} \\
      \uncover<4->{\vect{1,A}}    & \hspace{-1.1em} \uncover<7->{, \vect{1,\Dot}} \\
      \uncover<4->{\vect{1,A}}    & \hspace{-1.1em} \uncover<7->{, \vect{1,A}} \\
      \uncover<4->{\vect{1,B}}    & \hspace{-1.1em} \uncover<7->{, \vect{1,B}}
    } \uncover<6->{\right)} \uncover<9->{ = \pmat{
      \vect{4,0} \\
      \vect{4,\Dot} \\
      \vect{4,A} \\
      \vect{4,B}
    }} \\[0.5em]
    \uncover<11->{\emph{2: }} & \uncover<12->{M\left(} \mat{
        \uncover<11->{\vect{4,0}}    & \hspace{-1em} \uncover<13->{, \vect{4,0}} \\
        \uncover<11->{\vect{4,\Dot}} & \hspace{-1em} \uncover<13->{, \vect{4,B}} \\
        \uncover<11->{\vect{4,A}}    & \hspace{-1em} \uncover<13->{, \vect{4,A}} \\
        \uncover<11->{\vect{4,B}}    & \hspace{-1em} \uncover<13->{, \vect{4,\Dot}}
    } \uncover<12->{\right)} \uncover<15->{= \pmat{
      \vect{1,0} \\
      \vect{1,0} \\
      \vect{1,A} \\
      \vect{1,\Dot}
    }} \\[0.5em]
    \uncover<17->{\emph{3: }} & \uncover<18->{M\left(} \mat{
        \uncover<17->{\vect{1,0}}    & \hspace{-1em} \uncover<19->{, \vect{1,0}} \\
        \uncover<17->{\vect{1,0}}    & \hspace{-1em} \uncover<19->{, \vect{1,0}} \\
        \uncover<17->{\vect{1,A}}    & \hspace{-1em} \uncover<19->{, \vect{1,\Dot}} \\
        \uncover<17->{\vect{1,\Dot}} & \hspace{-1em} \uncover<19->{, \vect{1,A}}
    } \uncover<18->{\right)} \uncover<21->{= \pmat{
      \vect{4,0} \\
      \vect{4,0} \\
      \vect{4,\Dot} \\
      \vect{4,0}
    }}
  \end{align*} \end{column}
  \begin{column}{0.45\textwidth} \begin{align*}
    \uncover<23->{\emph{4: }} & \uncover<24->{M'\left(} \uncover<23->{\mat{
      \vect{4,0} \\
      \vect{4,0} \\
      \vect{4,\Dot} \\
      \vect{4,0}
    }} \uncover<24->{\right)} \uncover<26->{= \pmat{
      \vect{5,0} \\
      \vect{5,0} \\
      \vect{5,\Dot} \\
      \vect{5,0}
    }} \\[0.5em]
    \uncover<28->{\emph{5: }} & \uncover<29->{M'\left(} \uncover<28->{\mat{
      \vect{5,0} \\
      \vect{5,0} \\
      \vect{5,\Dot} \\
      \vect{5,0}
    }} \uncover<29->{\right)} \uncover<31->{= \pmat{
      \vect{6,0} \\
      \vect{6,0} \\
      \vect{6,\Dot} \\
      \vect{6,0}
    }} \\[0.5em]
    \uncover<33->{\emph{6: }} & \uncover<34->{M\left(} \mat{
        \uncover<33->{\vect{6,0}}    & \hspace{-1em} \uncover<35->{, \vect{6,0}} \\
        \uncover<33->{\vect{6,0}}    & \hspace{-1em} \uncover<35->{, \vect{6,\Dot}} \\
        \uncover<33->{\vect{6,\Dot}}    & \hspace{-1em} \uncover<35->{, \vect{6,0}} \\
        \uncover<33->{\vect{6,0}} & \hspace{-1em} \uncover<35->{, \vect{6,0}}
    } \uncover<34->{\right)} \uncover<37->{= \pmat{
      \vect{0,0} \\
      \vect{0,\Dot} \\
      \vect{0,B} \\
      \vect{0,0}
    }} 
    \uncover<37>{ \text{\slidefinish} }
  \end{align*} \end{column}
\end{columns} % }}}
\end{frame}  % }}}1
\begin{frame}  % computational relations {{{1
\emph{Takeaways} \uncover<2->{ \hspace{1em} on a relation $\RR\leq \AAM^n$ ... }
\begin{itemize}
  \uncover<3->{ \item certain elements of $R$ encode configurations of $\M$, }
  \uncover<5->{ \item $M$ and $M'$ encode the action of $\M$ in the presence
    of these elements. }
\end{itemize}

\vspace{-1.25em}

\uncover<4->{ \begin{small} \[
  \Config(k,\alpha,\beta)
  = \bigcup_{p\in P_n} {\scriptsize \Big\{ p \Big(
      \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},
      \vect{k,\Dot}
    \Big) \Big\} }
\] \end{small} }

\vspace{-0.5em}

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

\bigskip


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

\medskip

\uncover<11->{ The \emph{capacity} of a computation $\M^k(i,\alpha,\beta) =
(j,\alpha',\beta')$ is the max sum of the registers. }

\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
We consider the halting problem on \emph{0 register input}: config $=(1,0,0)$.

\pause \medskip

Let $\SS_m = \Sg_{\AAM^m}\big( \Config(1,0,0) \big)$.

\pause \medskip

\begin{thm}[The Coding Theorem]
\begin{itemize}
  \pause\item If $\M^n(1,0,0) = (k,\alpha,\beta)$ has capacity $< m$
  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$ then $\M^n(1,0,0) = (k,\alpha,\beta)$ for some
  $n$ and has capacity $< m$.
\end{itemize}
\end{thm}

\pause \medskip

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

  \pause\item $\SS_m$ is halting (i.e.\ contains $\Config(0,\alpha,\beta)$),

  \pause\item every computational $\RR\leq \AAM^\ell$ with capacity $\geq m$
  is halting.
  \slidefinish
\end{itemize}
\end{cor}
\end{frame}  % }}}1
\begin{frame}  % general framework {{{1
\begin{thm}[The Coding Theorem]
\begin{itemize}
  \item If $\M^n(1,0,0) = (k,\alpha,\beta)$ has capacity $< m$ then
  $\Config(k,\alpha,\beta)\subseteq S_m$.

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

\pause\smallskip

\emph{Framework for proving the hardness of algebraic properties}
\smallskip
\begin{itemize}
  \pause\item Start out with $\AAM = \left< \AM \; ; \; M, M' \right>$.

  \medskip

  \pause\item Add operations so that the property is recognizable in
    $\Rel(\AAM)$ \\[0.25em]
  \pause $\big($\hspace{0.1em} ideally in the $(\SS_m)_{m\in \NN}$
    \hspace{0.1em}$\big)$.

  \medskip

  \pause\item Use a computer to verify necessary computations.

  \medskip

  \pause\item Use software development techniques: \\[0.1em]
    \pause write unit tests, 
    \pause rapidly iterate the operation definitions.
\end{itemize}

\pause\smallskip

This allows us to give a more unified construction for the previously
mentioned undecidability results in Universal Algebra.
\slidefinish
\end{frame}  % }}}1

\section{Non-halting Implies Infinite Degree}
% TOC {{{1
\begin{frame} \frametitle{\inserttitle}
\tableofcontents[currentsection]
\end{frame}  % }}}1
\begin{frame}  % approach {{{1
\emph{Observe} \pause
\begin{align*}
  \uncover<+->{ \deg(\cl{C}) = \infty } 
    & \uncover<+->{ \quad\text{if and only if}\quad \forall n\ 
        \Rel_n(\cl{C}) \not\Entails \Rel(\cl{C}) } \\
    & \uncover<+->{ \quad\text{if and only if}\quad \forall n\ \exists \RR\
      \Rel_n(\cl{C}) \not\Entails \RR }
\end{align*}

\bigskip

\uncover<+->{ \emph{Idea:} to show that $\deg(\AAM) = \infty$ when $\M$ does
not halt, we show the last equivalence holds for $\cl{C} = \Clo(\AAM)$. }

\bigskip

\uncover<+->{ \emph{Two operations involved} }
\begin{itemize}
  \smallskip

  \item<+-> semilattice operation \hspace{1em} $\wedge$ \\
    \uncover<+->{ locally flat: $a\wedge b \neq \vect{*,\Er}$ iff $a = b$ }

  \medskip

  \item<+-> ``initialization'' operation \hspace{1em} $I(x,y)$ \\
    \uncover<+->{ returns any configuration to $\Config(1,0,0)$ }
\end{itemize}

\bigskip

\uncover<+->{ At this point 
  $\AAM = \left< \AM \; ; \; M, M', \wedge, I \right>$.
  \slidefinish }
\end{frame}  % }}}1
\begin{frame}  % Zadori theorem {{{1
$\Rel_n(\cl{C}) \Entails \RR$ \quad if and only if \quad \pause $\RR$ can be built from
$\Rel_n(\cl{C})$ using
\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{\inserttitle}
\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 by 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 We add operations to handle entailment in each of the
  different cases: \\ 
  $N_{\Dot}(w,x,y,z)$, $P(u,v,x,y)$, $H(x,y)$, $N_0(x,y,z)$, $S(x,y,z)$.

  \pause\item $\AAM = \big< \AM\;;\; M, M', \wedge, I, N_\Dot, P, H, N_0, S \big>$ 
  \pause\hspace{1em} (final version)
  \slidefinish
\end{itemize}
\end{frame}  % }}}1
\begin{frame}  % non-computational or halting {{{1
\vspace{-1em} \[
  \AAM = \big< \AM\;;\; M, M', \wedge, \alert<9-|handout:0>{I}, \alert<4-6|handout:0>{N_\Dot}, \alert<5-6|handout:0>{P}, \alert<9-|handout:0>{H}, \alert<9-|handout:0>{N_0}, S \big>
\]

\pause

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

  \item<4-> 2 $\Dot$'s: operation \alert<4-6|handout:0>{$N_\Dot$} handles
    entailment.

  \item<5-> Non-constant state: operation \alert<5-6|handout:0>{$P$} handles
    entailment.
\end{itemize}

\uncover<6->{ \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

\uncover<7->{ \emph{Case $\RR$ is halting} }
\begin{itemize}
  \item<8-> $R$ contains an element of $\Config(0,0,0)$.
  \item<9-> Any element of $\Config(0,0,0)$ can be used with operations
    \alert<9-|handout:0>{$I$}, \alert<9-|handout:0>{$H$}, and
    \alert<9-|handout:0>{$N_0$} to prove entailment.
\end{itemize}

\uncover<10->{ \begin{thmsmall} \small
If $3\leq m$ and $\RR\leq \AAM^m$ is halting then $\Rel_{m-1}(\AAM) \Entails
\RR$.
\uncover<10>{ \slidefinish }
\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 \hspace{1em} (both subsets of $[n]$)
\smallskip
\begin{itemize}[itemsep=0.75em]
  \pause\item $\D(\RR) = $ ``coordinates $i$ such that $\exists 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}[label=\textcolor{beamerblue}{$\circ$}, 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$}
\smallskip
\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-1}(\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 and Open Problems}
% TOC {{{1
\begin{frame} \frametitle{\inserttitle}
\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 at least $\deg(\AAM) - 16$.
\end{itemize}
\end{thm}

\pause\bigskip

\emph{Interesting observations}
\begin{itemize}[itemsep=0.5em]
  \pause\item There are infinitely many $\M$ with halting status
  independent of ZFC.

  \pause\item Thus, there are infinitely many $\M$ such that $\deg(\AAM) <
  \infty$ is independent of ZFC.

  \pause\item There are finite algebras $\A$ that whose finite-relatedness
  is independent of ZFC.

  \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]
  \pause is not computable. 
  \slidefinish
\end{itemize}
\end{frame}  % }}}1
\begin{frame} \frametitle{Finite Generation Problems} % {{{1
\begin{prob}
Given relations $\cl{R}$, decide if $\cl{C} = \Pol(\cl{R})$ is finitely
generated. \\
\pause
That is, decide whether $\cl{C} = \Clo(\cl{F})$ for some finite set of
operations $\cl{F}$.
\end{prob}

\pause\vfill

\begin{prob}
Given relations $\cl{R}$ and operations $\cl{F}$, decide whether
$\Pol(\cl{R}) = \Clo(\cl{F})$. \slidefinish
\end{prob}
\end{frame}  % }}}1
\begin{frame} \frametitle{Natural Duality Problems}  % {{{1
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\smallskip

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

\pause\smallskip

\begin{prob}
If $\M$ halts, is $\deg_{\partial}(\AAM)<\infty$? 
\end{prob}

\pause\vspace{2em}

\begin{prob}
Given finite $\m{A}$, decide whether $\m{A}$ admits a duality.
\slidefinish
\end{prob}
\end{frame}  % }}}1
\begin{frame} \frametitle{\inserttitle} % 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 at least $\deg(\AAM) - 16$.
\end{itemize}
\end{thm}

\pause\vspace{4em}

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

To Do:
- merge header back into template
- fewer transitions!
- picture for semilattice
