save progress on combinatorics

papers/icfp24/combinatorics.tex

@@ -1,7 +1,109 @@
 \section{Combinatorics}
 \label{sec:combinatorics}
 
-We denote free monoid on $A$ with $\LL(A)$ and free commutative monoid on $A$ with $\MM(A)$.
-$\MM(A + B) \eqv \MM(A) \times \MM(B)$.
+With universal properties we can structure our programs using ideas from algebra.
+For example $\term{length}$ is a common operation defined inductively for $\List$,
+but to state properties about $\term{length}$, e.g.
+$\term{length}(xs \doubleplus ys) = \term{length}(xs) + \term{length}(ys)$,
+we would need to prove them externally. With our framework we can define operations like $\term{length}$
+using the $\ext{(\blank)}$ operation, which would also give us a proof that they are homomorphisms for free.
+We can also use universal property to prove two different types are equal by showing they both
+satisfy the same universal property, which is desirable especially if proving a direct equivalence between
+the two types is very difficult.
+
+To illustrate this, we give some examples of how some common operations can be defined
+in terms of universal property.
+We use $\FF(A)$ to denote the free monoid or free commutative monoid on $A$.
+
+\subsection{Length}
+
+Any presentation of free monoids or free commutative monoids has a $\term{length} : \FF(A) \to \Nat$ function.
+$\Nat$ is a (commutative) monoid with $(0,+)$, so we can extend $\lambda x.\, 1\,:\,A \to \Nat$.
+This allows us to define $\term{length}$ for any construction of free (commutative) monoid, and also
+gives us a proof of $\term{length}$ being a homomorphism for free.
+
+\begin{figure}[H]
+    \centering
+    \begin{tikzcd}[ampersand replacement=\&,cramped]
+    	{\FF(A)} \&\& {(\mathbb{N}, 0, +)} \\
+    	\\
+    	A
+    	\arrow["\eta_A", from=3-1, to=1-1]
+    	\arrow["{\ext{(\lambda x. \, 1)}}", from=1-1, to=1-3]
+    	\arrow["{\lambda x. \, 1}"', from=3-1, to=1-3]
+    \end{tikzcd}
+    \caption{Definition of $\term{length}$ by universal property}
+    \label{fig:enter-label}
+\end{figure}
+
+
+\subsection{Membership}
+Any presentation of free monoids or free commutative monoids has a membership predicate:
+$\_\in\_ : A \to \FF(A) \to \hProp$. By fixing an element $x: A$, the element we want to define
+the membership proof for, and 
+assuming $A$ is a set, we can define $\yo_A(x) = \lambda y.\, x \id y : A \to \hProp$.
+Since $\hProp$ forms a (commutative) monoid under $\vee$,
+we can extend $\yo_A(x)$ to obtain $x \in \blank : \FF(A) \to \hProp$, giving us the membership predicate for $x$.
+
+\begin{figure}[H]
+    \centering
+    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXEZGKEEpIl0sWzIsMF0sWzAsMiwiQSJdLFszLDAsIihcXGhQcm9wLCBcXGJvdCwgXFx2ZWUpIl0sWzIsMCwiXFxldGFfQSJdLFswLDMsIih4IFxcaW4gXFxibGFuaykgLyBcXGV4dHtcXHlvX0EoeCl9Il0sWzIsMywiXFx5b19BKHgpIiwyXV0=
+    \begin{tikzcd}[ampersand replacement=\&,cramped]
+    	{\FF(A)} \&\& {} \& {(\hProp, \bot, \vee)} \\
+    	\\
+    	A
+    	\arrow["{\eta_A}", from=3-1, to=1-1]
+    	\arrow["{(x \in \blank) / \ext{\yo_A(x)}}", from=1-1, to=1-4]
+    	\arrow["{\yo_A(x)}"', from=3-1, to=1-4]
+    \end{tikzcd}
+    \caption{Definition of membership proof for $x$ by universal property}
+    \label{fig:enter-label}
+\end{figure}
+
+
+\subsection{Any and All predicate}
+
+Any presentation of free monoids or free commutative monoids $\FF(A)$ has the
+$\term{Any}$ and $\term{All}$ predicates, which allow us to lift a predicate $A \to \hProp$
+to any or all elements of $xs : \FF(A)$. We note that
+$\hProp$ forms a (commutative) monoid in two different ways: $(\bot,\vee)$ and $(\top,\wedge)$,
+therefore given a predicate $P : A \to \hProp$, we get:
+\begin{align*}
+    Any(P) &= \ext{P} : \FF(A) \to (\hProp, \bot, \vee) \\
+    All(P) &= \ext{P} : \FF(A) \to (\hProp, \top, \wedge)
+\end{align*}
+
+\begin{figure}[H]
+    \centering
+    \begin{minipage}[t]{0.49\textwidth}
+        \centering
+        \begin{tikzcd}[ampersand replacement=\&,cramped]
+        	{\FF(A)} \&\& {(\hProp, \top, \wedge)} \\
+        	\\
+        	A
+        	\arrow["\eta_A", from=3-1, to=1-1]
+        	\arrow["{\ext{P}}", from=1-1, to=1-3]
+        	\arrow["{P}"', from=3-1, to=1-3]
+        \end{tikzcd}
+        \caption{Definition of $\term{All}$ by universal property}
+        \label{fig:enter-label}
+    \end{minipage}
+    \begin{minipage}[t]{0.49\textwidth}
+        \centering
+        \begin{tikzcd}[ampersand replacement=\&,cramped]
+        	{\FF(A)} \&\& {(\hProp, \bot, \vee)} \\
+        	\\
+        	A
+        	\arrow["\eta_A", from=3-1, to=1-1]
+        	\arrow["{\ext{P}}", from=1-1, to=1-3]
+        	\arrow["{P}"', from=3-1, to=1-3]
+        \end{tikzcd}
+        \caption{Definition of $\term{Any}$ by universal property}
+        \label{fig:enter-label}
+    \end{minipage}
+\end{figure}
+
+% We denote free monoid on $A$ with $\LL(A)$ and free commutative monoid on $A$ with $\MM(A)$.
+% $\MM(A + B) \eqv \MM(A) \times \MM(B)$.
 
 

papers/icfp24/free-monoids.tex

@@ -1,9 +1,11 @@
 \section{Construction of Free Monoids}
 \label{sec:monoids}
 
-Free monoids are well-known to functional programmers. In this section, we consider various constructions of them in type theory, and prove their universal property. Because we are working in univalent type theory, these constructions are equivalent as types (and as monoids).
-
-\vc{some stuff about universal property and how it is useful}
+Free monoids are well-known to functional programmers. In this section, we consider various constructions
+of them in type theory, and prove their universal property. Because we are working in univalent type theory,
+these constructions are equivalent as types (and as monoids). By showing that these constructions satisfy
+the universal property of free monoid, we obtain a very general operation which allows us to structure our
+programs using ideas from algebra as explained in~\ref{sec:combinatorics}.
 
 \subsection{List}\label{mon:list}
 

papers/icfp24/introduction.tex

@@ -10,7 +10,7 @@ \section{Introduction}
   \tikz[anchor=base, baseline]{%
     \foreach \x/\color in {1/red,2/white,3/blue} {
         \node[circle,draw,fill=\color,line width=1pt] at (\x,0) {\phantom{\tiny\x}};
-        \ifthenelse{\NOT 3 = \x}{\node at ({\x+0.5},0) {,};}{}
+        \ifthenelse{\NOT 1 = \x}{\node at ({\x-0.5},0) {,};}{}
       }
   }
   \}
@@ -21,7 +21,7 @@ \section{Introduction}
       \tikz[anchor=base, baseline]{%
         \foreach \x/\color in {1/red,2/red,3/blue,4/white,5/blue,6/red,7/white,8/blue} {
             \node[circle,draw,fill=\color,line width=1pt] at (\x,0) {\phantom{\tiny\x}};
-            \ifthenelse{\NOT 8 = \x}{\node at ({\x+0.5},0) {,};}{}
+            \ifthenelse{\NOT 1 = \x}{\node at ({\x-0.5},0) {,};}{}
           }
       }
     ]
@@ -36,7 +36,7 @@ \section{Introduction}
       \tikz[anchor=base, baseline]{%
         \foreach \x/\color in {1/red,2/red,3/red,4/white,5/white,6/blue,7/blue,8/blue} {
             \node[circle,draw,fill=\color,line width=1pt] at (\x,0) {\phantom{\tiny\x}};
-            \ifthenelse{\NOT 8 = \x}{\node at ({\x+0.5},0) {,};}{}
+            \ifthenelse{\NOT 1 = \x}{\node at ({\x-0.5},0) {,};}{}
           }
       }
     ]
@@ -45,6 +45,16 @@ \section{Introduction}
 %
 Thus, the numbered of correct sorting functions is equal to the number of ways of ordering the colors!
 
+\redtext{Intuition: what does a correct sorting algorithm do?}
+\begin{itemize}
+    \item It partitions the list by a key, in this case, the colors of the balls.
+    \item The keys need to be totally ordered in order to sort the partitions.
+    \item The number of total orderings will equal the number of possible ways of sorting the sequence.
+\end{itemize}
+\redtext{
+    We will use this simple observation as a motivation, but rather than thinking of it terms of counting, we will go a dimension higher and consider isomorphisms (or bijections) of sets. Is there a connection between the set of total orderings on the carrier set, and the set of correct sorting functions? Our discovery is that there is a bijection between the two! From this observation, we obtain an axiomatic understanding of the correctness of sorting.
+}
+
 \subsection*{Solving the puzzle}
 
 Suppose $A$ is the 3-element set $\{a,b,c\}$. There are many possible orderings of these elements,
@@ -163,5 +173,6 @@ \subsubsection*{Outline and Contributions}
   \item In~\cref{sec:commutative-monoids}, we add commutativity to free monoids, and show how to extend the proofs of universal property appropriately, to get the universal property of free commutative monoids.
   \item \vc{In~\cref{sec:combinatorics}, we show how free monoids and free commutative monoids are different, by discussing various combinatorial properties and operations, which can be defined for both, and ones which cannot be defined for both}.
   \item In \cref{sec:sorting}, we build on the constructions of the previous sections and study intrinsically verified sorting function. The main result in this section is to connect total orders and sorting and commutativity, by proving an equivalence between decidable total orders on a carrier set $A$, and correct sorting algorithms on lists of elements of $A$.
+  \item All the work in this paper is formalized in Cubical Agda, which is discussed in~\cref{sec:formalization}, and the accompanying code is available as supplementary material. Although the formalization is a contribution in itself, the purpose of the paper is not to discuss the formalization, but to present the results in un-formalized form, using HoTT/UF as a foundation, so the ideas are accessible to a wider audience, even without a background in type theory or formalization.
   \item In~\cref{sec:discussion}, we discuss connections to related work, and future work.
 \end{myitemize}

papers/icfp24/localSettings.yaml

@@ -8,4 +8,7 @@ lookForAlignDelims:
 verbatimEnvironments:
     code: 1
     lcode: 1
-    mpcode: 1
+    mpcode: 1
+
+indentAfterItems:
+    myitemize: 1

papers/icfp24/macros.sty

@@ -67,3 +67,9 @@
 % apxproof
 \newtheoremrep{proposition}{Proposition}
 \newtheoremrep{lemma}{Lemma}
+
+% yoneda
+\DeclareFontFamily{U}{min}{}
+\DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
+\newcommand{\yo}
+{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}

papers/icfp24/math.sty

@@ -43,6 +43,7 @@
 %
 \newcommand{\LL}{\mathcal{L}}
 \newcommand{\MM}{\mathcal{M}}
+\newcommand{\FF}{\mathcal{F}}
 
 % sort
 \newcommand{\sort}{\mathsf{sort}}