\documentclass{beamer}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{setspace}
\usepackage{graphicx}
%\usepackage{tikz}
%\usetikzlibrary{matrix,arrows,backgrounds,shapes.misc,shapes.geometric,fit}
\usepackage{etex}
\usepackage{amsthm}
\usepackage{color}
\usepackage{wasysym}
\usepackage[all]{xy}
\usepackage{textpos}
\usepackage{ytableau}
\usepackage{tikz}
%\usetikzlibrary{calc,through,backgrounds}
%\CompileMatrices

\definecolor{grau}{rgb}{.5 , .5 , .5}
\definecolor{dunkelgrau}{rgb}{.35 , .35 , .35}
\definecolor{schwarz}{rgb}{0 , 0 , 0}
\definecolor{violet}{RGB}{143,0,255}
\definecolor{forestgreen}{RGB}{34, 100, 34}

\newcommand{\red}{\color{red}}
\newcommand{\grey}{\color{grau}}
\newcommand{\green}{\color{forestgreen}}
\newcommand{\violet}{\color{violet}}
\newcommand{\blue}{\color{blue}}
\newcommand{\white}{\color{white}}

\newcommand{\bIf}{\textbf{If} }
\newcommand{\bif}{\textbf{if} }
\newcommand{\bthen}{\textbf{then} }

