algebra.tex 9.52 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 09, 2016 54  \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-nonexp} \\  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 70 71  \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{Copy the rest of the explanation from the paper, when that one is more polished.}  Ralf Jung committed Feb 29, 2016 72 \paragraph{The division operator $\mdiv$.}  Ralf Jung committed Feb 29, 2016 73 74 75 76 77 78 79 80 81 82 83 84 85 86 One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt \leq \meltB$, then $\melt \mdiv \meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}). Otherwise, $\mdiv$ can have arbitrary behavior. This means that, in classical logic, the division operator can be defined for any PCM using the axiom of choice, and it will trivially satisfy \ruleref{cmra-div-op}. However, notice that the division operator also has to be \emph{non-expansive} --- so if the carrier $\monoid$ is equipped with a non-trivial $\nequiv{n}$, there is an additional proof obligation here. This is crucial, for the following reason: Considering that the extension order is defined using \emph{equality}, there is a natural notion of a \emph{step-indexed extension} order using the step-indexed equivalence of the underlying COFE: $\melt \mincl{n} \meltB \eqdef \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclM}$ One of the properties we would expect to hold is the usual correspondence between a step-indexed predicate and its non-step-indexed counterpart: $\All \melt, \meltB. \melt \leq \meltB \Lra (\All n. \melt \mincl{n} \meltB) \tagH{cmra-incl-limit}$ The right-to-left direction here is trick. For every $n$, we obtain a proof that $\melt \mincl{n} \meltB$. From this, we could extract a sequence of witnesses $(\meltC_m)_{m}$, and we need to arrive at a single witness $\meltC$ showing that $\melt \leq \meltB$. Without the division operator, there is no reason to believe that such a witness exists. However, since we can use the division operator, and since we know that this operator is \emph{non-expansive}, we can pick $\meltC \eqdef \meltB \mdiv \melt$, and then we can prove that this is indeed the desired witness.  Ralf Jung committed Mar 10, 2016 87 \ralf{The only reason we actually have division is that we are working constructively \emph{and}, at the same time, remain compatible with a classic interpretation of the existential. This is pretty silly.}  Ralf Jung committed Feb 29, 2016 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109  \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{Needs some magic to fix the baseline of the $\nequiv{n}$, or so} \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 110  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}  Ralf Jung committed Feb 29, 2016 111 112  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB} \end{mathpar}  Ralf Jung committed Mar 06, 2016 113 (This assumes that the type $\type$ is non-empty.)  Ralf Jung committed Feb 29, 2016 114   Ralf Jung committed Mar 08, 2016 115 116 117 \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 118 119  \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 120  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Mar 08, 2016 121  \item $\munit$ is a discrete COFE element  Ralf Jung committed Mar 08, 2016 122 123 124  \end{enumerate} \end{defn}  Ralf Jung committed Mar 07, 2016 125 126 127 128 129 130 131 132 \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 133 134 135 136 137 138 139 \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 140  $\All \melt \in \monoid, \meltB \in \monoid. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$  Ralf Jung committed Mar 08, 2016 141 142 143 144  \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 145 146  \begin{defn}  Ralf Jung committed Mar 09, 2016 147  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 148  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 149 150  \item $f$ is non-expansive \item $f$ preserves validity: \\  Ralf Jung committed Mar 09, 2016 151  $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$  Ralf Jung committed Mar 07, 2016 152  \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 09, 2016 153  $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$  Ralf Jung committed Mar 07, 2016 154 155 156 157 158 159 160  \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 161 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Mar 07, 2016 162   Ralf Jung committed Feb 29, 2016 163   Ralf Jung committed Jan 31, 2016 164 165 166 167 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: