algebra.tex 9.34 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 26 27 28  A COFE $A$ is called \emph{discrete} if all its elements are discrete. \end{defn} \begin{defn}  Ralf Jung committed Mar 09, 2016 29  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 30  $\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 31  It is \emph{contractive} if  Ralf Jung committed Mar 09, 2016 32  $\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 33 34 35 36 37 \end{defn} \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn}  Ralf Jung committed Mar 11, 2016 38 39 40 41 42 43 44 45  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 46 47  \begin{defn}  Ralf Jung committed Mar 11, 2016 48  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 49 50  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 11, 2016 51 The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.  Ralf Jung committed Mar 11, 2016 52 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 53 54 55  \subsection{RA}  Ralf Jung committed Mar 12, 2016 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 \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 $\All \melt_f. \melt \mtimes \melt_f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval$ 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 81   Ralf Jung committed Feb 29, 2016 82 83 84 \subsection{CMRA} \begin{defn}  Ralf Jung committed Mar 11, 2016 85  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 86  \begin{align*}  Ralf Jung committed Mar 10, 2016 87  \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 88 89 90  \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 91 92  \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 93  \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\  Ralf Jung committed Mar 08, 2016 94  \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 95 96 97  \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 98 99  \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 100 101 102  \end{align*} \end{defn}  Ralf Jung committed Mar 10, 2016 103 104 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 105 106 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 107 108 109 110 111  \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 112 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 \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 129  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}  Ralf Jung committed Feb 29, 2016 130 131  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB} \end{mathpar}  Ralf Jung committed Mar 06, 2016 132 (This assumes that the type $\type$ is non-empty.)  Ralf Jung committed Feb 29, 2016 133   Ralf Jung committed Mar 08, 2016 134 135 136 \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 137 138  \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 139  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Mar 08, 2016 140  \item $\munit$ is a discrete COFE element  Ralf Jung committed Mar 08, 2016 141 142 143  \end{enumerate} \end{defn}  Ralf Jung committed Mar 07, 2016 144 145 146 147 148 149 150 151 \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 $\All n, \melt_f. \melt \mtimes \melt_f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval_n$ 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 152 153 154 155 156 157 158 159 160 161 \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 162 163  \begin{defn}  Ralf Jung committed Mar 09, 2016 164  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 165  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 166 167  \item $f$ is non-expansive \item $f$ preserves validity: \\  Ralf Jung committed Mar 09, 2016 168  $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$  Ralf Jung committed Mar 07, 2016 169  \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 11, 2016 170  $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$  Ralf Jung committed Mar 07, 2016 171 172 173 174 175 176 177  \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 178 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Mar 07, 2016 179   Ralf Jung committed Feb 29, 2016 180   Ralf Jung committed Jan 31, 2016 181 182 183 184 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: