algebra.tex 7.63 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 Feb 29, 2016 5 \begin{defn}[Chain]  Ralf Jung committed Mar 09, 2016 6  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 7 8 \end{defn}  Ralf Jung committed Feb 29, 2016 9 \begin{defn}  Ralf Jung committed Mar 09, 2016 10  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 11 12 13 14  \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 15  \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}  Ralf Jung committed Feb 29, 2016 16 17 18 19 20  \end{align*} \end{defn} \ralf{Copy the explanation from the paper, when that one is more polished.}  Ralf Jung committed Mar 07, 2016 21 \begin{defn}  Ralf Jung committed Mar 09, 2016 22 23  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 24 25 26 27  A COFE $A$ is called \emph{discrete} if all its elements are discrete. \end{defn} \begin{defn}  Ralf Jung committed Mar 09, 2016 28  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 29  $\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 30  It is \emph{contractive} if  Ralf Jung committed Mar 09, 2016 31  $\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 32 33 34 35 36 37 38 39 \end{defn} \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn} Note that $\COFEs$ is cartesian closed. \begin{defn}  Ralf Jung committed Mar 09, 2016 40 41  A functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its actions $F_1$ on arrows is itself a non-expansive map. \ralf{We need bifunctors.}  Ralf Jung committed Mar 07, 2016 42 43  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 07, 2016 44 45 46 47  \subsection{RA} \ralf{Define this, including frame-preserving updates.}  Ralf Jung committed Mar 07, 2016 48   Ralf Jung committed Feb 29, 2016 49 50 51 \subsection{CMRA} \begin{defn}  Ralf Jung committed Mar 09, 2016 52  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, (\mdiv) : \monoid \times \monoid \nfn \monoid)$ satisfying  Ralf Jung committed Feb 29, 2016 53  \begin{align*}  Ralf Jung committed Mar 10, 2016 54  \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 55 56 57  \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 58 59 60 61  \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\ \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\ \All \melt, \meltB.& \melt \leq \meltB \Ra \mcore\melt \leq \mcore\meltB \tagH{cmra-core-mono} \\ \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 62 63 64 65 66 67 68 69  \All \melt, \meltB.& \melt \leq \meltB \Ra \melt \mtimes (\meltB \mdiv \melt) = \meltB \tagH{cmra-div-op} \\ \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\\ \melt \leq \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \end{align*} \end{defn}  Ralf Jung committed Mar 10, 2016 70 71 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 Feb 29, 2016 72   Ralf Jung committed Mar 11, 2016 73 \ralf{TODO: Get rid of division.}  Ralf Jung committed Feb 29, 2016 74 75 76 77 78  \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 79 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 \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 96  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}  Ralf Jung committed Feb 29, 2016 97 98  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB} \end{mathpar}  Ralf Jung committed Mar 06, 2016 99 (This assumes that the type $\type$ is non-empty.)  Ralf Jung committed Feb 29, 2016 100   Ralf Jung committed Mar 08, 2016 101 102 103 \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 104 105  \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 106  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Mar 08, 2016 107  \item $\munit$ is a discrete COFE element  Ralf Jung committed Mar 08, 2016 108 109 110  \end{enumerate} \end{defn}  Ralf Jung committed Mar 07, 2016 111 112 113 114 115 116 117 118 \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 119 120 121 122 123 124 125 \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$ \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 09, 2016 126  $\All \melt \in \monoid, \meltB \in \monoid. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$  Ralf Jung committed Mar 08, 2016 127 128 129 130  \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 131 132  \begin{defn}  Ralf Jung committed Mar 09, 2016 133  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 134  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 135 136  \item $f$ is non-expansive \item $f$ preserves validity: \\  Ralf Jung committed Mar 09, 2016 137  $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$  Ralf Jung committed Mar 07, 2016 138  \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 09, 2016 139  $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$  Ralf Jung committed Mar 07, 2016 140 141 142 143 144 145 146  \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 147 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Mar 07, 2016 148   Ralf Jung committed Feb 29, 2016 149   Ralf Jung committed Jan 31, 2016 150 151 152 153 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: