From 2a32b985ea97e65b70de87bd0d8a14c8a4c88a7c Mon Sep 17 00:00:00 2001 From: pufferfish <74378430+pufferffish@users.noreply.github.com> Date: Mon, 26 Feb 2024 13:36:17 +0000 Subject: [PATCH] save progress on combinatorics --- papers/icfp24/combinatorics.tex | 106 ++++++++++++++++++++++++++++++- papers/icfp24/free-monoids.tex | 8 ++- papers/icfp24/introduction.tex | 17 ++++- papers/icfp24/localSettings.yaml | 5 +- papers/icfp24/macros.sty | 6 ++ papers/icfp24/math.sty | 1 + 6 files changed, 134 insertions(+), 9 deletions(-) diff --git a/papers/icfp24/combinatorics.tex b/papers/icfp24/combinatorics.tex index b32d824..25950ca 100644 --- a/papers/icfp24/combinatorics.tex +++ b/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)$. diff --git a/papers/icfp24/free-monoids.tex b/papers/icfp24/free-monoids.tex index c5b860a..7914029 100644 --- a/papers/icfp24/free-monoids.tex +++ 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} diff --git a/papers/icfp24/introduction.tex b/papers/icfp24/introduction.tex index eb04a7c..a4fceb0 100644 --- a/papers/icfp24/introduction.tex +++ b/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} diff --git a/papers/icfp24/localSettings.yaml b/papers/icfp24/localSettings.yaml index 0087940..0612823 100644 --- a/papers/icfp24/localSettings.yaml +++ b/papers/icfp24/localSettings.yaml @@ -8,4 +8,7 @@ lookForAlignDelims: verbatimEnvironments: code: 1 lcode: 1 - mpcode: 1 \ No newline at end of file + mpcode: 1 + +indentAfterItems: + myitemize: 1 diff --git a/papers/icfp24/macros.sty b/papers/icfp24/macros.sty index 5c021b5..c9b4f49 100644 --- a/papers/icfp24/macros.sty +++ b/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}}\!} \ No newline at end of file diff --git a/papers/icfp24/math.sty b/papers/icfp24/math.sty index 5fddfd9..560d9e8 100644 --- a/papers/icfp24/math.sty +++ b/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}}