algebra.tex 9.64 KB
 Ralf Jung committed Jan 31, 2016 1 \section{Algebraic Structures}  Ralf Jung committed Jan 31, 2016 2   Ralf Jung committed Feb 29, 2016 3 4 \subsection{COFE}  Ralf Jung committed Mar 12, 2016 5 This definition varies slightly from the original one in~\cite{catlogic}.  Ralf Jung committed Feb 29, 2016 6 \begin{defn}[Chain]  Ralf Jung committed Mar 09, 2016 7  Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.  Ralf Jung committed Feb 29, 2016 8 9 \end{defn}  Ralf Jung committed Feb 29, 2016 10 \begin{defn}  Ralf Jung committed Mar 09, 2016 11  A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}, \lim : \chain(\cofe) \to \cofe)$ satisfying  Ralf Jung committed Feb 29, 2016 12 13 14 15  \begin{align*} \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\  Ralf Jung committed Feb 29, 2016 16  \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}  Ralf Jung committed Feb 29, 2016 17 18 19 20 21  \end{align*} \end{defn} \ralf{Copy the explanation from the paper, when that one is more polished.}  Ralf Jung committed Mar 07, 2016 22 \begin{defn}  Ralf Jung committed Mar 09, 2016 23 24  An element $x \in \cofe$ of a COFE is called \emph{discrete} if $\All y \in \cofe. x \nequiv{0} y \Ra x = y$  Ralf Jung committed Mar 07, 2016 25  A COFE $A$ is called \emph{discrete} if all its elements are discrete.  Ralf Jung committed Mar 12, 2016 26 27  For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$  Ralf Jung committed Mar 07, 2016 28 29 30 \end{defn} \begin{defn}  Ralf Jung committed Mar 09, 2016 31  A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if  Ralf Jung committed Mar 09, 2016 32  $\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y)$  Ralf Jung committed Mar 07, 2016 33  It is \emph{contractive} if  Ralf Jung committed Mar 09, 2016 34  $\All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x)$  Ralf Jung committed Mar 07, 2016 35 \end{defn}  Ralf Jung committed Mar 12, 2016 36 The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.  Ralf Jung committed Mar 07, 2016 37 38 39 40  \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn}  Ralf Jung committed Mar 11, 2016 41 42 43 44 45 46 47 48  Note that $\COFEs$ is cartesian closed: \begin{defn} Given two COFEs $\cofe$ and $\cofeB$, the set of non-expansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with \begin{align*} f \nequiv{n} g \eqdef{}& \All x \in \cofe. f(x) \nequiv{n} g(x) \end{align*} \end{defn}  Ralf Jung committed Mar 07, 2016 49 50  \begin{defn}  Ralf Jung committed Mar 11, 2016 51  A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.  Ralf Jung committed Mar 07, 2016 52 53  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 11, 2016 54 The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.  Ralf Jung committed Mar 11, 2016 55 Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.  Ralf Jung committed Mar 07, 2016 56 57 58  \subsection{RA}  Ralf Jung committed Mar 12, 2016 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 \begin{defn} A \emph{resource algebra} (RA) is a tuple \\ $(\monoid, \mval \subseteq \monoid, \mcore{-}: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying \begin{align*} \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\ \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\ \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\ \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\ \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\ \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\ \text{where}\qquad %\qquad\\ \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{ra-incl} \end{align*} \end{defn} \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if  Ralf Jung committed Mar 12, 2016 77  $\All \melt_\f. \melt \mtimes \melt_\f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval$  Ralf Jung committed Mar 12, 2016 78 79 80 81 82 83  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn} \ralf{Copy the explanation from the paper, when that one is more polished.}  Ralf Jung committed Mar 07, 2016 84   Ralf Jung committed Feb 29, 2016 85 86 87 \subsection{CMRA} \begin{defn}  Ralf Jung committed Mar 11, 2016 88  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying  Ralf Jung committed Feb 29, 2016 89  \begin{align*}  Ralf Jung committed Mar 10, 2016 90  \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\  Ralf Jung committed Feb 29, 2016 91 92 93  \All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\ \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\ \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\  Ralf Jung committed Mar 08, 2016 94 95  \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\ \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\  Ralf Jung committed Mar 11, 2016 96  \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\  Ralf Jung committed Mar 08, 2016 97  \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\  Ralf Jung committed Feb 29, 2016 98 99 100  \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\ &\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\ \text{where}\qquad\qquad\\  Ralf Jung committed Mar 12, 2016 101 102  \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}\\ \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}  Ralf Jung committed Feb 29, 2016 103 104 105  \end{align*} \end{defn}  Ralf Jung committed Mar 10, 2016 106 107 This is a natural generalization of RAs over COFEs. All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.  Ralf Jung committed Mar 11, 2016 108 109 We define the plain $\mval$ as the limit'' of the $\mval_n$: $\mval \eqdef \bigcap_{n \in \mathbb{N}} \mval_n$  Ralf Jung committed Feb 29, 2016 110 111 112 113 114  \paragraph{The extension axiom (\ruleref{cmra-extend}).} Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq. The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:  Ralf Jung committed Mar 10, 2016 115 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 \begin{center} \begin{tikzpicture}[every edge/.style={draw=none}] \node (a) at (0, 0) {$\melt$}; \node (b) at (1.7, 0) {$\meltB$}; \node (b12) at (1.7, -1) {$\meltB_1 \mtimes \meltB_2$}; \node (a12) at (0, -1) {$\melt_1 \mtimes \melt_2$}; \path (a) edge node {$\nequiv{n}$} (b); \path (a12) edge node {$\nequiv{n}$} (b12); \path (a) edge node [rotate=90] {$=$} (a12); \path (b) edge node [rotate=90] {$=$} (b12); \end{tikzpicture}\end{center} where the $n$-equivalence at the bottom is meant to apply to the pairs of elements, \ie we demand $\melt_1 \nequiv{n} \meltB_1$ and $\melt_2 \nequiv{n} \meltB_2$. In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$. This operation is needed to prove that $\later$ commutes with existential quantification and separating conjunction: \begin{mathpar}  Ralf Jung committed Mar 06, 2016 132  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}  Ralf Jung committed Feb 29, 2016 133 134  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB} \end{mathpar}  Ralf Jung committed Mar 06, 2016 135 (This assumes that the type $\type$ is non-empty.)  Ralf Jung committed Feb 29, 2016 136   Ralf Jung committed Mar 08, 2016 137 138 139 \begin{defn} An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 08, 2016 140 141  \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$ \item $\munit$ is a left-identity of the operation: \\  Ralf Jung committed Mar 08, 2016 142  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Mar 08, 2016 143  \item $\munit$ is a discrete COFE element  Ralf Jung committed Mar 08, 2016 144 145 146  \end{enumerate} \end{defn}  Ralf Jung committed Mar 07, 2016 147 148 \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if  Ralf Jung committed Mar 12, 2016 149  $\All n, \melt_\f. \melt \mtimes \melt_\f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval_n$  Ralf Jung committed Mar 07, 2016 150 151 152 153 154  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn} Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.  Ralf Jung committed Mar 08, 2016 155 156 157 158 159 160 161 162 163 164 \begin{defn} A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt] \item $\monoid$ is a discrete COFE \item $\val$ ignores the step-index: \\ $\All \melt \in \monoid. \melt \in \mval_0 \Ra \All n, \melt \in \mval_n$ \end{enumerate} \end{defn} Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation. Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.  Ralf Jung committed Mar 07, 2016 165 166  \begin{defn}  Ralf Jung committed Mar 09, 2016 167  A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{monotone} (written $f : \monoid_1 \monra \monoid_2$) if it satisfies the following conditions:  Ralf Jung committed Mar 08, 2016 168  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 169 170  \item $f$ is non-expansive \item $f$ preserves validity: \\  Ralf Jung committed Mar 09, 2016 171  $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$  Ralf Jung committed Mar 07, 2016 172  \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 11, 2016 173  $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$  Ralf Jung committed Mar 07, 2016 174 175 176 177 178 179 180  \end{enumerate} \end{defn} \begin{defn} The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows. \end{defn} Note that $\CMRAs$ is a subcategory of $\COFEs$.  Ralf Jung committed Mar 09, 2016 181 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Mar 07, 2016 182   Ralf Jung committed Feb 29, 2016 183   Ralf Jung committed Jan 31, 2016 184 185 186 187 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: