← Games as recursive coalgebras: A categorical view on the Nim-sum

Olderversion__Submission20240503__main20240503.tex

\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{array}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
% \addbibresource{biblio.bib}
\addbibresource{CommonBiblio.bib}
\addbibresource{GamesAsWellFoundedCoalgebras.bib}
\tikzset{pullback/.style={minimum size=1.2ex,path picture={
\draw[opacity=1,black,-,#1] (-0.5ex,-0.5ex) -- (0.5ex,-0.5ex) -- (0.5ex,0.5ex);%
}}}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{todo}[theorem]{Todo}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}

\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{idea}[theorem]{Idea}

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\invmemo}[1]{\textcolor{blue}{memo: #1}}
\newcommand{\para}[1]{\paragraph{\textbf{#1}}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Func}[2]{[#1,#2]}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\demph}[1]{\textbf{#1}}
\newcommand{\ob}{\mathrm{ob}}


\newcommand{\X}{\mathbb{X}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\W}{\mathbb{W}}
\newcommand{\gS}{\mathbb{S}}
\newcommand{\A}{\mathbb{A}}
\newcommand{\I}{\mathbb{I}}
\newcommand{\Pf}{\mathcal{P}_{\mathrm{fin}}}
\newcommand{\Gs}{\mathbf{Games}}
\newcommand{\nsum}{\oplus}
\newcommand{\Alg}[1]{\mathbf{Alg}_{#1}}
\newcommand{\Coalg}[1]{\mathbf{Coalg}_{#1}}
\newcommand{\RecCoalg}[1]{\mathbf{RecCoalg}_{#1}}
\newcommand{\PfAlg}{\Alg{\Pf}}
\newcommand{\PfCoalg}{\Coalg{\Pf}}
% \newcommand{\mex}[1]{\mathrm{mex}(#1)}
\newcommand{\mex}{\mathrm{mex}}
\newcommand{\xem}{\mathrm{xem}}
\newcommand{\hylo}{\mathrm{hylo}}
% \newcommand{\G}[2]{\mathcal{G}_{#1}(#2)}
\newcommand{\G}{\mathcal{G}}
\newcommand{\rel}{\to}
\newcommand{\red}{\mathrm{red}}
\newcommand{\cp}{\ast}
\newcommand{\acc}{\rightsquigarrow}
\newcommand{\str}{\theta}
\newcommand{\Image}{\mathrm{Im}}
\newcommand{\HF}{\mathbb{HF}}
\newcommand{\Nim}[1]{\mathrm{Nim}_{#1}}
\renewcommand{\H}{\mathbb{H}}
\newcommand{\epi}{twoheadrightarrow}
\newcommand{\mono}{rightarrowtail}
\newcommand{\RB}{\mathcal{R}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\rd}{\mathrm{rd}}
\newcommand{\ADJ}[4]
    {
    \begin{tikzcd}[ampersand replacement = \&, column sep = small]
        {#1}
        \ar[rr, shift right=1.3ex, "{#2}"']
        \&\perp\&
        {#3}
        \ar[ll, shift right=1.3ex,"{#4}"']
    \end{tikzcd}
    }
\DeclarePairedDelimiter{\gen}{\langle}{\rangle}

\title{Games as recursive coalgebras\\ A categorical derivation and generalization of Nim-sum}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo}}
% \date{\today}
\subjclass[2020]{MSC}
\keywords{Keywords}


\begin{document}
\begin{abstract}
    
\end{abstract}
\maketitle
\tableofcontents
\section{Introduction}

\subsection{Context in combinatorial game theory}
\subsection{Context in category theory}
\subsection{Context in Logics and computer science}
\cite{riehl2019elephant}

\textbf{Acknowledgement}
\subsection{Conway's appendix}
Throughout this paper, $\N$ denotes the set of all non-negative integers $\N = \{0,1,2, \dots\}$.

%\newpage
\section{Games as graphs}
In this section, we recall \dq{classical} game-theoretic notions and phenomena, which will be reinterpreted and generalized later. \memo{See \cite{siegel2013combinatorial} for details.}

\subsection{Elementary definition of Games}
There are so many different definitions of impartial games. \memo{add bib} In this paper, we adopt a graph-theoretic one. Informally speaking, a vertex is a state of the game, and an edge is a possible move.
\begin{definition}[(impartial) games]\label{DefinitionGames}
    A \emph{game} $\X$ is a pair $\X = (X, \rel)$ of a (possibly infinite) set $X$ and a relation $\rel\subset X \times X$ that satisfies two finiteness conditions:
    \begin{enumerate}
        \item (finite options) For any $x \in X$, the number of options $\# \{x' \in X \mid x\rel x'\}$ is finite.
        \item (finite time) There is no infinite path. $x_0 \rel x_1 \rel x_2 \rel \dots$
    \end{enumerate}
\end{definition}

To win a given game, we need to know \dq{$N$-states} (Next-player-winning states) and \dq{$P$-states} (Previous-player-winning states), defined as follows. The following definition is not circuler, due to the \dq{finite time} condition.
% its winning states and losing states.
\begin{definition}[Outcome]\label{DefinitionOutcome}
    For a game $\X=(X, \rel)$ and its state $x\in X$,
    the outcome of $x$ is
    \[
    \begin{cases}
        N& \text{(if there exists $x\rel x'$ whose outcome is $P$.)}\\
        P& \text{(otherwise)}
    \end{cases}
    \]
\end{definition}

We end this subsection by giving several famous examples of combinatorial games.

\begin{example}[Nim]\label{ExampleNim}
    Let $\Nim{n}$ denote a nim game with $n$-heaps. In our formulation, it is $(\N^{n}, \rel)$, where $(a_1, \dots a_n)\rel (b_1, \dots b_n)$ if and only if there exists $1\leq i \leq n$ such that $a_i > b_i$ and for any $j \neq i$, $a_j = b_j$.
\end{example}

\begin{theorem}[Bouton's theorem]
    
\end{theorem}

\begin{example}[Subtraction Game]\label{ExampleSubtractionGame}
\memo{Write!}
\end{example}

\begin{example}[Wythoff]\label{ExampleWythoff}
\memo{Write!}
\end{example}

The next example is not well-known (at least in the following form), but will turn out to be theoretically important and is worth being called \emph{the universal game}.
\begin{example}[The terminal game: Binary exponent nim]\label{ExampleTheUniversalGameInTermsOfNumbers}
% The underlying set of the universal game is g
% \end{example}
% \begin{remark}[The universal game of natural numbers]
    % Since the terminal object is defined by universality, it is unique up to canonical isomorphism. Another description of the terminal object is given by \emph{Ackerman's interpretation} of hereditarily finite sets. \memo{ref}
    The underlying set of the binary exponent nim is $\N$, and the relation $n \rel m$ is defined by
    \[n \rel m \iff 2^m \text{ appears in the binary expansion of }n.\]
    For example, when $n=10000$, since
    \[
    n=10000=2^{13}+2^{10}+2^{9}+2^{8}+2^{4},
    \]
    there are $5$ possible moves, namely $10000\rel4,8,9,10,13$.
    The state $n=10000$ is $N$-state, because the next player can move to $8$, then the other player has no choice other than moving to $3$, and the last move $3\to 0$ terminates the game. 

    Later, we will observe that this game is universal, in the following senses:
    \begin{itemize}
        \item This game is the terminal object of the category of games.
        % $\Gs$.
        \item This is the universal \dq{recursively defined data} of games
        \item Every state of every game is canonically \dq{equivalent} to the unique state (i.e., natural number) of this game.
    \end{itemize}
    \memo{write the game!}
    
    \memo{"almost all states are N-state"}

    \memo{Is it related to the product-exp description of games?}
\end{example}

\begin{example}[The universal game: Hereditarily finite sets]\label{ExampleHereditarilyFiniteSets}
    
\end{example}

\begin{definition}[Birthday]
    
\end{definition}

\subsection{Game addition and Grundy number}

\begin{definition}[mex]
    For a finite set of natural numbers $S\subset \N$, $\mex(S)$ is the minimum natural number that does not belong to the subset $S$. In other words, mex of $S$ is the minimum element of the complement of $S$:
\[\mex(S) = \min S^{\mathrm{c}}.\]
\end{definition}

\begin{definition}[Grundy number]
    For a game $\X = (X, \rel)$ and a state $x\in X$, \emph{Grundy number} $\G_{\X}(x)$ is recursively defined as
\[\G_{\X}(x)=\mex(\{\G_{\X}(x')\mid x \rel x'\}).\]
\end{definition}
This recursive definition does work because of the finiteness conditions in the definition of games.

The importance of Grundy number is due to the following proposition.
\begin{proposition}
    The P-player (Previous player) wins the game $\X$ with the initial state  $x\in X$ if and only if $\G_{\X}(x) = 0$.
\end{proposition}
\begin{proof}
\memo{add bib}
\end{proof}

% Moreover, Grundy number is compatible with the \emph{addition of games}.
Next, we introduce the notion of the sum game. It is conventionally called sum and denoted by $\X + \Y$, but in this paper, we prefer the tensor symbol $\X\otimes \Y$.
\begin{definition}[Addition of games]
For two games $\X = (X,\rel_{\X}), \Y = (Y,\rel_{\Y})$, their \emph{sum} $\X \otimes \Y$ is a game $(X\times Y, \rel_{\X \otimes \Y})$, where $(x,y) \rel_{\X \otimes \Y} (x',y')$ if and only if 
$(x \rel_{\X} x' \land y=y')$ or $(x=x' \land y \rel_{\Y}y')$.
\end{definition}
\memo{This is called \dq{box product} in graph theory. \cite{kapulkin2023closed}}
\begin{example}
    The $n$-heaps nim game is the sum of $n$-copies of ($1$-heap) nim games.\[\Nim{n} = \Nim{1} \otimes \dots \otimes \Nim{1}\]
\end{example}

There is a well-known way to calculate the Grundy number of a state of a sum game: nim-sum.

\begin{definition}[Nim-sum]
    \emph{Nim-sum} is the abelian group structure on $\N$, induced by the bijection $\N \to \bigoplus_{k=0}^{\infty} \Z/2\Z$ given by the binary expansion . In other words, nim-sum is the digit-wise exclusive disjunction (xor) of the binary expansion.
\end{definition}
For example, $7\nsum 5 = (111)_{2} \nsum (101)_{2} = (010)_{2} = 2$.

The following famous proposition is not due to me. For a proof, see \memo{add bib}
\begin{theorem}[Nim-sum rule= generalized Bouton's theorem \memo{citation}]\label{theoremNimSumRule}
    For two games $\X = (X,\rel_{\X}), \Y = (Y,\rel_{\Y})$ and states $x\in X, y\in Y$, the Grundy number of $(x,y)$ is given by Nim-sum:
    \[\G_{\X\otimes\Y}(x,y)= \G_{\X}(x)\nsum\G_{\Y}(y).\]
\end{theorem}
Combining two propositions above, we can deduce a winning states of a sum game.
\begin{example}[Analysis of nim]\label{ExampleAnalysisOfNim}
    For example, we can deduce a winning strategy of $n$-heap nim $\Nim{n}$, which is a sum of $n$-copy of $\Nim{1}$.
    \memo{Write}
\end{example}


% \section{Category of games}\label{SectionCategoryOfGames}
\subsection{Category of games}\label{SubSectionCategoryOfGames}
    In this subsection, we will define the category of games, which will be rephrased in category-theoretic terminology in the latter part of this paper.

    A naive idea of \emph{game morphisms} might be functions that preserve the transition relation. In other words, a game morphism from $\X$ to $\Y$ might be guessed to be a function $X \to Y$ such that, if $x\rel_{\X} x'$ then $f(x) \rel_{\Y} f(x')$.

    However, for several reasons, we will not adopt that naive definition. One intuitive reason is that they preserve only \dq{graph-theoretic data} and do not preserve \dq{game-theoretic data}. For example, such a \dq{graph-theoretic} function might send a $P$-state to an $N$-state and does not preserve the Grundy number and the birthday of games.
    \memo{Write a sketch}

    Modifying such a problematic point, we define the notion of game morphism utilizing the \dq{path-lifting property}:
    \begin{definition}[Game morphism]\label{DefinitionGameMorphism}
        A \emph{game morphism} from a game $\X = (X, \rel_{\X})$ to $\Y = (Y, \rel_{\Y})$ is a function $f\colon X \to Y$ such that
        \begin{description}
            \item[Graph morphism] if $x\rel_{\X} x'$ then $f(x) \rel_{\Y} f(x')$. \label{ConditionGraphpreserving}
            \item[Path-lifting] if $f(x) \rel_{\Y} y$, then there exists $x' \in \X$ such that $x\rel_{\X}x'$ and $f(x')= y$. \label{conditionLocallySurjective}
        \end{description}
    \end{definition}

Later, we will see that this notion of game morphisms coincides with the notion of coalgebra homomorphisms \memo{ref}, and that game morphisms preserve all \dq{recursively defined data} of games, including ending states, outcomes, Grundy numbers, and birthdays.

\begin{notation}\label{NotationCategoryOfGames}
    The category of games and game morphisms is denoted by $\Gs$, and the canonical forgetful functor is denoted by $U \colon \Gs \to \Set$.
\end{notation}

\begin{remark}[Categorical properties of the category of games]
How well does the category of games behave categorically? Investigating the categorical properties of the category of games is not the main topic of this paper, but here I will list some facts.
\begin{itemize}
    \item The category of games $\Gs$ is locally finitely presentable. In particular, it has all small limits and small colimits.
    \item  The category of games $\Gs$ has a subobject classifier.
    \item The category of games $\Gs$ is not cartesian closed.
\end{itemize}
\end{remark}


\section{Games as recursive coalgebras}

\subsection{Coalgebras and recursive coalgebras}\label{subsectionCoalgebraicMethod}
% \subsection{Coalgebras of an endofuntors}
\begin{definition}[Coalgebras and algebras]\label{DefinitionCoalgebra}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a \demph{$T$-coalgebra} is a pair of an object $X \in \ob(\C)$ and a morphism $\str \colon X \to TX$. A \demph{$T$-algebra} is a pair of an object $X \in \ob(\C)$ and a morphism $\alpha \colon TX \to X$.
\end{definition}

\begin{definition}[Coalgebra homomorphism and algebra homomorphism]
\label{DefinitionCoalgebraMorphism}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a homomorphism of $T$-coalgebras from $(X, \str)$ to $(X',\str')$ is a morphism $f\colon X \to X'$ in $\C$ such that 
    \[
    \begin{tikzcd}
        X\ar[r,"f"]\ar[d,"\str"]&X'\ar[d,"\str'"]\\
        TX\ar[r,"Tf"]&TX'
    \end{tikzcd}
    \]
    commutes. Homomorohisms between $T$-algebras are similarly defined.
\end{definition}

\begin{notation}\label{NotationCoalg}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, the category of $T$-coalgebras and $T$-coalgebra homomorphisms is denoted by $\Coalg{T}$. The category of $T$-algebras and $T$-algebra homomorphisms is denoted by $\Alg{T}$.
\end{notation}

\begin{definition}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a \demph{coalgebra-algebra morphism} from a $T$-coalgebra $(X, \str)$  to  a $T$-algebra $(A,\alpha)$ is a morphism $f\colon X\to A$ in the category $\C$ such that the diagram
    \[
    \begin{tikzcd}
        X\ar[d,"\str"]\ar[r,"f"]&A\\
        TX\ar[r,"Tf"]&TA\ar[u,"\alpha"']
    \end{tikzcd}
    \]
    commutes.
\end{definition}

\begin{definition}
    A $T$-coalgebra $\X=(X,\str)$ is a \demph{recursive coalgebra} if for any $T$-alegebra $\A=(A,\alpha)$, there is a unique coalgebra-algebra morphism $\X\to \A$. The full subcategory of $\Coalg{T}$ that consists of all recursive coalgebras is denoted by $\RecCoalg{T}$.

    For recursive coalgebra $\X=(X, \theta)$ and a $T$-algebra $\A=(A, \alpha)$, the unique coalgebra-algebra morphism $X\to A$ is called the \demph{hylomorphism} and denoted by $\hylo_{\A, \X}\colon X \to A$.
\end{definition}

\begin{remark}
\cite{taylor1999practical}
For now, see \href{https://ncatlab.org/nlab/show/recursion+scheme}{[recursion scheme]} in nLab.
For the relationship with well-founded coalgebra, see the recent study \cite{adamek2020well} by Adamek, Milius, and Moss.
\end{remark}

\begin{proposition}[\memo{Labek+ Taylor}]\label{PropositionTerminalRecursiveCoalgebra}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, if a $T$-algebra $\A=(A,\alpha)$ is the initial $T$-algebra, then
    \begin{itemize}
        \item the structure map $\alpha \colon TA \to A$ is an isomorphism, and
        \item the coalgebra $(A, \alpha^{-1}\colon A \to TA)$ is the terminal recursive coalgebra.
    \end{itemize}
\end{proposition}
\begin{proof}
    The first assertion is known as Lambek's lemma. The second assertion immediately follows from the related definitions.
\end{proof}




\subsection{Games as recursive coalgebras}
\begin{definition}[finite powerset functor]\label{DefinitionPf}
    The finite powerset functor $\Pf:\Set \to \Set$ is the subfunctor of the covariant powerset functor $\mathcal{P}:\Set \to \Set$ such that 
    $\Pf(X) = \{S \subset X\mid \# S < \infty\}$.
\end{definition}

\begin{theorem}
    The category of games is equivalent to the category of recursive $\Pf$-coalgebras.
    \[
    \Gs\simeq \RecCoalg{\Pf}
    \]
\end{theorem}
\begin{proof}
    % Notice that our formulation of games is a special case of $\Pf$-coalgebra.
For a game $\X = (X,\rel)$, we can define a structure map $\str:X \to \Pf(X)$ by $ x \mapsto \str (x) \coloneq \{x'\in X\mid x\rel x'\}$. The \dq{finite options} condition in the definition of games ensures the finiteness of $\str(x)$.

This correspondence defines a fully faithful functor $\Gs \to \Coalg{\Pf}$. This follows since a function $f\colon X \to X'$ is a $\Pf$-coalgebra homomorphism if and only if $f(\str(x))=\str'(f(x))$. The inclusion relation $f(\str(x))\subset \str'(f(x))$ is equivalent to the \dq{Graph morphism condition}, and the other inclusion relation $f(\str(x))\supset \str'(f(x))$ is equivalent to the \dq{Path-lifting condition}.

To prove the essential image of the fully faithful functor is the full subcategory of recursive coalgebras, it suffices to see that a $\Pf$-coalgebra $(X,\str)$ is recursive if and only if the corresponding graph satisfies the \dq{finite time} condition. If the graph satisfies the finite time condition, we can resursively construct the unique coalgebra-algebra morphism, and prove that it is recurisive coalgebra. Conversely, suppose a coalgebra $\X= (X,\str)$ is a recursive coalgebra. Define a $T$-algebra $\A=(\N,\xem)$ by
\[
\xem(S) \coloneq \min\{n \in \N\mid \text{for any }m\in S, m<n\},
\]
and consider the hylomorphism $\hylo_{\A,\X}\colon X \to N$. If $x\to x'$, then we can prove that $\hylo_{\A,\X}(x)>\hylo_{\A,\X}(x')$. By the well-foundedness of the poset $(\N,<)$, this proves that thecorresponding graph of the coalgebra $\X=(X, \str)$ satisfies the finite time condition, thus is a game.
\end{proof}

\begin{remark}
    \cite{adamek2020well}
\end{remark}



\begin{example}[Nim is von Neumann's natural numbers!]\label{ExampleNimCoalgebra}
    Let $(\N, \nu:\N \to \Pf(\N))$ denote the 
    $\Pf$-coalgebra corresponding to the ($1$-heap) nim game $\Nim{1}=(\N, >)$. This function $\nu$ is given by 
    \[\nu:\N \to \Pf(\N): n \mapsto \{0,1, \dots, n-1\}.\]
    In other words, this is von Neumann's set-theoretic definition of natural numbers.
    % \memo{
    % }
\end{example}

Such an appearance of a set-theoretic construction is 
    % kind of necessary. Because both the initial algebra and the terminal game are the set-theoretic object $\H$, 
    % the set of all hereditarily finite sets, and 
    due to the fact that the nim game is the subgame of the terminal game, which we will investigate in the next subsection.
    See next subsection.

\subsection{The terminal game}
\memo{ask refs}
% With the category-theoretic terminology, we can conduct universal costructions of games! The first, and

Possibly the most important game is, the terminal object of $\Gs$. This subsection aims to descrbe the terminal game.
First, we define hereditarily finite sets, by recursion.
\begin{definition}[Hereditarily finite sets]
A \emph{hereditarily finite set} is recursively defined as a finite set of hereditarily finite sets\footnote{Rigorously speaking, a hereditarily finite set is a set that is ensured to be hereditarily finite by this recursive definition.} .
     % A set $A$ is \emph{hereditarily finite} if all elements of $A$ are hereditarily finite.
     The set of all hereditarily finite sets is denoted by $\H$.
\end{definition}

This recursive definition might look confusing. We give several examples of hereditarily finite sets.
\begin{example}\label{LabelExampleHereditarilyFiniteSets}
The following sets are hereditarily finite sets:
\begin{itemize}
    \item The empty set $\emptyset$ is trivially hereditarily finite since it has no element.
    \item Therefore, the set $\{\emptyset\}$ is also hereditarily finite. 
    \item By induction, every (von Neumann's formulation of) natural number $n=\{0,1, \dots n-1\}$ is hereditarily finite. In other words, 
    \[\N = \{0=\emptyset,\ 1=  \{\emptyset\},\ 2= \{\emptyset,\{\emptyset\}\},\ 3=\{\emptyset,  \{\emptyset\}, \{\emptyset,\{\emptyset\}\}\}, \dots\} \subset \H.\] 
    \item The set $\{\{\emptyset\}\}$ is a hereditarily finite set that is not a natural number.
\end{itemize}
\end{example}

Notice that, by definition, $\Pf(\H)$ is set-theoretically equal to $\H$. Therefore, $\H$ admits the canonical $\Pf$-algebra structure \[\id_{\H}:\H \to \Pf(\H)\] and $\Pf$-coalgebra structure \[\id_{\H}:\Pf(\H) \to \H.\]

\begin{proposition}\label{PropositionInitialAlgebraIsHereditarilyFiniteSets}
The $\Pf$-algebra $\H$ is the initial $\Pf$-algebra.
\end{proposition}
\begin{proof}
    Since $\Pf$ preserves filtered colimits, we can utilize Adamek's construction of the initial algebra (\memo{cite}). Since the set $\H$ is the colimit of
    \[
        \begin{tikzcd}
            \emptyset \ar[r]& \Pf(\emptyset) \ar[r]& \Pf(\Pf(\emptyset)) \ar[r]&\Pf(\Pf(\Pf(\emptyset))) \ar[r]&\cdots \H,
        \end{tikzcd}
    \]
    this completes the proof.
\end{proof}

\begin{definition}[Terminal game]\label{DefinitionUniversalGame}
    The \demph{terminal game} $\H=(\H,\to)$ is a game whose underlying set is the set of all hereditrily finite set $\H$ and whose relation $\rel$ is defined by 
    \[A \rel B \iff B \in A.\]
\end{definition}

\begin{proposition}\label{PropositionUniversalIsTerminal}
    The terminal game $\H$ is the terminal object of $\Gs$.
\end{proposition}
\begin{proof}
    This is due to Proposition \ref{PropositionTerminalRecursiveCoalgebra} and Proposition \ref{PropositionInitialAlgebraIsHereditarilyFiniteSets}.
    % , it is enough to prove that $\H$ is the initial $T$-algebra.
\end{proof}

\begin{remark}[Ackerman's interpretation]
There is another way to describe the terminal game, using natural numbers $\N$ instead of hereditarily finite sets $\H$. Consider a $\Pf$-algebra structure on $\N$ defined by
 % One canonical choice of such bijection is
    \[b: \Pf(\N)\to \N \colon S \mapsto \sum_{s\in S} 2^s.\]
    % on the set of natural numbers $\N$.
    It is simply a binary expression and hence bijective.
% Throughout this paper, $\H = \Pf(\H) $ is the crucial fact. But is it necessary to consider $\H$? Just by considering the cardinality, we should be able to consider a bijection between $\N$ and $\Pf(\N)$ as well!
    % since they are both countable sets.
    The unique $\Pf$-algebra morphism $\mathrm{Ack}\colon\H \to \N$ is called \emph{Ackerman's interpretation} \cite{ackermann1937widerspruchsfreiheit} and known to be bijective.
    % In fact, $\mathrm{Ack}$ gives an isomorphism between them as $\Pf$-algebras and $\Pf$-coalgebras (or, games).
    Consequently, this $T$-algebra $(\N,b)$ is also an initial object in $\Alg{\Pf}$, and hence also gives the terminal object in $\Gs \simeq \RecCoalg{\Pf}$. This is what we called the binary exponent nim in Example \ref{ExampleTheUniversalGameInTermsOfNumbers}.
\end{remark}

\begin{notation}
    For a game $\X$, the unique game morphism to $\H$ is denoted by $\rd_{\X}\colon \X \to \H$.
\end{notation}

\begin{proposition}
    For a game $\X$ and a $\Pf$-algebra $\A=(A, \alpha)$, the hylomorphism $\hylo_{\A,\X}\colon \X \to \A$ is decomposed into 
    \[
    \begin{tikzcd}
    X \ar[r,"\rd_{\X}"] \ar[rr,"\hylo_{\A,\X}"', bend right] & \H\ar[r,"\hylo_{\A, \H}"] & A
    \end{tikzcd}
    \]
\end{proposition}

\begin{remark}[Two definitions of combinatorial games]\label{RemarkTwoDefinitionsOfCombinatorialGames}
\end{remark}



\subsection{Recursively defined values are hylomorphisms}

\begin{definition}
    A \demph{game evaluation} to a set $A$ is a family of functions
    \[
    \{v_{\X}\colon X\to A\}_{\X=(X, \str)\text{: game}}.
    \]
    from all games to the set $A$.
    A game evaluation is \demph{recursively defined} if there exists a $\Pf$-algebra $\A=(A, \alpha)$ such that for any game $\X$, the  function $v_{\X}$ is equal to the corresponding hylomorphism $\hylo_{\A, \X}\colon X \to A$.
\end{definition}

\begin{example}
    Grundy number $\{\G_{\X}\colon X \to \N\}$ is recursively defined by the $\Pf$-algebra $(\N, \mex\colon \Pf(\N) \to \N)$.
\end{example}

\begin{example}
    Outcome $\{X \to \{N,P\}\}$ is recursively defined by the $\Pf$-algebra $(\{N,P\}, o)$, where
    \[
    o\colon \Pf(\{N,P\})\to \{N,P\}\colon S \mapsto 
    \begin{cases}
        P &(P \notin S)\\
        N &(P\in S).
    \end{cases}
    \]
\end{example}

\begin{remark}
    There is a $\Pf$-algebra homomorphism from $(\N,\mex)$ to $(\{N,P\}, o)$. This proves the proposition \memo{cite}.
\end{remark}

\begin{example}
    Birthday $\{b_{\X}\colon X \to \N\}$ is recursively defined by the $\Pf$-algebra $(\N,\xem)$
    \[
    \xem \colon \Pf(\N)\to \N\}\colon S \mapsto \min\{n \in \N\mid \text{for any }m\in S, m<n\}
    \]
\end{example}

% \begin{example}[outcome]
% The outcome function $\{X \to \{\}\}$
% \end{example}

In summary, we obtain the following proposition:
\begin{proposition}
Grundy number, outcome, and birthday are recursively defined.
\end{proposition}
% \begin{proof}
%     Grundy number $\{\G \X\to \N\}$
% \end{proof}


\begin{table}
    \centering
    \begin{tabular}{|c|c|} \hline 
         Recursively defined game evaluation&  $\Pf$-algebra\\ \hline 
         outcome&  $(\{N,P\}, o)$\\ \hline 
         misere outcome&  $(\{N,P\},\mu)$\\ \hline 
         remoteness&  $(\N, \rho)$\\ \hline 
         Grundy number&  $(\N,\mex)$\\ \hline
 Birthday& $(\N,\xem)$\\\hline
    \end{tabular}
    \caption{Game evaluations and $\Pf$-algebras}
    \label{TableGameEvaluations}
\end{table}

\begin{corollary}
    A game morphism preserves all recursively defined game evaluations. In particular, a game morphism preserves
    \begin{itemize}
        \item Grundy number
        \item outcome
        \item misere outcome
        \item birthday
        \item remoteness
    \end{itemize}
\end{corollary}

There are a lot of other examples:
\begin{example}[Ended]
    
\end{example}

\begin{example}
    In combinatorial game theory, a \demph{misere game} is a game, where the player who takes the last move loses. For misere games, the notion of outcome should be modified so that the ending state is a $N$-state.
    Defining a $\Pf$-algebra $(\{N,P\},\mu)$ by
    \[
     \mu \colon \Pf(\{N,P\})\to \{N,P\}\colon S \mapsto 
    \begin{cases}
        P &(S=\{N\})\\
        N &(S\neq \{N\}),
    \end{cases}
    \]
    the corresponding game evaluation is the \demph{misere outcome}. 
\end{example}

\begin{example}[remoteness]
    
\end{example}

\begin{remark}[Grundy number and Birthday are dual]
    
\end{remark}



\section{Application: Nim-sum type theorem schema}
This section aims to provide a theorem schamea that generarizes the nim-sum rule \ref{theoremNimSumRule}.

\subsection{Raw bouton monoid}
\begin{proposition}
    For a monoidal category $(\C, I, \otimes)$ with a terminal object $1$, the object $1$ has a unique monoid structure with respect to the monoidal structure.
\end{proposition}
\begin{proof}
    All structural maps, $\eta\colon I \to 1$ and $\mu\colon 1\otimes 1 \to 1$, are uniquely determined. All needed commutattivities are trivial since $1$ is the terminal object. 
\end{proof}

We will utilize the following well-known fact.
\begin{proposition}[Well-known]
    A lax monoidal functor $F\colon (\C, I_{\C}, \otimes_{\C})\to (\D,I_{\D},\otimes_{\D} )$ sends a monoid object in $\C$ to a monoid object in $\D$.
\end{proposition}

\begin{definition}We adopt the following terminologies:
\begin{itemize}
    \item For a monoidal category $(\C, I_{\C}, \otimes_{\C})$ with a terminal object $1$, the \demph{terminal monoid} is the unique monoid object whose underlying object is $1$, which is the terminal object of the category of monoid objects.
    \item For a lax monoidal functor $F\colon (\C, I_{\C}, \otimes_{\C})\to (\D,I_{\D},\otimes_{\D})$, the \demph{$F$-terminal monoid} is the monoid object in $\D$, obtained by sending the terminal monoid of $\C$ by the functor $F$.
\end{itemize}
\end{definition}

\begin{example}
    The terminal monoid in $(\C, I_{\C}, \otimes_{\C})$ is $\id_{\C}$-terminal monoid.
\end{example}

\begin{example}
    For the free abelian group functor $F\colon \Set\to \mathbf{Ab}$, the $F$-terminal monoid is the ring of integers $\Z$.
\end{example}

% \begin{remark}
%     In fact, the terminal monoid is the terminal object of the category of monoid objects in $(\C, I_{\C}, \otimes_{\C})$.
% \end{remark}

% For many lax monoidal functors, the $F$-monoid is tirivial. For example, the forgetful functor 

\begin{definition}
    For a monoidal structure $(\Gs, I, \ast)$ on the category of games $\Gs$ such that the forgetful functor $U \colon (\Gs, I, \ast) \to (\Set,1,\times)$ is lax monoidal, the \demph{raw bouton monoid} $\RB_{\ast}$ is the $U$-terminal monoid with respect to the monoidal structure $\ast$. 
    % The raw bouton monoid is denoted by $(\rB, \rm, \ru)$.
\end{definition}
The raw bouton monoid is a usual monoid (i.e., a monoid in $\Set$), and whose underlying set is $\H$ due to Proposition \ref{PropositionUniversalIsTerminal}.

% \begin{proposition}
%     For a monoidal structure $(\Gs, \ast, I)$ on the category of games $\Gs$ such that the forgetful functor $U \colon \Gs \to \Set$ is lax monoidal, the underlying set of $\RB_{\ast}$ is the set of hereditarily finite set $\H$. 
% \end{proposition}

\begin{notation}
    We adopt the following notation:
    \begin{itemize}
        \item The multiplication function of the raw bouton monoid $\RB_{\ast}$ is denoted by $\circledast \colon\H\times \H \to \H$. Notice that this multiplication function depends on the monoidal structure $\ast$.
        \item For two games $\X=(X,\rel_{\X})$ and $\Y=(Y,\rel_{\Y})$, the coherence map of the lax monoidal functor is denoted by $\mu_{\X,\Y}\colon X\times Y = U\X \times U\Y \to U(\X\ast \Y)$, and $\mu_{\X,\Y}(x,y)\in  U(\X\ast \Y)$ is simply denoted by $(x,y) \in  U(\X\ast \Y)$.
    \end{itemize}
\end{notation}

\begin{proposition}[Raw generalized nim-sum rule]
For two games $\X=(X,\rel_{\X})$ and $\Y=(Y,\rel_{\Y})$, we have the following equation in the raw bouton monoid $\RB_{\ast}$:
    \[
    \rd_{\X\ast\Y}(x,y) = \rd_{\X}(x) \circledast \rd_{\Y}(y).
    \]
\end{proposition}
\begin{proof}
    Since $\H$ is the terminal game, we have the following commutative diagram in $\Gs$:
    \[
    \begin{tikzcd}
        &\X\ast \Y\ar[rd,"\rd_{\X\ast \Y}"],\ar[d,"\rd_{\X}\ast \rd_{\Y}"']&\\
        &\H\ast\H\ar[r,"\rd_{\H\ast \H}"]&\H.
    \end{tikzcd}
    \]

    By sending this diagram by $U$ and utilizing the naturality of $\mu$, we have the following commutative diagram in $\Set$:
    \[
    \begin{tikzcd}
        X\times Y=U\X\times U\Y \ar[d,"U\rd_{\X}\times U\rd_{\Y}"']\ar[r,"\mu_{\X,\Y}"]&U(\X\ast \Y)\ar[rd,"U(\rd_{\X\ast \Y})"],\ar[d,"U(\rd_{\X}\ast \rd_{\Y})"']&\\
        \H \times \H=U\H \times U\H\ar[r,"\mu_{\H,\H}"]\ar[rr, bend right , "\circledast"']&U(\H\ast\H)\ar[r,"U(\rd_{\H\ast \H})"]&U(\H)=\H.
    \end{tikzcd}
    \]
    This proves the proposition.
\end{proof}

\subsection{Bouton monoid}


% In principle, the raw Bouton monoid $\RB_{\ast}$ contains sufficient information to analyze games by decomposition, but practically, it is too large to compute efficiently. Therefore, in order to calculate desired information about games (such as outcome), we define an appropriate size quotient monoid of the raw Bouton monoid.

In principle, the raw Bouton monoid $\RB_{\ast}$ contains sufficient information to decompose and analyze games, but practically, it is too large to compute. Therefore, by quotienting the monoid to the size necessary to calculate desired information about the game (such as outcome of games), a more practical \demph{Bouton monoid} will be defined in this subsection.

\begin{definition}[Minimum quotient monoid]
    For a monoid $M$, a set $S$ and a function $f\colon M \to S$, the \demph{minimum quotient monoid} of $f\colon M \to S$ is a surjective monoid homomorphism $q_f \colon M \twoheadrightarrow M_f$ such that
    \begin{enumerate}
        \item $f$ factors through $q_f$ (as a function). \label{ConditionSfactor}

        \item For an arbitrary surjective monoid homomorphism $q \colon M \to N$ such that $f$ factors thorough $q$,
        % satisfying condition (\ref{ConditionSfactor})
        there exists a function $r\colon N \to M_f$, (which is necessarily unique and is a surjective monoid homomorphism) such that $q_{f} = r\circ q$. \label{ConditionMinimum}

                \[
        \begin{tikzcd}
            M\ar[rr,"f"]\ar[rd,"q", two heads]\ar[rdd,"q_{f}"', two heads]&&S\\
            &N\ar[ru,dashed]\ar[d,"r", dashed]&\\
            &M_{f}\ar[ruu,dashed]&
        \end{tikzcd}
        \]
    \end{enumerate}
\end{definition}

\begin{proposition}[Unique existence]\label{PropositionUniqueExistenceOfUniversalQuotient}
    For a monoid $M$, a set $S$, and a function $f\colon M \to S$, the minimum quotient monoid of $f$ exists and is unique (up to a canonical isomorphism). Furthermore, the corresponding congruence relation $\sim_{f} \subset M\times M$ is given by
    \[
    m\sim_{f} m' \iff \text{for any }a,b\in M, f(amb)=f(am'b).
    \]
    That is, the quotient map $q_{f}\colon M\twoheadrightarrow M_{f}$ is (isomorphic to) the canonical surjection $M \twoheadrightarrow M/{\sim_{f}}$.
\end{proposition}
\begin{proof}
% The maximum quotient monoid is the quotient o
% % Since the maximum quotient monoid is the right adjoint of the embedding functor
% % \[
% % \text{(the complete latice of quotient monoids of $M$)}\to M/\Set,
% % \]
% % the proposition follows from the general adjoint functor theorem.
First, we need to prove the equivalence relation $\sim_f$ is a congruence relation. If $m\sim_f m'$ and $n\sim_f n'$, for any $a,b\in M$, we have
\[
f(amnb)= f(am'nb)=f(am'n'b),
\]
and thus $mn\sim_f m'n'$. This proves that $\sim_f$ is a congruence relation, and $q_f\colon M \to M_f \coloneqq M/{\sim_f}$ is a surjective monoid homomorphism.

In order to prove the condition \ref{ConditionSfactor}, we need to prove $m\sim_f m' \implies f(m) = f(m')$, and this immediately follows from the definition of $\sim_f$.

Lastly, we prove the condition \ref{ConditionMinimum}. We prove $q(m) = q(m') \implies m\sim_f m'$.  If $q(m) = q(m')$, then for any $a,b\in M$, we have $q(amb)=q(a)q(m)q(b)= q(a)q(m')q(b)=q(am'b)$, and $f(amb)=f(am'b)$, since $f$ factors through $q$. This proves that $q(m) = q(m') \implies m\sim_f m'$ and the condition \ref{ConditionMinimum}.
\end{proof}

\begin{remark}
    The construction of minimum quotient monoid is ubiquitous in combinatorial game theory. For example, even the \dq{equality} of games is conventionally defined in this way! See \cite{siegel2013combinatorial}.
\end{remark}

\begin{definition}[Bouton monoid]
For a monoidal structure $(\Gs,I, \ast)$ such that the forgetful functor $U\colon (\Gs,I,\ast) \to (\Set, 1,\times)$ is lax monoidal and a $\Pf$-algebra $\A=(A, \alpha)$, the \demph{Bouton monoid} $\B_{\ast, \A}$ is the minimum quotient monoid of a function 
\[
\begin{tikzcd}
    \RB_{\ast}= \H \ar[r,"\hylo_{\A,\H}"]& A.
\end{tikzcd}
\]
The canonical surjective monoid homomorphism from $\RB_{\ast}$ to $\B_{\ast,\A}$ is denoted by $q_{\ast, \A}\colon \RB_{\ast}\twoheadrightarrow \B_{\ast,\A}$.
% where $\RB_{\ast}$ is equipped with the raw Bouton monoid structure with respect to the monoidal structure $\ast$.
\end{definition}

\begin{notation}
    We adopt the following notations:
    \begin{itemize}
        \item For a game $\X=(X,\rel_{\X})$, the function
        \[
        \begin{tikzcd}
            X \ar[r,"\rd_{\X}"] & \RB_{\ast} \ar[r,"q_{\ast,\A}"] &\B_{\ast,\A}
        \end{tikzcd}
        \]
        is denoted by $\G_{\ast,\A}\colon \X \to \B_{\ast,\A}$.
    \end{itemize}
\end{notation}

\section{Remaining Questions}\label{SectionFutureWorks}
We believe that this paper is just a starting point of the theory of "Games as recursive coalgebras". There are still a lot of things to be calculated. We post some of the remaining questions in this appendix.

\subsection{Mathematically stated questions}
\begin{question}[The closed structure]
    What is the internal hom?
\end{question}

\begin{question}
    Are the bouton functions always recursively defined?
\end{question}
\subsection{Ambiguous (but ambitious) questions!}
\memo{It's quite natural to consider a multiplayer game, probability game, 2-turns/1-turn game, and other variants of games. And might be dealt with using some appropriate algebras. Furthermore, can we consider other graph data, like entropy?  I know there is a notion of the temperature of a game. Is it an example of this framework?}

\memo{By considering coalgebra-> algebra map (from now, we call it ca map) (or, profunctor Alg -> Coalg), we may able to discard $\H$ and discuss everything so far...(?) The canonical map may be the unique ca map, and a game (or well-foundedness) may be equivalent to the condition that for any algebra, there uniquely exists a ca map to it.}


Replacing $\Pf$ with other endofunctors to describe other types of game theory, like partisan, probabilistic, mis\`ere, transfinite, and loopy games.

\begin{question}
    Double cat
\end{question}
\begin{question}
    lpac
\end{question}
\begin{question}
    semantics
\end{question}

\begin{question}
    Is there a topos-theoretic analogy?
\end{question}

\begin{question}
    As a relative local state classifier.
\end{question}




\printbibliography

\end{document}