\newcommand{\id}{\operatorname{id}}
\newcommand{\rev}{\operatorname{rev}}
\newcommand{\conncomp}{\operatorname{conncomp}}
\newcommand{\conn}{\operatorname{conn}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\KK}{\mathbb{K}}
\newcommand{\lf}[2]{{#1}^{\underline{#2}}}
\newcommand{\powset}[2][]{\ifthenelse{\equal{#2}{}}{\mathcal{P}\left(#1\right)}{\mathcal{P}_{#1}\left(#2\right)}}
\newcommand{\set}[1]{\left\{ #1 \right\}}
\newcommand{\abs}[1]{\left| #1 \right|}
\newcommand{\tup}[1]{\left( #1 \right)}
\newcommand{\ive}[1]{\left[ #1 \right]}
\newcommand{\verts}[1]{\operatorname{V}\left( #1 \right)}
\newcommand{\edges}[1]{\operatorname{E}\left( #1 \right)}
\newcommand{\arcs}[1]{\operatorname{A}\left( #1 \right)}
\newcommand{\underbrack}[2]{\underbrace{#1}_{\substack{#2}}}
\newcommand{\are}{\ar@{-}}
\newcommand{\arebi}[1][]{\ar@{<-}@/_/[#1] \ar@/^/[#1]}
\newcommand{\arti}{\ar@{~>}}
\newcommand{\OO}{\operatorname {O}}
\newcommand{\Nm}{\operatorname {N}}
\newcommand{\Par}{\operatorname{Par}}
\newcommand{\Comp}{\operatorname{Comp}}
\newcommand{\Pfin}{\mathcal{P}_{\operatorname{fin}}}
\newcommand{\Mat}{\operatorname{M}}
\newcommand{\bk}{\mathbf{k}}
\newcommand{\Nplus}{\mathbb{N}_{+}}
\newcommand\arxiv[1]{{\red \href{http://www.arxiv.org/abs/#1}{\texttt{arXiv:#1}}}}
\newcommand\oeis[1]{{\red \url{https://oeis.org/#1}}}
\newcommand{\Orb}{{\mathcal O}}
\newcommand{\GL}{\operatorname {GL}}
\newcommand{\SL}{\operatorname {SL}}
\newcommand{\Or}{\operatorname {O}}
\newcommand{\im}{\operatorname {Im}}
\newcommand{\Iso}{\operatorname {Iso}}
\newcommand{\Adm}{\operatorname{Adm}}
\newcommand{\calS}{\mathcal{S}}
\newcommand{\Supp}{\operatorname{Supp}}
\newcommand{\zero}{\mathbf{0}}
\newcommand{\xx}{\mathbf{x}}
\newcommand{\ord}{\operatorname*{ord}}
\newcommand{\whitenothing}{{\white \ }}
\newcommand{\bbK}{{\mathbb{K}}}
\newcommand{\move}{\longrightarrow}
\newcommand{\moves}{\overset{*}{\longrightarrow}}
\newcommand{\movestr}{\overset{!}{\longrightarrow}}
\newcommand{\movestrs}{\overset{*!}{\longrightarrow}}
%\newcommand{\Trop}{\operatorname*{Trop}}
%\newcommand{\TropZ}{{\operatorname*{Trop}\mathbb{Z}}}
\newcommand{\rato}{\dashrightarrow}
\newcommand{\lcm}{\operatorname*{lcm}}
\newcommand\staircasepath[4]{
\fill[cyan!25]  (#1) rectangle +(#2,#3);
\fill[fill=lime]
(#1)
\foreach \dir in {#4}{
\ifnum\dir=1
-- ++(1,0)
\else
-- ++(0,1)
\fi
} |- (#1);
\draw[help lines] (#1) grid +(#2,#3);
\draw[dashed] (#1) -- +(#2,#2);
\coordinate (prev) at (#1);
\foreach \dir in {#4}{
\ifnum\dir=1
\coordinate (dep) at (1,0);
\else
\coordinate (dep) at (0,1);
\fi
\draw[line width=2pt,-stealth] (prev) -- ++(dep) coordinate (prev);
};
}
\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
            \node[shape=circle,draw,inner sep=2pt] (char) {#1};}}

\newcommand{\fti}[1]{\frametitle{\ \ \ \ \ #1}}
\newenvironment{iframe}[1][]{\begin{frame} \fti{[#1]} \begin{itemize}}{\end{frame}\end{itemize}}
\newcommand{\nfr}{\vspace{10cm} \end{frame} \begin{frame}}

\setbeamertemplate{itemize/enumerate body begin}{\large}
\setbeamertemplate{itemize/enumerate subbody begin}{\large}
\setbeamertemplate{itemize/enumerate subsubbody begin}{\large}

\usepackage{url}%this line and the next are related to hyperlinks
%\usepackage[colorlinks=true, pdfstartview=FitV, linkcolor=blue, citecolor=blue, urlcolor=blur]{hyperref}

\usepackage{color}

%\usetheme{Antibes}
%\usetheme{Bergen}
%\usetheme{Berkeley}
%\usetheme{Berlin}
%\usetheme{Boadilla}
%\usetheme{Copenhagen}
%\usetheme{Darmstadt}
%\usetheme{Dresden}
\usetheme{Frankfurt}
%\usetheme{Goettingen}
%\usetheme{Hannover}
%\usetheme{Ilmenau}
%\usetheme{JuanLesPins}
%\usetheme{Luebeck}
%\usetheme{Madrid}
%\usetheme{Malmoe}
%\usetheme{Marburg}
%\usetheme{Montpellier}
%\usetheme{PaloAlto}
%\usetheme{Pittsburgh}
%\usetheme{Rochester}
%\usetheme{Singapore}
%\usetheme{Szeged}
%\usetheme{Warsaw}

\usefonttheme[onlylarge]{structurebold}
\setbeamerfont*{frametitle}{size=\normalsize,series=\bfseries}
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\setbeamertemplate{itemize/enumerate body begin}{}
\setbeamertemplate{itemize/enumerate subbody begin}{\normalsize}
%\setbeamertemplate{section in head/foot shaded}[default][60]
%\setbeamertemplate{subsection in head/foot shaded}[default][60]
\beamersetuncovermixins{\opaqueness<1>{0}}{\opaqueness<2->{15}}

%\usepackage{beamerthemesplit}
\usepackage{epsfig,amsfonts,bbm,mathrsfs}
\usepackage{verbatim} 



\newcommand{\STRUT}{\vrule width 0pt depth 8pt height 0pt}
\newcommand{\ASTRUT}{\vrule width 0pt depth 0pt height 11pt}


\theoremstyle{plain}
\newtheorem{conj}[theorem]{Conjecture}


\setbeamertemplate{headline}{}
%This removes a black stripe from the top of the slides.


\author{Darij Grinberg}
\title[The diamond lemma and its applications]{The diamond lemma and its applications}

\date{3 May 2018 // 20 May 2018}

\begin{document}

\frame{\titlepage
\textbf{slides:} \\ {\red \url{http://www.cip.ifi.lmu.de/~grinberg/algebra/diamond-talk.pdf} } \\
\textbf{references:}
\begin{itemize}
\item {\red \href{https://doi.org/10.1016/0012-365X(95)00131-F}{Eriksson, \textit{Strong convergence and the polygon property of 1-player games}}}.
\item {\red \href{https://mathoverflow.net/a/289320/}{MathOverflow answer \#289320} (with list of references)}.
\item {\red \href{https://www.maths.tcd.ie/~vdots/AlgebraicOperadsAnAlgorithmicCompanion.pdf}{Bremner/Dotsenko, \textit{Algebraic Operads: An Algorithmic Companion}}}.
\end{itemize}}

\begin{frame}
\fti{1. Bubblesort}
\begin{center}
{\Huge \bf \sc 1.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf Bubblesort}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{https://arxiv.org/src/1509.03803v2/anc/groth1alt.pdf}{Galashin/Grinberg/Liu, arXiv:1509.03803v2 ancillary file}}, Section 4.2.
\end{itemize}
\end{frame}

\begin{frame}
\fti{Bubblesort, the game}

\begin{itemize}

\item Consider the following 1-player game:
      \begin{itemize}
      \item \textbf{Start} with a list $\tup{a_1, a_2, \ldots, a_n}$ of $n$ numbers.
      \item \textbf{Allowed move:} Pick any $i \in \set{1,2,\ldots,n-1}$ such that $a_i > a_{i+1}$,
            and swap $a_i$ with $a_{i+1}$.
      \end{itemize}
      \pause
      \textbf{Questions:} Will the game always terminate? \\
      And will the final result depend on the choice of moves?

\pause

\only<3-8>{
\item Example: (we underline the two entries we are about to swap)
      \only<3>{
      \[
       \tup{\underline{6,2},1} \to \phantom{\tup{2,\underline{6,1}} \to \tup{\underline{2,1},6} \to \tup{1,2,6} .}
      \]
      }%
      \only<4>{
      \[
       \tup{\underline{6,2},1} \to \tup{2,\underline{6,1}} \to \phantom{\tup{\underline{2,1},6} \to \tup{1,2,6} .}
      \]
      }%
      \only<5>{
      \[
       \tup{\underline{6,2},1} \to \tup{2,\underline{6,1}} \to \tup{\underline{2,1},6} \to \phantom{\tup{1,2,6} .}
      \]
      }%
      \only<6-11>{
      \[
       \tup{\underline{6,2},1} \to \tup{2,\underline{6,1}} \to \tup{\underline{2,1},6} \to \tup{1,2,6} .
      \]
      }%
      \pause\pause\pause\pause
      Alternatively, from the same starting position:
      \[
       \tup{6,\underline{2,1}} \to \tup{\underline{6,1},2} \to \tup{1,\underline{6,2}} \to \tup{1,2,6} .
      \]
      \pause
      Looks good so far; what about other tuples?
} \pause

\item \textbf{Yes}, it will terminate \\
      \quad since the number of inversions decreases at each move.\\
      \only<10-11>{\textbf{No}, the final result doesn't depend on the choice of moves, \\
      \quad since an $n$-tuple has only one weakly increasing permutation.}

\only<11>{
\item This is a non-deterministic version of bubblesort (the simplest sorting algorithm ever).
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Bubblesort, the game: partial order}

\begin{itemize}

\item Now what if $a_1, a_2, \ldots, a_n$ aren't numbers, but are elements of a poset instead?
      \pause

\item Example:
      \[
      \xymatrix{
       & \delta \are[dl] \are[dr] \\
       \beta \are[dr] & & \gamma \are[dl] \\
       & \alpha
      }
      \]
      Start with the list $\tup{\delta, \gamma, \beta, \alpha}$. \pause
      \begin{align*}
       \tup{\underline{\delta, \gamma}, \beta, \alpha}
       &\to \tup{\gamma, \delta, \underline{\beta, \alpha}}
       \to \tup{\gamma, \underline{\delta, \alpha}, \beta}
       \to \tup{\underline{\gamma, \alpha}, \delta, \beta} \\
       &\to \tup{\alpha, \gamma, \underline{\delta, \beta}}
       \to \tup{\alpha, \gamma, \beta, \delta} .
      \end{align*}
      We've got a linear extension of our poset, but is it still independent of the moves?

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{2. Chip-firing with a sink}
\begin{center}
{\Huge \bf \sc 2.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf Chip-firing with a sink}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{https://arxiv.org/abs/0801.3306}{Holroyd/Levine/M\'esz\'aros/Peres/Propp/Wilson, \textit{Chip-Firing and Rotor-Routing on Directed Graphs}}}.
\item {\red \href{http://people.reed.edu/~davidp/divisors_and_sandpiles/}{Corry/Perkinson, \textit{Divisors and Sandpiles}}}.
\item {\red \href{http://web.cs.elte.hu/~lovasz/morepapers/abacus.pdf}{Bj\"orner/Lov\'asz, \textit{Chip-firing games on directed graphs}}}.
\item {\red \href{http://www.cip.ifi.lmu.de/~grinberg/t/17s/hw5s.pdf}{Spring 2017 Math 5707 homework set 5}}.
\item {\red \href{http://www.cip.ifi.lmu.de/~grinberg/t/18s/4707-2018apr25-add.txt}{more links}}.
\end{itemize}
\end{frame}

\begin{frame}
\fti{Chip-firing with a sink}

\begin{itemize}

\item Start with a digraph (= directed graph).
      \only<1>{
      \[
       \xymatrix{
        \alpha \ar[r] \ar[d] & \beta \ar[d] \\
        \varepsilon \ar[ru] \ar[r] & \gamma \ar[r] & \delta \ar[lu]
       }
      \]
      } %
      \only<2>{
      \[
       \xymatrix{
        \alpha \ar[r] \ar[d] & \beta \ar[d] \\
        \varepsilon \ar[ru] \ar[r] & \gamma \ar[r] & {\blue \delta} \ar[lu]
       }
      \]
      } %
      \only<3,5>{
      \[
       \xymatrix{
        3 \ar[r] \ar[d] & 2 \ar[d] \\
        2 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      } %
      \only<6>{
      \[
       \xymatrix{
        \underline{3} \ar[r] \ar[d] & 2 \ar[d] \\
        2 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      } %
      \only<7>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & \underline{3} \ar[d] \\
        3 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      } %
      \only<8>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 2 \ar[d] \\
        3 \ar[ru] \ar[r] & \underline{2} \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      } %
      \only<9>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 2 \ar[d] \\
        3 \ar[ru] \ar[r] & \underline{1} \ar[r] & {\blue 3} \ar[lu]
       }
      \]
      } %
      \only<10>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 2 \ar[d] \\
        \underline{3} \ar[ru] \ar[r] & 0 \ar[r] & {\blue 4} \ar[lu]
       }
      \]
      } %
      \only<11>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & \underline{3} \ar[d] \\
        1 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 4} \ar[lu]
       }
      \]
      } %
      \only<12>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 2 \ar[d] \\
        1 \ar[ru] \ar[r] & \underline{2} \ar[r] & {\blue 4} \ar[lu]
       }
      \]
      } %
      \only<13>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & \underline{2} \ar[d] \\
        1 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 5} \ar[lu]
       }
      \]
      } %
      \only<14>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & \underline{1} \ar[d] \\
        1 \ar[ru] \ar[r] & 2 \ar[r] & {\blue 5} \ar[lu]
       }
      \]
      } %
      \only<15>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 0 \ar[d] \\
        1 \ar[ru] \ar[r] & \underline{3} \ar[r] & {\blue 5} \ar[lu]
       }
      \]
      }  %
      \only<16>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 0 \ar[d] \\
        1 \ar[ru] \ar[r] & \underline{2} \ar[r] & {\blue 6} \ar[lu]
       }
      \]
      }  %
      \only<17>{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 0 \ar[d] \\
        1 \ar[ru] \ar[r] & \underline{1} \ar[r] & {\blue 7} \ar[lu]
       }
      \]
      }  %
      \only<18->{
      \[
       \xymatrix{
        1 \ar[r] \ar[d] & 0 \ar[d] \\
        1 \ar[ru] \ar[r] & 0 \ar[r] & {\blue 8} \ar[lu]
       }
      \]
      }
      \only<2-4>{\\ Choose a vertex $s$ that is \textit{globally reachable} (i.e., for each vertex $v$, there is a path from $v$ to $s$).
      Call it the \textit{sink}. (Marked in {\blue blue} above.)}
      \pause\\
      \only<3-4>{A \textit{chip configuration} is a choice of nonnegative integer for each vertex.
      We consider a number $i$ at vertex $v$ to mean ``$i$ chips lying at $v$''.}
      \pause\pause

\item The \textit{chip-firing game} is played as follows:
      \begin{itemize}
      \item \textbf{Start} with a chip configuration.
      \item \textbf{Allowed move:} Choose a vertex $v \neq {\blue s}$ that has at least as many chips
            as it has outgoing arcs, \\
            and ``fire'' it (i.e., for each arc $v \overset{a}{\to} w$, send a chip from $v$ to $w$).
      \end{itemize}
      \only<6->{Example: See image above (we underline the vertex about to be fired).}
      \only<18>{Note: The {\blue sink} cannot be fired!}
      \only<19>{
      \\ \textbf{Questions:} Will the game always terminate? \\
      And will the final result depend on the choice of moves?
      }

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{3. The finite diamond lemma}
\begin{center}
{\Huge \bf \sc 3.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf The finite diamond lemma}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{https://doi.org/10.1016/0012-365X(95)00131-F}{Eriksson, \textit{Strong convergence and the polygon property of 1-player games}}}.
\item {\red \href{https://mathoverflow.net/a/289320/}{MathOverflow answer \#289320} (with list of references)}.
\end{itemize}
\end{frame}

\begin{frame}
\fti{Defining 1-player games}

\begin{itemize}

\only<1>{
\item Let us generalize these examples.
}
\pause

\item A \textit{1-player game} consists of:
      \begin{itemize}
      \item a set of \textit{positions};
      \item a set of \textit{moves}, each of which goes from one position to another.
      \end{itemize}
      \pause
      In more familiar terms:
      \begin{itemize}
      \item game = digraph (possibly infinite);
      \item positions = vertices;
      \item moves = arcs.
      \end{itemize}
      \pause

\item A position is said to be \textit{terminal} if no moves are possible from this position
      (i.e., it is a vertex with outdegree $0$). \pause

\item If $u$ and $v$ are two positions (= vertices), then we write:
      \begin{itemize}
      \item $u \move v$ if we can get to $v$ from $u$ in one move \\ \qquad (i.e., there is an arc $u \to v$); \pause
      \item $u \moves v$ if we can get to $v$ from $u$ in several moves \\ \qquad (i.e., there is a walk $u \to v$).
      \end{itemize}
      \pause Note: $u \moves u$, since ``several moves'' includes ``$0$ moves''.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Monovariance, confluence}

\begin{itemize}

\item A 1-player game is said to be:
      \begin{itemize}
      \item \textit{monovariant} if there is a map $h$ from the set of
            all positions to $\NN$ such that
            \[
             h\tup{u} > h\tup{v} \text{ whenever } u \move v .
            \]
            \pause This means that there is a nonnegative-integer
            monovariant that decreases with each move. (Thus, the
            game always terminates.) \pause
      
      \item \textit{confluent} if for each position $u$, there is a
            \textbf{unique} terminal position $v$ such that
            $u \moves v$. \pause
            \\ This means that the terminal position does not depend
            on the choice of moves.
      \end{itemize}
      \pause

\item So, we can answer our questions from the previous sections
      if we can show that our games are monovariant and
      confluent. \pause

\item Note: Monovariance is not a necessary condition; we will
      loosen it later.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Local confluence}

\begin{itemize}

\item A 1-player game is said to be:
      \begin{itemize}
      \item \textit{locally confluent} if for any positions $u$, $v$
            and $w$ with \[ u \move v \text{ and } u \move w, \] there exists
            a position $t$ such that \[ v \moves t \text{ and } w \moves t . \]
            \pause
            \only<2>{Visually: \vspace{-0.2cm}
            \[
            \xymatrix{
            & u \ar[ld] \ar[rd] \\
            v & &  w
            }
            \]
            }%
            \only<3>{Visually: \vspace{-0.2cm}
            \[
            \xymatrix{
            & u \ar[ld] \ar[rd] \\
            v \arti[ddr] & & w \arti[ddl] \\
            & \\
            & t
            } .
            \]
            (Hence, local confluence is also called the ``diamond condition''.)
            } \pause
            \pause This means that if a position $u$ allows
            two possible moves $u \move v$ and $u \move w$, then
            there are a sequence of moves from $v$ and a sequence of
            moves from $w$ that lead to the same outcome. \\ \pause
            I.e., roughly speaking: There are no ``watershed decisions''
            that lead into irreconcileable branches.
      \end{itemize}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}

\fti{Newman's diamond lemma, finite case}

\begin{itemize}

\item \textbf{Theorem (Newman's lemma, aka diamond lemma, in the finite case).} \\
      \textbf{If} a 1-player game is
      \begin{itemize}
      \item \textbf{monovariant} and
      \item \textbf{locally confluent},
      \end{itemize}
      \textbf{then} it is \textbf{confluent}. \pause

\item In other words, in a monovariant 1-player game, confluence can be checked
      locally: \\
      If the result depends on the choice of moves, then we can pinpoint
      \textbf{one specific choice} that acts as a watershed.

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}

\fti{A Rosetta stone}

\begin{itemize}

\item The diamond lemma is used in many places, and different cultures use different languages. \\
      Attempt at a dictionary: \\
      \begin{tabular}{|c|c|c|}
       \hline \textbf{our terminology} & \textbf{digraphs} & \textbf{computer science} \\
       \hline 1-player game & digraph & abstract rewriting system (ARS) \\
       position & vertex & object \\
       move & arc & reduction step \\
       play sequence & walk & reduction sequence \\
       terminal position & sink & normal form \\
       \hline
      \end{tabular}
      Here, ``sink'' means ``vertex with outdegree $0$''; this has nothing to do with
      the ``sink'' in chip-firing.
      \pause

\item This is related to finite-state machines, but our moves aren't determined by input.

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}

\fti{Application: bubblesort, 1}

\begin{itemize}

\item Recall the bubblesort game on a poset:
      \begin{itemize}
      \item \textbf{Positions:} lists $\tup{a_1, a_2, \ldots, a_n}$ of $n$ elements of a poset $P$.
      \item \textbf{Moves:} Pick any $i \in \set{1,2,\ldots,n-1}$ such that $a_i > a_{i+1}$,
            and swap $a_i$ with $a_{i+1}$.
      \end{itemize} \pause

\item \textbf{Proposition.} The game always terminates, and the outcome does not depend on the choice of moves.
      \pause

\item \textit{Proof:} By the diamond lemma, it suffices to prove monovariance and local confluence. \\ \pause
      \only<4>{
      \textbf{Monovariance:} Let
      \begin{align*}
       h \tup{ a_1, a_2, \ldots, a_n }
       &= \tup{\text{number of inversions of } \tup{ a_1, a_2, \ldots, a_n }} \\
       &= \tup{\text{number of pairs } \tup{i, j} \text{ with } i < j \text{ and } a_i > a_j } .
      \end{align*}
      Easy to see:
      \[
        h\tup{u} > h\tup{v} \text{ whenever } u \move v .
      \]
      }
      \only<5->{
      \textbf{Local confluence:} If $u \move v$ and $u \move w$, then
      \begin{itemize}
       \item $v$ is obtained from $u$ by swapping $a_i$ with $a_{i+1}$;
       \item $w$ is obtained from $u$ by swapping $a_j$ with $a_{j+1}$.
      \end{itemize}
      Want to find $t$ such that $v \moves t$ and $w \moves t$. \pause
      \\ WLOG assume $j \geq i$ (else swap $v$ and $w$). \pause
      \begin{itemize}
      \item 
      \only<6>{
      \textbf{Case 1:} $j = i$. Then, $v \moves t$ and $w \moves t$ for $t = v = w$.
      }
      \end{itemize}
      }

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}

\fti{Application: bubblesort, 2}

\begin{itemize}

\item \textit{Proof (continued).}
      \textbf{Local confluence:}
      \begin{itemize}
      \item
      \only<1>{
      \textbf{Case 2:} $j = i+1$. Then, $a_i > a_{i+1} > a_{i+2}$ and
      \begin{align*}
       u &= \tup{\ldots, \underline{a_i, a_{i+1}}, a_{i+2}, \ldots}
       \move \tup{\ldots, a_{i+1}, a_i, a_{i+2}, \ldots} = v \qquad \text{and} \\
       u &= \tup{\ldots, a_i, \underline{a_{i+1}, a_{i+2}}, \ldots}
       \move \tup{\ldots, a_i, a_{i+2}, a_{i+1}, \ldots} = w.
      \end{align*}
      } \pause
      \only<2>{
      \textbf{Case 2:} $j = i+1$. Then, $x > y > z$ and
      \begin{align*}
       u &= \tup{\ldots, \underline{x, y}, z, \ldots}
       \move \tup{\ldots, y, x, z, \ldots} = v \qquad \text{and} \\
       u &= \tup{\ldots, x, \underline{y, z}, \ldots}
       \move \tup{\ldots, x, z, y, \ldots} = w.
      \end{align*}
      (We have renamed $a_i, a_{i+1}, a_{i+2}$ as $x, y, z$.)
      } \pause
      \only<3->{
      \textbf{Case 2:} $j = i+1$. Then, $x > y > z$ and
      \begin{align*}
       u &= \tup{\underline{x, y}, z}
       \move \tup{y, x, z} = v \qquad \text{and} \\
       u &= \tup{x, \underline{y, z}}
       \move \tup{x, z, y} = w.
      \end{align*}
      }
      \only<3>{(We have omitted all other entries.)
      } \pause
      \only<4>{
      ``Reconcile'' $v$ and $w$ as follows:
      \[
       \xymatrix@C=1cm{
       & u = \tup{x, y, z} \ar[dl] \ar[dr] \\
       v = \tup{y, x, z} \ar[d] & & w = \tup{x, z, y} \ar[d] \\
       \tup{y, z, x} \ar[dr] & & \tup{z, x, y} \ar[dl] \\
       & t = \tup{z, y, x}
       }
      \]
      }%
      \only<5>{
      ``Reconcile'' $v$ and $w$ as follows:
      \[
       \xymatrix@C=1cm{
       & u = \tup{x, y, z} \ar[dl] \ar[dr] \\
       v = \tup{y, x, z} \ar@{~>}[ddr] & & w = \tup{x, z, y} \ar@{~>}[ddl] \\
       & & \\
       & t = \tup{z, y, x}
       }
      \]
      }
      \end{itemize}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Application: bubblesort, 3}

\begin{itemize}

\item \textit{Proof (continued).}
      \textbf{Local confluence:}
      \begin{itemize}
      \item
      \only<1>{
      \textbf{Case 3:} $j > i+1$. Then, $a_i > a_{i+1}$ and $a_j > a_{j+1}$ and
      \begin{align*}
       u &= \tup{\ldots, \underline{a_i, a_{i+1}}, \ldots, a_j, a_{j+1}, \ldots} \\
       & \qquad \move \tup{\ldots, a_{i+1}, a_i, \ldots, a_j, a_{j+1}, \ldots} = v \qquad \text{and} \\
       u &= \tup{\ldots, a_i, a_{i+1}, \ldots, \underline{a_j, a_{j+1}}, \ldots} \\
       & \qquad \move \tup{\ldots, a_i, a_{i+1}, \ldots, a_{j+1}, a_j, \ldots} = w.
      \end{align*}
      } \pause
      \only<2>{
      \textbf{Case 3:} $j > i+1$. Then, $p > q$ and $x > y$ and
      \begin{align*}
       u &= \tup{\ldots, \underline{p, q}, \ldots, x, y, \ldots} \\
       & \qquad \move \tup{\ldots, q, p, \ldots, x, y, \ldots} = v \qquad \text{and} \\
       u &= \tup{\ldots, p, q, \ldots, \underline{x, y}, \ldots} \\
       & \qquad \move \tup{\ldots, p, q, \ldots, y, x, \ldots} = w.
      \end{align*}
      (We have renamed $a_i, a_{i+1}, a_j, a_{j+1}$ as $p, q, x, y$.)
      } \pause
      \only<3->{
      \textbf{Case 3:} $j > i+1$. Then, $p > q$ and $x > y$ and
      \begin{align*}
       u &= \tup{ \underline{p, q},  x, y} \\
       & \qquad \move \tup{ q, p,  x, y} = v \qquad \text{and} \\
       u &= \tup{ p, q,  \underline{x, y}} \\
       & \qquad \move \tup{ p, q,  y, x} = w.
      \end{align*}
      (We have omitted all other entries.)
      } \pause
      \only<4>{\\
      ``Reconcile'' $v$ and $w$ as follows:
      \[
       \xymatrix@C=1cm{
       & u = \tup{p, q, x, y} \ar[dl] \ar[dr] \\
       v = \tup{q, p, x, y} \ar[dr] & & w = \tup{p, q, y, x} \ar[dl] \\
       & t = \tup{q, p, y, x}
       }
      \]
      }
      \end{itemize}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Application: bubblesort, 4}

\begin{itemize}

\item \textit{Proof (continued).}
      We have now checked both monovariance and local confluence. \\
      Hence, by the diamond lemma, the game is confluent, qed. \pause

\item This is a folklore fact; for a writeup, see Section 4.2 of
      {\red \href{https://arxiv.org/src/1509.03803v2/anc/groth1alt.pdf}{Galashin/Grinberg/Liu, arXiv:1509.03803v2 ancillary file}}.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Application: chip-firing}

\begin{itemize}

\item Recall the chip-firing game on a digraph $D$ with vertex set $V$:
      \[
       \xymatrix{
        \underline{3} \ar[r] \ar[d] & 2 \ar[d] \\
        2 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
       \qquad \text{\raisebox{-.6cm}{$\longrightarrow$}}
       \qquad
       \xymatrix{
        1 \ar[r] \ar[d] & 3 \ar[d] \\
        3 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      \vspace{-0.2cm}
      \begin{itemize}
      \item \textbf{Positions:} chip configurations, i.e., maps $f : V \to \NN$.
      \item \textbf{Moves:} ``Firing'' a vertex $v \neq {\blue s}$ that has at least as many chips
            as it has outgoing arcs.
      \end{itemize} \pause

\item \textbf{Proposition.} The game always terminates, and the outcome does not depend on the choice of moves.
      \pause

\item \textit{Proof:} By the diamond lemma, it suffices to prove monovariance and local confluence. \\ \pause
      \only<4>{
      \textbf{Monovariance:} Let $t = \sum\limits_{v \in V} f\tup{v}$ and
      \[ h\tup{f} = \sum\limits_{v \in V} f\tup{v} \cdot \tup{\tup{t+1}^{\abs{V}} - \tup{t+1}^{\abs{V} - d\tup{v, s}} } , \]
      where $d \tup{v, s}$ is the minimum length of a path from $v$ to ${\blue s}$.
      }
      \only<5>{
      \textbf{Local confluence:} Easy: If two vertices can both be fired at the same time, then they can be fired in either order, and the outcome is the same.
      }

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}

\fti{Newman's diamond lemma, finite case: proof, 1}

\begin{itemize}

\item \textbf{Theorem (diamond lemma, in the finite case).} \\
      If a 1-player game is \textbf{monovariant} and \textbf{locally confluent},
      then it is \textbf{confluent}. \pause

\item \textit{Proof.} Let our game be monovariant (with function $h$) and
      locally confluent. \\
      We need to show that for each position $u$, there is a
      \textit{unique} {\red terminal} position reachable from $u$. \\
      (I say that $v$ is \textit{reachable from $u$} if $u \moves v$.) \\
      We call this statement $\calS(u)$. \pause \\
      We prove $\calS(u)$ by strong induction on $h\tup{u}$. \pause \\
      \textit{Induction step:} Let $h\tup{u} = n$.
      Assume that $\calS(x)$ holds for all positions $x$ with $h \tup{x} < n$. \pause \\
      Thus, for each position $x$ with $h \tup{x} < n$, there is a unique {\red terminal} position reachable from $x$. Call it {\red $x^\circ$}; thus, $x \moves {\red x^\circ}$. \pause \\
      WLOG $u$ is not terminal (otherwise, $\calS(u)$ is obvious). \pause \\
      Thus there is a $v$ such that $u \move v$. \pause \\
      Hence, $h\tup{v} < h\tup{u} = n$, so that {\red $v^\circ$} exists.

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Newman's diamond lemma, finite case: proof, 2}

\begin{itemize}

\item \textit{Proof (continued).} We must prove $\calS(u)$. So far we know:
      \begin{itemize}
      \item $u$ is a position with $h \tup{u} = n$.
      \item $v$ is a position with $u \move v$.
      \item {\red $v^\circ$} is a terminal position with $u \move v \moves {\red v^\circ}$.
      \end{itemize}
      \pause \only<2-3>{Thus, there exists \textbf{some} terminal position reachable from $u$ (namely, {\red $v^\circ$}).
      Remains to prove its uniqueness. \\}
      \only<2>{\vspace{0.55cm}}
      \only<3>{Let {\red $q$} be any other terminal position reachable from $u$. We want to prove ${\red q} = {\red v^\circ}$.}
%      \vspace{-0.4cm}
%      \begin{minipage}{0.3\textwidth}% adapt widths of minipages to your needs
      \only<2-3>{ \vspace{-0.4cm} }
      \only<2>{
      \[
       \xymatrix{
       & u \ar[dl] \\
       v \arti[dd]\\
       & {\white t} & {\white t} \\
       {\red v^\circ} & {\white t^\circ}
       }
      \]}
      \only<3-4>{
      \[
       \xymatrix{
       & u \ar[dl] \arti[dddr] \\
       v \arti[dd] &  \\
       & {\white t} &  \\
       {\red v^\circ} & {\white t^\circ} & {\red q}
       }
      \]}
      \only<5>{
      \[
       \xymatrix{
       & u \ar[dl] \ar[dr] \\
       v \arti[dd] & & w \arti[dd] \\
       & {\white t} \\
       {\red v^\circ} & {\white t^\circ} & {\red q}
       }
      \]}
      \only<6>{
      \[
       \xymatrix{
       & u \ar[dl] \ar[dr] \\
       v \arti[dd] \arti[dr] & & w \arti[dd] \arti[dl]  \\
       & t \\
       {\red v^\circ} & {\white t^\circ} & {\red q}
       }
      \]
      }
      \only<7>{
      \[
       \xymatrix{
       & u \ar[dl] \ar[dr] \\
       v \arti[dd] \arti[dr] & & w \arti[dd] \arti[dl]  \\
       & t \arti[d] \\
       {\red v^\circ} & {\red t^\circ} & {\red q}
       }
      \]
      }
      \only<8>{
      \[
       \xymatrix{
       & u \ar[dl] \ar[dr] \\
       v \arti[dd] \arti[dr] & & w \arti[dd] \arti[dl]  \\
       & t \arti[d] \\
       {\red v^\circ} & {\red t^\circ} \ar@{=}[l] & {\red q}
       }
      \]
      }
      \only<9>{
      \[
       \xymatrix{
       & u \ar[dl] \ar[dr] \\
       v \arti[dd] \arti[dr] & & w \arti[dd] \arti[dl]  \\
       & t \arti[d] \\
       {\red v^\circ} & {\red t^\circ} \ar@{=}[l] \ar@{=}[r] & {\red q}
       }
      \]
      }
%      \end{minipage}
%      \hspace{0.3cm}
%      \hfill
%      \begin{minipage}{0.6\textwidth}%\raggedleft
      \only<4>{Since {\red $q$} is terminal but $u$ is not, we have $u \move w \moves {\red q}$ for some position $w$.}
      \only<5>{
      Local confluence shows that there is a $t$ satisfying $v \moves t$ and $w \moves t$.}
      \only<6>{$h\tup{t} \leq h\tup{v} < h\tup{u} = n$; thus, {\red $t^\circ$} is well-defined. }
      \only<7>{$h\tup{v} < h\tup{u} = n$, so $\calS(v)$ holds. \\ Thus, there is a unique terminal position reachable from $v$. \\
      Since both {\red $v^\circ$} and {\red $t^\circ$} fit the bill, we thus obtain ${\red v^\circ} = {\red t^\circ}$.}
      \only<8>{$h\tup{w} < h\tup{u} = n$, so $\calS(w)$ holds. \\ Thus, there is a unique terminal position reachable from $w$. \\
      Since both {\red $q$} and {\red $t^\circ$} fit the bill, we thus obtain ${\red q} = {\red t^\circ}$.}
      \only<9>{Thus, ${\red q} = {\red t^\circ} = {\red v^\circ}$, qed.}
%      \end{minipage}
      \pause

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}

\fti{Newman's diamond lemma, finite case: a variant}

\begin{itemize}

\item \textbf{Theorem (diamond lemma, in the finite case).} \\
      If a 1-player game is monovariant and {locally confluent}, \\
      then it is {confluent}. \pause

\item \textbf{Theorem (Eriksson's polygon property theorem, in the finite case).} \\
      If a 1-player game is {monovariant} and {locally confluent},
      with the additional property that the walks $v \moves t$ and $w \moves t$
      in the local confluence condition have \textbf{equal lengths}, \\ \pause
      then it is {confluent}, with the additional property that
      for each position $v$, all walks from $v$ to the final position have
      \textbf{equal lengths}. \pause \\
      \textit{Proof idea.} Let $P$ be the set of positions. \\
      Define a new game, with
      \begin{itemize}
      \item set of positions $P \times \NN$;
      \item moves $\tup{u, k} \move \tup{v, k+1}$
            whenever $u \move v$ is a move of the original game and $k \in \NN$.
      \end{itemize}
      Apply the diamond lemma to this new game.

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}

\fti{``Baby diamond lemma''}

\begin{itemize}

\item \only<1>{Here is a similar, but simpler fact (exercise) also known as diamond lemma sometimes: \\} \pause
      \textbf{Theorem (``baby diamond lemma'').}
      Assume that a 1-player game has the following property:
      \begin{itemize}
      \item For any positions $u$, $v$
        and $w$ with $u \move v \text{ and } u \move w$, there exists
        a position $t$ such that $v \move t \text{ and } w \move t$.
      \end{itemize}
      \pause Then:
      \begin{itemize}
      \item For any positions $u$, $v$ and $w$ with
        \begin{align*}
        u &\moves v \text{ by a sequence of } n \text{ moves}; \text{ and }\\
        u &\moves w \text{ by a sequence of } m \text{ moves},
        \end{align*}
      there exists
        a position $t$ such that
        \begin{align*}
        v &\moves t \text{ by a sequence of } m \text{ moves}; \text{ and }\\
        w &\moves t \text{ by a sequence of } n \text{ moves}.
        \end{align*}
      \end{itemize} \pause

\item Note that monovariance is not required. \pause

\item Chip-firing satisfies the above property. Bubblesort does not. \pause

\item Some call only this theorem the ``diamond lemma''.

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}

\fti{``Baby diamond lemma'': proof idea}

\begin{itemize}

\item \textit{Proof idea for ``baby diamond lemma'':}
      \only<1>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] & & \ar[dr] \\
      & \ar[dl] & & & & \ar[dr] \\
      v & & & & & & w \\
      & \whitenothing \\
      & & \whitenothing
      }
      \]
      }
      \only<2>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] & & & & \ar[dr] \\
      v & & & & & & w \\
      & \whitenothing \\
      & & \whitenothing
      }
      \]
      }
      \only<3>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] & & \ar[dr] \\
      v & & & & & & w \\
      & \whitenothing \\
      & & \whitenothing
      }
      \]
      }
      \only<4>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v & & & & & & w \\
      & \whitenothing \\
      & & \whitenothing
      }
      \]
      }
      \only<5>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] & & & & w \\
      & \whitenothing \\
      & & \whitenothing
      }
      \]
      }
      \only<6>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] & & w \\
      & \whitenothing & & & \\
      & & \whitenothing
      }
      \]
      }
      \only<7>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & w \ar[dl] \\
      & \whitenothing & & & & & \\
      & & \whitenothing
      }
      \]
      }
      \only<8>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & w \ar[dl] \\
      & \whitenothing \ar[dr] & & \ar[dl] & & & \\
      & & \whitenothing
      }
      \]
      }
      \only<9>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & w \ar[dl] \\
      & \whitenothing \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \\
      & & \whitenothing & & & &
      }
      \]
      }
      \only<10>{
      \[
      \xymatrix{
      & & & u \ar[dl] \ar[dr] \\
      & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] \\
      v \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \ar[dr] & & w \ar[dl] \\
      & \whitenothing \ar[dr] & & \ar[dl] \ar[dr] & & \ar[dl] \\
      & & \whitenothing \ar[dr] & & \ar[dl] & \\
      & & & t
      }
      \]
      }      

\end{itemize}
\vspace{9cm}

\end{frame}

\begin{frame}
\fti{4. Further applications}
\begin{center}
{\Huge \bf \sc 4.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf Application: the domino game}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{https://doi.org/10.1016/0012-365X(95)00131-F}{Eriksson, \textit{Strong convergence and the polygon property of 1-player games}}}.
\item {\red \href{http://www.math.ku.dk/~olsson/manus/comb_rep_all.pdf}{Olsson, \textit{Combinatorics and Representations of Finite Groups}}}, sections 1--3.
\end{itemize}
\end{frame}

\begin{frame}
\fti{Application: The domino game, 1}

\begin{itemize}

\item Consider the following game:
      \begin{itemize}
      \item \textbf{Positions:} integer partitions (drawn as Young diagrams).
      \only<2->{
      \item \textbf{Moves:} Remove a domino (i.e., either $\ydiagram{2}$ or $\ydiagram{1,1}$)
            from the outer rim (i.e., the diagram must have no cells to the right
            or below the domino).
      }
      \end{itemize}
      \only<1>{ \vspace{1.6cm}
      \[
       \ydiagram{5, 5, 4, 1}
      \]
      }
      \only<2>{
      \[
       \ydiagram[*(white)]{5,5,1,1} *[*(red)]{0,0,1+2}
       \move \ydiagram[*(white)]{5,5,1,1}
      \]
      }
      \only<3>{
      \[
       \ydiagram[*(white)]{3,3,3,1} *[*(red)]{3+1,3+1}
       \move \ydiagram[*(white)]{3,3,3,1}
      \]
      }
      \only<4>{
      \[
       \ydiagram[*(white)]{2,1} *[*(red)]{0,0,0+1,0+1}
       \move \ydiagram[*(white)]{2,1}
      \]
      }
      \only<5>{
      \[
       \ydiagram[*(white)]{3,2,2} *[*(red)]{0,2+1,2+1}
       \move \ydiagram[*(white)]{3,2,2}
      \]
      }
      \only<6>{
      \begin{align*}
       \ydiagram[*(white)]{1+1} *[*(red)]{1,1}
       &\not\move \ydiagram[*(white)]{1+1} \qquad
       \textbf{not a valid move!}
      \end{align*}
      [\textbf{Note:} The ``outer rim'' condition ensures that the
      result of removing the domino is still a Young diagram,
      \textbf{without shifting}.]
      }
      \only<7>{Example of the game:
      \ytableausetup{boxsize=1em}
      \begin{align*}
       &\ydiagram[*(white)]{5,4,3,1,1} *[*(red)]{0,0,0,1+1,1+1}
       \move \ydiagram[*(white)]{5,4,1,1,1} *[*(red)]{0,0,1+2}
       \move \ydiagram[*(white)]{5,2,1,1,1} *[*(red)]{0,2+2} \\
       &\move \ydiagram[*(white)]{5,2,1} *[*(red)]{0,0,0,0+1,0+1}
       \move \ydiagram[*(white)]{3,2,1} *[*(red)]{3+2}
       \move \ydiagram[*(white)]{3,2,1}
      \end{align*}
      }

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Application: The domino game, 2}

\begin{itemize}

\item Consider the following game:
      \begin{itemize}
      \item \textbf{Positions:} integer partitions (drawn as Young diagrams).
      \item \textbf{Moves:} Remove a domino (i.e., either $\ydiagram{2}$ or $\ydiagram{1,1}$)
            from the outer rim (i.e., the diagram must have no cells to the right
            or below the domino).
      \end{itemize} \pause

\item \textbf{Proposition.} The game terminates and is confluent (i.e., the
      result does not depend on the choice of moves). \pause

\item \textit{Proof.} Apply the diamond lemma. \pause \\
      \only<4>{\textbf{Monovariance:} $h\tup{\lambda} = \abs{\lambda}$ decreases by $2$ with each move.
      }
      \pause
      \textbf{Local confluence:} Easy check. The only nontrivial case: \\
      \only<5>{two overlapping dominos that can be removed simultaneously:
      \[
       \ydiagram[*(white)]{5,3,2,2,1} *[*(yellow)]{0,3+1} *[*(blue)]{0,0,2+1} *[*(forestgreen)]{0,0,3+1}
      \]
      }
      \only<6>{(local view:) \vspace{-0.6cm}
      \[
       \xymatrix{
       & \ydiagram[*(white)]{1} *[*(yellow)]{0,0+1} *[*(blue)]{1+1} *[*(forestgreen)]{0,1+1} \ar[dl] \ar[dr] \\
       \ydiagram{1,1} & & \ydiagram{2} \\
       & {\white \varnothing}
       }
      \]
      }
      \only<7>{(local view:) \vspace{-0.6cm}
      \[
       \xymatrix{
       & \ydiagram[*(white)]{1} *[*(yellow)]{0,0+1} *[*(blue)]{1+1} *[*(forestgreen)]{0,1+1} \ar[dl] \ar[dr] \\
       \ydiagram{1,1} \ar[dr] & & \ydiagram{2} \ar[dl] \\
       & \varnothing
       }
      \]
      }

\end{itemize}

\vspace{9cm}

\end{frame}

% \begin{frame}
% \fti{Application: The domino game, 3}

% \begin{itemize}

% \item Consider the following game:
      % \begin{itemize}
      % \item \textbf{Positions:} integer partitions (drawn as Young diagrams).
      % \item \textbf{Moves:} Remove a domino (i.e., either $\ydiagram{2}$ or $\ydiagram{1,1}$)
            % from the outer rim (i.e., the diagram must have no cells to the right
            % or below the domino).
      % \end{itemize}

% \only<1-2>{
% \item \textbf{Proposition.} The game terminates and is confluent (i.e., the
      % result does not depend on the choice of moves).
% } \pause
% \only<2>{
% \item Moreover, the number of vertical dominos and the number of horizontal dominos removed
      % in the game also don't depend on the choice of moves.
% }  \pause
% \item Even better, the following also don't depend on the choice of moves:
      % \begin{itemize}
      % \item the multiset of rows from which vertical dominos were removed;
      % \item the multiset of columns from which horizontal dominos were removed.
      % \end{itemize}
      % \pause
      % \textit{Proof idea.} Again, define a new game whose positions ``remember'' this extra data,
      % as in the proof of the Polygon property. \pause \\
      % These two multisets are best encoded as two separate partitions.

% \end{itemize}

% \vspace{9cm}

% \end{frame}

\begin{frame}
\fti{Application: The domino game: terminal positions}

\begin{itemize}

\item The terminal positions are called the \textit{$2$-cores}, aka \textit{staircases}. \\
      They are the partitions of the form
      \[
       \tup{m, m-1, m-2, \ldots, 1} \qquad \text{for } m \in \NN .
      \]
      \[
       \ydiagram{4,3,2,1}
      \]
      \pause
      \only<2>{
      \textit{Proof idea.} If a Young diagram has no dominos to remove, then it can
      have neither two equal-length rows, nor two equal-length columns.
      Thus, each row is by $1$ shorter than the previous row.
      }
      % \pause

% \item Thus, each partition $\lambda$ of $n$ gives rise (by playing the game) to
      % \begin{itemize}
      % \item a $2$-core, which has the form $\tup{m, m-1, m-2, \ldots, 1}$ for some $m \in \NN$;
      % \item a partition $\mu^v$ encoding the multiset of rows from which vertical dominos were removed;
      % \item a partition $\mu^h$ encoding the multiset of columns from which horizontal dominos were removed.
      % \end{itemize}
      % \pause These satisfy $n = m\tup{m+1}/2 + 2 \abs{\mu^v} + 2 \abs{\mu^h}$. \pause \\
      % This gives a bijection $\lambda \mapsto \tup{m, \mu^v, \mu^h}$.

\end{itemize}

\vspace{9cm}

\end{frame}

% \begin{frame}
% \fti{Application: The domino game, 5}

% \begin{itemize}

% \item Thus, for each $n \in \NN$, we have a bijection
      % \begin{align*}
       % &\set{\text{partitions of } n} \\
      % \to &\bigsqcup_{\substack{m, a, b \in \NN ; \\ m\tup{m+1}/2 + 2a + 2b = n}} \set{\text{partitions of } a} \times \set{\text{partitions of } b} .
      % \end{align*}
      % \pause

% \item Hence the identity
      % \[
       % p_n = \sum_{\substack{m, a, b \in \NN ; \\ m\tup{m+1}/2 + 2a + 2b = n}} p_a p_b ,
      % \]
      % where $p_k$ stands for the number of partitions of $k$. \pause

% \item In other words: $F\tup{x} = F\tup{x^2}^2 G\tup{x}$, where
      % \[
       % F\tup{x} = \prod_{k=1}^\infty \dfrac{1}{1-x^k} \qquad \text{and} \qquad G\tup{x} = \sum_{m=0}^\infty x^{m\tup{m+1}/2}.
      % \]
      % \pause

% \item See also {\red \href{https://artofproblemsolving.com/community/c6h1392038}{AoPS post \#1392038}}.

% \end{itemize}

% \vspace{9cm}

% \end{frame}

\begin{frame}
\fti{Application: The domino game, generalized}

\begin{itemize}

\item More generally, instead of removing dominos, one can remove ``$p$-rim hooks'' for any given positive integer $p$.
      \\
      (Eriksson calls this the ``$p$-snake game''.)
      \\
      This gives rise to ``$p$-cores'' (useful in characteristic-$p$ representation theory of symmetric groups).

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{5. The general diamond lemma}
\begin{center}
{\Huge \bf \sc 5.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf The general diamond lemma}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{http://www.cs.chalmers.se/~coquand/bul.ps}{Bezem, Coquand, \textit{Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic}}}.
\end{itemize}
\end{frame}

\begin{frame}
\fti{Monovariance revisited, 1}

\begin{itemize}

\item \textbf{Recall:} A 1-player game is said to be:
      \begin{itemize}
      \item \textit{monovariant} if there is a map $h$ from the set of
            all positions to $\NN$ such that
            \[
             h\tup{u} > h\tup{v} \text{ whenever } u \move v .
            \]
      \end{itemize} \pause

\item This is often too restrictive in practice. \pause

\item Standard answer: replace monovariance by ``termination'':

\item A 1-player game is said to be:
      \begin{itemize}
      \item \textit{terminating}
            if there is no infinite chain
            $u_0 \move u_1 \move u_2 \move \cdots$ .
      \end{itemize} \pause
      
\item \textbf{Theorem (Newman's lemma, classical version).} \\
      \textbf{If} a 1-player game is
      \begin{itemize}
      \item \textbf{terminating} and
      \item \textbf{locally confluent},
      \end{itemize}
      \textbf{then} it is \textbf{confluent}. \pause

\item This is actually an ``if and only if''. \pause

\item \textbf{Bad news:} This theorem is no longer constructive,
      and the proof uses tricky logic.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Monovariance revisited, 2}

\begin{itemize}

\item Fortunately, we can turn the theorem constructive \textbf{and}
      make the proof simple again. \pause \\
      \textbf{Trick (Bezem/Coquand):} Replace ``terminating'' by
      ``Noetherian'', and define the latter constructively by
      requiring an induction rule to work. \pause \\
      (You might have seen Noetherian induction.
      Imagine defining a Noetherian space as a space on which
      Noetherian induction works, rather than using chains of subspaces!) \pause
\item I will use my own notations, but the idea is from Bezem/Coquand.
      \pause

\item We will use posets (= partially ordered sets); but totally ordered
      sets are enough for what we want to do. \\
      You may read ``totally ordered set'' for ``poset'' in the following.

\end{itemize}

\vspace{9cm}
      
\end{frame}

\begin{frame}
\fti{Monovariance revisited, 3}

\begin{itemize}

\item A poset $S$ is said to be
      \textit{Noetherian} if
      and only if it allows (strong) induction over $s \in S$,
      i.e., if the following rule holds:
      \begin{itemize}
      \item If $\mathcal{A}\left(s\right)$ is a statement for each
            $s \in S$, and if each $s \in S$ satisfies
            \[
            \left( \mathcal{A}\left(t\right) \text{ for all } t < s \right)
            \Longrightarrow \mathcal{A}\left(s\right) ,
            \]
            then each $s \in S$ satisfies $\mathcal{A}\left(s\right)$.
      \end{itemize}
      \pause

\item A 1-player game is said to be:
      \begin{itemize}
      \item {\blue \textit{Noetherian}} if there is a map $h$ from the set of
            all positions to {\blue a Noetherian poset $S$} such that
            \[
             h\tup{u} > h\tup{v} \text{ whenever } u \move v .
            \]
      \end{itemize} \pause

\item \textbf{Theorem (Newman's lemma, constructive version).} \\
      \textbf{If} a 1-player game is
      \begin{itemize}
      \item {\blue \textbf{Noetherian}} and
      \item \textbf{locally confluent},
      \end{itemize}
      \textbf{then} it is \textbf{confluent}. \pause

\item Note how lazy we are: All but the blue parts are copied from the finite
      case!
      The proof, too, can be directly copied over.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Examples of Noetherian posets}

\begin{itemize}

\item This is only useful if we can find
      Noetherian posets $S$. \pause

\item In classical logic, a poset $S$ is Noetherian if it has no
      infinite chains $s_0 > s_1 > s_2 > \cdots$. \\
      So this is just the obvious way to force the game to be terminating.
      \pause

\item In constructive logic: \\
      First of all, $\NN$ is Noetherian. \pause \\
      So is each finite poset.
      \pause \\
      What else?

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Lexicographic product: definition}

\begin{itemize}

\item Let $P$ and $Q$ be two posets. \\
      The \textit{lexicographic product} of $P$ and $Q$ is the poset
      $P \times Q$ with ordering given by
      \begin{align*}
      \left(\left(p, q\right) < \left(p', q'\right) \right)
      \ \Longleftrightarrow \ %
      \left( \left(p < p'\right) \text{ or } \left(p = p' \text{ and } q < q'\right) \right) .
      \end{align*} \pause

\item If $P$ and $Q$ are totally ordered, then so is $P \times Q$. \pause

\item The lexicographic product is associative, and thus extends to several posets,
      yielding
      $P_1 \times P_2 \times \cdots \times P_k$ with
      lexicographic order: \pause
      \begin{align*}
      & \ \left( \tup{a_1, a_2, \ldots, a_k} > \tup{b_1, b_2, \ldots, b_k} \right) \\
      \Longleftrightarrow
      & \ \left( \text{there is some } i \text{ such that } a_i > b_i \text{, and} \right. \\
      & \ \qquad \left. \text{each } j < i \text{ satisfies } a_j = b_j \right) .
      \end{align*} \pause

\item \textbf{Theorem.} If $P$ and $Q$ are Noetherian posets, then so is their
      lexicographic product $P \times Q$.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Lexicographic product: proof of Noetherianness}

\begin{itemize}

\item \textbf{Theorem.} If $P$ and $Q$ are Noetherian posets, then so is their
      lexicographic product $P \times Q$. \pause

\item \textit{Proof idea.} Assume $P$ and $Q$ are Noetherian. \\ \pause
      Let $\mathcal{A}\left(p, q\right)$ be a statement for each
      $\tup{p, q} \in P \times Q$. \\
      Assume that each $\tup{p, q} \in P \times Q$ satisfies
      \[
      \left( \mathcal{A} \tup{p', q'} \text{ for all } \tup{p', q'} < \tup{p, q} \right)
      \Longrightarrow \left( \mathcal{A} \tup{p, q} \right) .
      \]
      Goal: Show that each $\tup{p, q} \in P \times Q$ satisfies
      $\mathcal{A} \tup{p, q}$. \pause

\item Prove $\mathcal{A} \tup{p, q}$ by induction on $p$ (thanks to Noetherianness of $P$,
      using
      \[
      \mathcal{A}'\left(p\right) := \left(\mathcal{A}\left(p,q\right) \text{ holds for all } q \in Q \right)
      \]
      as the statement) and, inside it, an induction on $q$ (thanks to Noetherianness of $Q$). \pause

\item This proves the Theorem. \pause

\item \textbf{Corollary.} If $P_1, P_2, \ldots, P_k$ are finitely many Noetherian posets,
      then their lexicographic product $P_1 \times P_2 \times \cdots \times P_k$
      is Noetherian as well.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Chip-firing revisited}

\begin{itemize}

\item \textbf{Example} for use of a lexicographic product:

\item Recall the chip-firing game on a digraph $D$ with vertex set $V$:
      \[
       \xymatrix{
        \underline{3} \ar[r] \ar[d] & 2 \ar[d] \\
        2 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
       \qquad \text{\raisebox{-.6cm}{$\longrightarrow$}}
       \qquad
       \xymatrix{
        1 \ar[r] \ar[d] & 3 \ar[d] \\
        3 \ar[ru] \ar[r] & 1 \ar[r] & {\blue 2} \ar[lu]
       }
      \]
      \vspace{-0.2cm}
      \begin{itemize}
      \item \textbf{Positions:} chip configurations, i.e., maps $f : V \to \NN$.
      \item \textbf{Moves:} ``Firing'' a vertex $v \neq {\blue s}$ that has at least as many chips
            as it has outgoing arcs.
      \end{itemize} \pause

\only<2>{
\item We proved monovariance using
      \begin{align*}
      h : \set{\text{positions}} &\to \NN , \\
                f       &\mapsto \sum\limits_{v \in V} f\tup{v} \cdot \tup{\tup{t+1}^{\abs{V}} - \tup{t+1}^{\abs{V} - d\tup{v, s}} } ,
      \end{align*}
      where $t = \sum\limits_{v \in V} f\tup{v}$ and
      where $d \tup{v, s}$ is the minimum length of a path from $v$ to ${\blue s}$.
}

\only<3>{
\item We can more easily prove Noetherianness using
      \begin{align*}
      h : \set{\text{positions}} &\to \tup{\text{lexicographic product of } m+1 \text{ copies of } \NN } , \\
                f       &\mapsto \left(\sum\limits_{v \in V;\  d \tup{v, s} > k} f\tup{v} \right)_{0 \leq k \leq m} ,
      \end{align*}
      where $m = \max_{v \in V} d \tup{v, s}$. \pause \\
      (The monovariance was an afterthought of this.)
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Finite subsets form a Noetherian order: statement}

\begin{itemize}

\item Here comes another way of constructing Noetherian totally ordered sets. \pause

\item Let $S$ be a totally ordered set. \\
      Let $\Pfin\tup{S}$ be the set of all finite subsets of $S$. \\
      Equip $\Pfin\tup{S}$ with a total order as follows:
      \begin{align*}
      \left( A \leq B \right)
      \ \Longleftrightarrow \  %
      \left( A \subseteq B \text{ or } \max \left(A \setminus B \right) < \max \left(B \setminus A \right) \right) .
      \end{align*}
      (We understand $\max \left(A \setminus B \right) < \max \left(B \setminus A \right)$ to be false if $B \subseteq A$.)
      \pause \\
      In other words, $A \leq B$ if and only if $A$ can be obtained from $B$
      by repeatedly
      \begin{itemize}
      \item removing an element;
      \item replacing an element by (possibly several) smaller elements.
      \end{itemize}
      \pause

\item It is easy to see that $\Pfin\tup{S}$ is totally ordered.

\item \textbf{Theorem.}
       If $S$ is Noetherian, then so is $\Pfin\tup{S}$.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Finite subsets form a Noetherian order: proof, 1}

\begin{itemize}

\item \textbf{Theorem.}
       If $S$ is Noetherian, then so is $\Pfin\tup{S}$.

\item \textit{Proof idea.} Assume $S$ is Noetherian. \pause \\
      For each $a \in S$, we let $S_{\leq a}$ be the subset
      $\set{s \in S \mid s \leq a}$ of $S$ (a totally ordered set,
      with order inherited from $S$). \\
      Thus, $\Pfin\tup{S_{\leq a}}$ is a sub-totally ordered set of $\Pfin\tup{S}$. \pause
\item For each $a \in S$, let $\mathcal{G}\tup{a}$ be the statement
      $\left(\Pfin\tup{S_{\leq a}} \text{ is Noetherian}\right)$. \\
      We shall prove that $\mathcal{G}\tup{a}$ holds for all $a \in S$. \\
      This will easily yield the claim (since the $S_{\leq a}$ for all $a$ cover $S$). \pause
\item We shall prove $\mathcal{G}\tup{a}$ by induction on $a$ (since $S$ is Noetherian).
      So we assume that $\mathcal{G}\tup{b}$ holds for all $b < a$. \pause
\item We must prove $\mathcal{G}\tup{a}$. \\
      In other words, we must prove that $\Pfin\tup{S_{\leq a}}$ is Noetherian. \pause
\item Let $\mathcal{A}\tup{M}$ be a statement for each $M \in \Pfin\tup{S_{\leq a}}$. \\
      Assume that $\mathcal{A}\tup{M}$ holds whenever all $N < M$ satisfy $\mathcal{A}\tup{N}$. \\
      We must show that $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Finite subsets form a Noetherian order: proof, 2}

\begin{itemize}

\item What we know so far:
      \begin{enumerate}
      \item[(1)] $\mathcal{G}\tup{b}$ holds (that is, $\Pfin\tup{S_{\leq b}}$ is Noetherian) for all $b < a$.
      \item[(2)] $\mathcal{A}\tup{M}$ is a statement for each $M \in \Pfin\tup{S_{\leq a}}$.
      \item[(3)] $\mathcal{A}\tup{M}$ holds whenever all $N < M$ satisfy $\mathcal{A}\tup{N}$.
      \end{enumerate}
      We must show that $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$. \pause

\item First, we claim that
      \begin{enumerate}
      \item[(4)] $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq b}}$ for each $b < a$.
      \end{enumerate}
      Indeed, this is proven by induction on $M$, which is allowed by (1), and which uses (3) for the induction step. \pause

\item Rewrite (4) (and the obvious fact that $\mathcal{A}\tup{\varnothing}$ holds, which again follows from (3)) as
      \begin{enumerate}
      \item[(5)] $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \notin M$.
      \end{enumerate} \pause

\item Thus, (3) yields that $\mathcal{A}\tup{\set{a}}$ holds.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Finite subsets form a Noetherian order: proof, 3}

\begin{itemize}

\item What we know so far:
      \begin{enumerate}
      \item[(1)] $\mathcal{G}\tup{b}$ holds (that is, $\Pfin\tup{S_{\leq b}}$ is Noetherian) for all $b < a$.
      \item[(2)] $\mathcal{A}\tup{M}$ is a statement for each $M \in \Pfin\tup{S_{\leq a}}$.
      \item[(3)] $\mathcal{A}\tup{M}$ holds whenever all $N < M$ satisfy $\mathcal{A}\tup{N}$.
      \item[(5)] $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \notin M$.
      \end{enumerate}
      We must show that $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$. \pause

\item Next, we claim that
      \begin{enumerate}
      \item[(6)] $\mathcal{A}\tup{M \cup \set{a}}$ holds for each $M \in \Pfin\tup{S_{\leq b}}$ for each $b < a$.
      \end{enumerate}
      Indeed, this is proven by induction on $M$, which is allowed by (1), and which uses (3) and (5) for the induction step
      (since each set in $\Pfin\tup{S_{\leq a}}$ that is $< M \cup\set{a}$ is either of the form $N \cup\set{a}$
      with $N < M$, or does not contain $a$). \pause

\item Rewrite (6) (and the fact that $\mathcal{A}\tup{\set{a}}$ holds) as
      \begin{enumerate}
      \item[(7)] $\mathcal{A}\tup{M \cup \set{a}}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \notin M$.
      \end{enumerate}
      
\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Finite subsets form a Noetherian order: proof, 4}

\begin{itemize}

\item What we know so far:
      \begin{enumerate}
      \item[(2)] $\mathcal{A}\tup{M}$ is a statement for each $M \in \Pfin\tup{S_{\leq a}}$.
      \item[(5)] $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \notin M$.
      \item[(7)] $\mathcal{A}\tup{M \cup \set{a}}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \notin M$.
      \end{enumerate}
      We must show that $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$. \pause

\item Rewrite (7) as
      \begin{enumerate}
      \item[(8)] $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$ satisfying $a \in M$.
      \end{enumerate} \pause
      
\item Combine (5) with (8) to conclude that $\mathcal{A}\tup{M}$ holds for each $M \in \Pfin\tup{S_{\leq a}}$. \\
      Thus, we proved that $\Pfin\tup{S_{\leq a}}$ is Noetherian. \pause

\item To prove that $\Pfin\tup{S}$ is Noetherian, it suffices to notice that each $M \in \Pfin\tup{S}$
      belongs to $\Pfin\tup{S_{\leq a}}$ for some $a \in S$ (or is empty). \pause

\item (I've got the idea from Mines/Richman/Ruitenburg, \textit{A Course in Constructive Algebra}, proof of Theorem 6.4.
      They work with different notations and prove a more general result.)

\end{itemize}

\vspace{9cm}

\end{frame}


\begin{frame}
\fti{More posets}

\begin{itemize}

\item In classical logic, there are several nontrivial Noetherian posets:
      \begin{itemize}
      \item weakly decreasing tuples of arbitrary size with lexicographic order;
      \item infinite sequences with lexicographic order;
      \item trees (infamous hydra theorem);
      \item graphs w.r.t. minor relation,
      \item etc.
      \end{itemize}
      (Correct me if/where I'm wrong.) \\
      I don't know which of these are still Noetherian in constructive logic.

\end{itemize}

\vspace{9cm}

\end{frame}

% The following two frames are commented out since the proof is wrong and I'm
% not even sure if the Theorem is correct.

% \begin{frame}
% \fti{Monomialization: definition}

% \begin{itemize}

% \item Here is a poset transformation that preserves Noetherianness: %
      % \item Let $P$ be a poset.
      % \item A \textit{$P$-trail} shall mean a finite weakly
      % decreasing tuple $\tup{a_1 \geq a_2 \geq \cdots \geq a_k}$ of
      % elements of $P$. \pause
      % \item If $\overrightarrow{a} = \tup{a_1 \geq a_2 \geq \cdots \geq a_k}$ and
      % $\overrightarrow{b} = \tup{b_1 \geq b_2 \geq \cdots \geq b_\ell}$ are two
      % $P$-trails, then we write $\overrightarrow{a} \geq \overrightarrow{b}$ if and only
      % if
      % \begin{itemize}
      % \item \textbf{either} $\overrightarrow{b}$ is a prefix of $\overrightarrow{a}$
            % (that is, $k \geq \ell$ and
            % $\tup{b_1 \geq b_2 \geq \cdots \geq b_\ell}
            % = \tup{a_1 \geq a_2 \geq \cdots \geq a_\ell}$),
      % \item \textbf{or} there exists an $i$ such that
            % \[
            % a_i > b_i, \qquad \text{ but } a_j = b_j \text{ for all } j < i .
            % \]
      % \end{itemize}
      % \pause
      % \item The set of $P$-trails, equipped with this partial order, will
            % be denoted by $\mathcal{M}\left(P\right)$ and called the
            % \textit{monomialization} of $P$. \pause
      % \item If $P$ is totally ordered, then so is $\mathcal{M}\left(P\right)$. \\
            % (This is one of the forms of lexicographic order.) \pause
      % \item \textbf{Theorem (constructive form of Gordan's lemma).}
            % If $P$ is Noetherian, then so is $\mathcal{M}\left(P\right)$.

% \end{itemize}

% \vspace{9cm}

% \end{frame}

% \begin{frame}
% \fti{Monomialization: proof of Noetherianness of $\mathcal{M}\left(P\right)$}

% \begin{itemize}

% \item \textbf{Theorem (constructive form of Gordan's lemma).}
            % If $P$ is Noetherian, then so is $\mathcal{M}\left(P\right)$.

% \item \textit{Proof idea.} Assume $P$ is Noetherian. \pause \\
      % Let $\mathcal{A}\left(\overrightarrow{s}\right)$ be a statement for each
      % $\overrightarrow{s} \in \mathcal{M}\left(P\right)$.
      % Assume that each $\overrightarrow{s} \in \mathcal{M}\left(P\right)$ satisfies
            % \[
            % \left( \mathcal{A}\left(\overrightarrow{t}\right) \text{ for all } \overrightarrow{t} < \overrightarrow{s} \right)
            % \Longrightarrow \mathcal{A}\left(\overrightarrow{s}\right) .
            % \]
      % Goal: Show that each $\overrightarrow{s} \in \mathcal{M}\left(P\right)$ satisfies $\mathcal{A}\left(\overrightarrow{s}\right)$.
      % \pause

% \item Define an auxiliary predicate:
      % For each $a \in P$ and $g \in \NN$, let $\mathcal{S}\left(a,g\right)$ mean that
      % every $P$-trail $\overrightarrow{s}$ with the properties that
      % \begin{itemize}
      % \item all entries of $\overrightarrow{s}$ are $\leq a$;
      % \item at most $g$ entries of $\overrightarrow{s}$ are $= a$
      % \end{itemize}
      % satisfies $\mathcal{A}\left(\overrightarrow{s}\right)$. \pause

% \item Prove $\mathcal{S}\left(a,g\right)$ by induction on $a$ (thanks to Noetherianness of $P$,
      % using
      % \[
      % \mathcal{A}\left(a\right) := \left(\mathcal{S}\left(a,g\right) \text{ holds for all } g \in \NN\right)
      % \]
      % as the statement) and, inside it, an induction on $g$.

% \end{itemize}

% \vspace{9cm}

% \end{frame}

\begin{frame}
\fti{6. Application: Gr\"obner bases}
\begin{center}
{\Huge \bf \sc 6.} \\
\noindent\rule[0.5ex]{\linewidth}{1pt}
{\Large \bf Application: Gr\"obner bases}
\end{center}
\vspace{1cm}
References:
\begin{itemize}
\item {\red \href{https://www.maths.tcd.ie/~vdots/AlgebraicOperadsAnAlgorithmicCompanion.pdf}{Bremner/Dotsenko, \textit{Algebraic Operads: An Algorithmic Companion}}}.
\item Becker/Weispfennig, \textit{Gr\"obner Bases: A computational approach to commutative algebra}.
\item Cox/Little/O'Shea, \textit{Ideals, Varieties, and Algorithms}.
\end{itemize}
\end{frame}

\begin{frame}

\fti{Introduction: polynomial division, the game, 1}

\begin{itemize}

\item Fix a commutative ring $\KK$, and a monic polynomial
      \[
       d = x^m - d_1 x^{m-1} - d_2 x^{m-2} - \cdots - d_m x^0 \in \KK\ive{x} .
      \]

\item The polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} polynomials $f \in \KK\ive{x}$.
      \item \textbf{Moves:} Pick any $n \geq m$ such that $x^n$ appears in $f$;
            call $c$ its coefficient;
            subtract $c x^{n-m} d$ from $f$
            % replace the term
            % \[
            % c x^n \text{ by } c d_1 x^{n-1} + c d_2 x^{n-2} + \cdots + c d_m x^{n-m}
            % \]
            % in $f$
            (that is, subtract the multiple of $d$ that kills the $x^n$-term in $f$ and leaves the higher terms unchanged).
      \end{itemize}
      (``Appears in $f$'' means ``appears with nonzero coefficient in $f$''.) \pause

\item \textbf{Proposition.} The game always terminates, and the outcome does not depend on the choice of moves.
      
\end{itemize}

\vspace{9cm}

\end{frame}


\begin{frame}
\fti{Introduction: polynomial division, the game, 2}

\begin{itemize}

\item The polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} polynomials $f \in \KK\ive{x}$.
      \item \textbf{Moves:} Pick any $n \geq m$ such that $x^n$ appears in $f$;
            call $c$ its coefficient in $f$;
            subtract $c x^{n-m} d$ from $f$.
            % replace the term
            % \[
            % c x^n \text{ by } c d_1 x^{n-1} + c d_2 x^{n-2} + \cdots + c d_m x^{n-m}
            % \]
            % in $f$.
      \end{itemize}

\item \textbf{Proposition.} The game always terminates, and the outcome does not depend on the choice of moves.
      \pause

\only<2-4>{
\item \textit{Proof:} By the (general) diamond lemma, it suffices to prove Noetherianness and local confluence. \\ \pause
      \only<3>{
      \textbf{Noetherianness:} Let
      \begin{align*}
       h : \KK\ive{x} &\to \Pfin\tup{\NN}, \\
       f &\mapsto \set{n \in \NN \mid x^n \text{ appears in } f} .
      \end{align*}
      Easy to see:
      \[
        h\tup{u} > h\tup{v} \text{ whenever } u \move v .
      \]
      }
      \only<4>{
      \textbf{Local confluence:} Exercise.
      }
}
\only<5>{
\item This shouldn't come as a surprise: The ``game'' is just polynomial division by $d$,
      but done in an unsystematic (and slow) fashion.
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Introduction: polynomial division, modified}

\begin{itemize}

\only<1-7>{
\item Let us modify the game somewhat to make it more predictable.
}
\only<2-3>{
\item The polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} polynomials $f \in \KK\ive{x}$.
      \item \textbf{Moves:} Pick any $n \geq m$ {\blue such that $x^n$ appears in $f$}; \\
            call $c$ its coefficient in $f$; \\
            subtract $c x^{n-m} d$ from $f$.
            % replace the term
            % \[
            % c x^n \text{ by } c d_1 x^{n-1} + c d_2 x^{n-2} + \cdots + c d_m x^{n-m}
            % \]
            % in $f$.
      \end{itemize}
}
\only<3>{
\item The move requires the coefficient of $x^n$ to be nonzero. \\
      This is fickle and not very constructive. \\
      Better: Keep track of powers of $x$ that have already been killed in previous moves (but not by random cancellation), and only require $x^n$ to be not one of them.
}

\only<4->{
\item The {\blue modified} polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} {\blue pairs $\tup{M, f}$ consisting of an $M \in \Pfin\tup{\NN}$ and a} polynomial $f \in \KK\ive{x}$.
      \item \textbf{Moves:} Pick any $n \geq m$ {\blue such that $n \in M$}; \\
            call $c$ its coefficient in $f$; \\
            {\blue replace $n$ by $n-1, n-2, \ldots, n-m$ in $M$}; \\
            subtract $c x^{n-m} d$ from $f$.
            % replace the term
            % \[
            % c x^n \text{ by } c d_1 x^{n-1} + c d_2 x^{n-2} + \cdots + c d_m x^{n-m}
            % \]
            % in $f$.
      \end{itemize}
}
\only<5>{
\item All changes are in blue. \\
      The set $M$ keeps track of all powers of $x$ that can possibly still appear in $f$,
      but random cancellations do not get removed from $M$.
}
\only<6-7>{
\item If we forget about $M$, then each move of the modified game either
      corresponds to a move or the original game, or leaves $f$ unchanged.
}
\only<7-8>{
\item \textbf{Proposition.} The modified game always terminates, and the outcome does not depend on the choice of moves.
}
\only<8>{
\item \textit{Proof.} As for the previous game, but easier. \\
      \textbf{Noetherianness:} Let
      \begin{align*}
       h : \set{\text{positions}} &\to \Pfin\tup{\NN}, \\
       \tup{M, f} &\mapsto M .
      \end{align*}
      \textbf{Local confluence:} Even easier than before.
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multiple variables}

\begin{itemize}

\only<1>{
\item Let us generalize: \pause
}
\item Consider a polynomial ring $\KK\ive{x_1, x_2, \ldots, x_n}$ in $n$ variables.
\item \textit{Monomials} are formal expressions $x_1^{a_1} x_2^{a_2} \cdots x_n^{a_n}$ with
      $\tup{a_1, a_2, \ldots, a_n} \in \NN^n$. \pause
\only<3-4>{
\item Monomials can be multiplied in the obvious way.
\item We say that a monomial $\mathfrak{m} = x_1^{a_1} x_2^{a_2} \cdots x_n^{a_n}$
      \textit{divides} a monomial
      $\mathfrak{n} = x_1^{b_1} x_2^{b_2} \cdots x_n^{b_n}$ if $a_i \leq b_i$
      for all $i$. \\
      In this case,
      $\mathfrak{n} / \mathfrak{m} := x_1^{b_1 - a_1} x_2^{b_2 - a_2} \cdots x_n^{b_n - a_n}$.
}
\only<4>{
\item The \textit{lcm} (lowest common multiple) of two monomials
      $\mathfrak{m} = x_1^{a_1} x_2^{a_2} \cdots x_n^{a_n}$
      and $\mathfrak{n} = x_1^{b_1} x_2^{b_2} \cdots x_n^{b_n}$
      is defined to be the monomial
      $\lcm\tup{\mathfrak{m}, \mathfrak{n}}
      := x_1^{\max\set{a_1, b_1}} x_2^{\max\set{a_2, b_2}} \cdots x_n^{\max\set{a_n, b_n}}$.
}
\only<5->{
\item We equip $\NN^n$ with the lexicographic order (i.e., the total order obtained
      as the lexicographic product $\NN \times \NN \times \cdots \times \NN$).
      \pause
\item We transfer this order to monomials. Thus,
      \begin{align*}
      & \ \left( x_1^{a_1} x_2^{a_2} \cdots x_n^{a_n} > x_1^{b_1} x_2^{b_2} \cdots x_n^{b_n} \right) \\
      \Longleftrightarrow
      & \ \left( \tup{a_1, a_2, \ldots, a_n} > \tup{b_1, b_2, \ldots, b_n} \right) \\
      \Longleftrightarrow
      & \ \left( \text{there is some } i \text{ such that } a_i > b_i \text{, and} \right. \\
      & \ \qquad \left. \text{each } j < i \text{ satisfies } a_j = b_j \right) .
      \end{align*}
}
\only<6>{
\item This is a total order. \\
      Thus, every nonzero polynomial $p$ has a unique \textit{leading monomial}
      (i.e., maximum monomial appearing with nonzero coefficient). \\
      We say that $p$ is \textit{monic} if the coefficient of its leading monomial is $1$.
}
\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game}

\begin{itemize}

\item Fix a commutative ring $\KK$, and finitely many monic polynomials $g_1, g_2, \ldots, g_k$
      in $\KK\ive{x_1, x_2, \ldots, x_n}$. \pause \\
      For each $i$, let $\mathfrak{h}_i$ be the leading monomial of $g_i$. \pause

\item The multivariate polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} polynomials $f \in \KK\ive{x_1, x_2, \ldots, x_n}$.
      \item \textbf{Moves:} Pick any monomial $\mathfrak{m}$ that appears in $f$
            and any $i$ such that $\mathfrak{h}_i \mid \mathfrak{m}$.
            Call $c$ the coefficient of $\mathfrak{m}$ in $f$.
            Subtract $c \tup{\mathfrak{m} / \mathfrak{h}_i} g_i$ from $f$
            % Replace the term
            % \[
            % c \mathfrak{m} \text{ by } - c \tup{\mathfrak{m} / \mathfrak{h}_i} \tup{g_i - \mathfrak{h}_i}
            % \]
            % in $f$
            (that is, subtract the multiple of $g_i$ that kills the
            $\mathfrak{m}$-term in $f$ and leaves higher terms unchanged).
      \end{itemize} \pause

\item The game always terminates. \pause

\item When is it confluent?

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Example 1}

\begin{itemize}

\item \textbf{Example 1:}
      \begin{itemize}
      \item $n = 2$. Write $x$ and $y$ for $x_1$ and $x_2$.
      \item $k = 2$. Let $g_1 = {\blue x^2 y} - x$ and $g_2 = {\blue y^2 x} - y$.
      \end{itemize}

\only<2>{
\item Start the game with $f = x^2 y^2$:
      \[
      \underline{x^2 y^2} \overset{g_1}{\longrightarrow} x y \text{ (terminal)}
      \]
      (where $\overset{g_i}{\longrightarrow}$ means that the move uses $g_i$)
      versus
      \[
      \underline{x^2 y^2} \overset{g_2}{\longrightarrow} x y \text{ (terminal)}.
      \]
      Looks good so far.
}
\only<3>{
\item Start the game with $f = x^3 y^3$:
      \[
      \underline{x^3 y^3} \overset{g_1}{\longrightarrow} \underline{x^2 y^2} \overset{g_1}{\longrightarrow} x y \text{ (terminal)}
      \]
      versus
      \[
      \underline{x^3 y^3} \overset{g_2}{\longrightarrow} \underline{x^2 y^2} \overset{g_1}{\longrightarrow} x y \text{ (terminal)}.
      \]
      Looks good so far.
}
\only<4>{
\item Not hard to see: This one is confluent.
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Example 2}

\begin{itemize}

\item \textbf{Example 2:}
      \begin{itemize}
      \item $n = 2$. Write $x$ and $y$ for $x_1$ and $x_2$.
      \item $k = 2$. Let $g_1 = {\blue x^2 y} - y$ and $g_2 = {\blue y^2 x} - x$.
      \end{itemize}

\only<2->{
\item Start the game with $f = x^2 y^2$:
      \[
      \underline{x^2 y^2} \overset{g_1}{\longrightarrow} y^2 \text{ (terminal)}
      \]
      versus
      \[
      \underline{x^2 y^2} \overset{g_2}{\longrightarrow} x^2 \text{ (terminal)}.
      \]
      \only<3>{
      Not confluent!}
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Example 3}

\begin{itemize}

\item \textbf{Example 3:}
      \begin{itemize}
      \item $n = 2$. Write $x$ and $y$ for $x_1$ and $x_2$.
      \item $k = 2$. Let $g_1 = {\blue x^2} - x - y$ and $g_2 = {\blue y^2} - x - y$.
      \end{itemize}

\only<2-3>{
\item Start the game with $f = x^2 y^2$:
      \begin{align*}
      \underline{x^2 y^2}
      &\overset{g_1}{\longrightarrow} \underline{x y^2} + y^3
      \overset{g_2}{\longrightarrow} x^2 + xy + \underline{y^3}
      \overset{g_2}{\longrightarrow} \underline{x^2} + 2xy + y^2
      \\
      &\overset{g_1}{\longrightarrow} x + y + 2xy + \underline{y^2}
      \overset{g_2}{\longrightarrow} 2x + 2y + 2xy
      \text{ (terminal)}
      \end{align*}
      versus
      \begin{align*}
      \underline{x^2 y^2}
      &\overset{g_2}{\longrightarrow} \underline{x^3} + x^2 y
      \overset{g_1}{\longrightarrow} x^2 + xy + \underline{x^2 y}
      \overset{g_1}{\longrightarrow} x^2 + 2xy + \underline{y^2}
      \\
      &\overset{g_2}{\longrightarrow} x + y + \underline{x^2} + 2xy
      \overset{g_1}{\longrightarrow} 2x + 2y + 2xy .
      \text{ (terminal)}
      \end{align*}
      \pause\pause
      Looks confluent so far. But how to prove it in general?
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Confluence criterion}

\begin{itemize}

\item Fix a commutative ring $\KK$, and finitely many monic polynomials $g_1, g_2, \ldots, g_k$
      in $\KK\ive{x_1, x_2, \ldots, x_n}$. \\
      For each $i$, let $\mathfrak{h}_i$ be the leading monomial of $g_i$.

\only<1>{
\item The multivariate polynomial division game:
      \begin{itemize}
      \item \textbf{Positions:} polynomials $f \in \KK\ive{x_1, x_2, \ldots, x_n}$.
      \item \textbf{Moves:} Pick any monomial $\mathfrak{m}$ that appears in $f$
            and any $i$ such that $\mathfrak{h}_i \mid \mathfrak{m}$.
            Call $c$ the coefficient of $\mathfrak{m}$ in $f$.
            Subtract $c \tup{\mathfrak{m} / \mathfrak{h}_i} g_i$ from $f$
            % Replace the term
            % \[
            % c \mathfrak{m} \text{ by } - c \tup{\mathfrak{m} / \mathfrak{h}_i} \tup{g_i - \mathfrak{h}_i}
            % \]
            % in $f$
            (that is, subtract the multiple of $g_i$ that kills the
            $\mathfrak{m}$-term in $f$ and leaves higher terms unchanged).
      \end{itemize}
}

\only<2->{
\item \textbf{Theorem (Buchberger).} The game is confluent if and only if for each
      $i$ and $j$, there is a position $t$ such that
      \[
       \xymatrix{
       & \operatorname{lcm}\tup{\mathfrak{h}_i, \mathfrak{h}_j} \ar_{g_i}[dl] \ar^{g_j}[dr] \\
        \arti[dr] & & \arti[dl]  \\
       & t
       }
      \]
      (where $\overset{g_i}{\longrightarrow}$ means ``move using $g_i$'', while
      $\overset{g_j}{\longrightarrow}$ means ``move using $g_j$'').
}
\only<3>{
\item It suffices to consider the case $i < j$.
}
\only<4>{
\item Again, the game can be modified so it no longer depends on the nonvanishing of coefficients.
      \\ The modified game has the same properties.
}

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Example 3 revisited}

\begin{itemize}

\item \textbf{Example 3:}
      \begin{itemize}
      \item $n = 2$. Write $x$ and $y$ for $x_1$ and $x_2$.
      \item $k = 2$. Let $g_1 = {\blue x^2} - x - y$ and $g_2 = {\blue y^2} - x - y$.
      \end{itemize}

\item Let us prove that this game is confluent. \pause \\
      $\lcm\tup{\mathfrak{h}_1, \mathfrak{h}_2} = x^2 y^2$. \pause \\
      We only need to consider the case $i < j$; thus $i = 1$ and $j = 2$. \\
      Thus we need to find $t$ such that
      \[
       \xymatrix{
       & x^2 y^2 \ar_{g_1}[dl] \ar^{g_2}[dr] \\
        \arti[dr] & & \arti[dl]  \\
       & t
       }
      \] \pause
      But we did that a few slides ago! ($t = 2x + 2y + 2xy$.)
      \\ So the game is confluent.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Buchberger 1}

\begin{itemize}

\item Actually, this holds more generally: \\
      \textbf{Theorem (Buchberger's 1st criterion).} If the monomials $\mathfrak{h}_i$ and $\mathfrak{h}_j$
      have no indeterminates in common (i.e., no variable appears in both;
      equivalently, $\lcm\tup{\mathfrak{h}_i, \mathfrak{h}_j} = \mathfrak{h}_i \mathfrak{h}_j$),
      then there is a position $t$ such that
      \[
       \xymatrix{
       & \operatorname{lcm}\tup{\mathfrak{h}_i, \mathfrak{h}_j} \ar_{g_i}[dl] \ar^{g_j}[dr] \\
        \arti[dr] & & \arti[dl]  \\
       & t
       }
      \] \pause

\item Thus, for example, the game is always confluent if
      $\mathfrak{h}_i = x_i^{\text{something}}$ for each $i$.

\end{itemize}

\vspace{9cm}

\end{frame}

\begin{frame}
\fti{Multivariate polynomial division, the game: Gr\"obner bases}

\begin{itemize}

\item Fix a commutative ring $\KK$, and finitely many monic polynomials $g_1, g_2, \ldots, g_k$
      in $\KK\ive{x_1, x_2, \ldots, x_n}$. \\
      For each $i$, let $\mathfrak{h}_i$ be the leading monomial of $g_i$.

\only<2->{
\item When the game is confluent, the polynomials $g_1, g_2, \ldots, g_k$ are said to form a
      \textit{Gr\"obner basis}. \\
      The terminal position obtained in the game is then called the
      \textit{remainder of $f$ upon division by $g_1, g_2, \ldots, g_k$}.
}
\only<3->{
\item Gr\"obner bases are often defined with respect to other orders (not just the lexicographic one).
      \\ The theory is then similar.
}
\only<4->{
\item Used throughout computational algebraic geometry and beyond.
}
\only<5>{
\item There is a noncommutative version, where monomials are replaced by \textit{words}
      (and the indeterminates don't commute).
}

\end{itemize}

\vspace{9cm}

\end{frame}

\end{document}

\begin{frame}
\fti{TODO}

\begin{itemize}

\item Finish these slides:
      \begin{itemize}
      \item Application: Zeckendorf family identities.
      \item Application: Bender-Knuth involutions for reverse plane partitions.
      \item Application: jeu de taquin.
      \item Application: numbers game?
      \end{itemize}
      %\item {\red \href{https://arxiv.org/src/1509.03803v2/anc/groth1alt.pdf}{Galashin/Grinberg/Liu, arXiv:1509.03803v2 ancillary file}}.
%\item {\red \href{http://www.cip.ifi.lmu.de/~grinberg/zeckendorfLONG.pdf}{Grinberg, \textit{Zeckendorf family identities generalized}}} (not the proof shown below; that one hasn't been written up).
%\item {\red \href{https://www.irif.fr/~krivine/articles/Lambda.pdf}{Krivine, \textit{Lambda-calculus: types and models}}}, Section 1.3 (we won't show this one).


\end{itemize}

\vspace{9cm}

\end{frame}

\end{document}

