algebra.tex 13.6 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 15, 2016 5 The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).  Ralf Jung committed Mar 12, 2016 6 This definition varies slightly from the original one in~\cite{catlogic}.  Ralf Jung committed Mar 15, 2016 7   Ralf Jung committed Feb 29, 2016 8 \begin{defn}[Chain]  Robbert Krebbers committed Oct 17, 2016 9  Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.  Ralf Jung committed Feb 29, 2016 10 11 \end{defn}  Ralf Jung committed Feb 29, 2016 12 \begin{defn}  Robbert Krebbers committed Oct 17, 2016 13  A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}, \lim : \chain(\cofe) \to \cofe)$ satisfying  Ralf Jung committed Feb 29, 2016 14 15 16 17  \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 Aug 04, 2016 18  \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}  Ralf Jung committed Feb 29, 2016 19 20 21  \end{align*} \end{defn}  Ralf Jung committed Mar 15, 2016 22 23 24 The key intuition behind COFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps. In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{cofe-mono})---and in the limit, it agrees with plain equality (\ruleref{cofe-limit}). In order to solve the recursive domain equation in \Sref{sec:model} it is also essential that COFEs are \emph{complete}, \ie that any chain has a limit (\ruleref{cofe-compl}).  Ralf Jung committed Feb 29, 2016 25   Ralf Jung committed Mar 07, 2016 26 \begin{defn}  Ralf Jung committed Mar 09, 2016 27 28  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 29  A COFE $A$ is called \emph{discrete} if all its elements are discrete.  Ralf Jung committed Mar 12, 2016 30 31  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 32 33 34 \end{defn} \begin{defn}  Ralf Jung committed Mar 09, 2016 35  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 36  $\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 37  It is \emph{contractive} if  Ralf Jung committed Aug 04, 2016 38  $\All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y)$  Ralf Jung committed Mar 07, 2016 39 \end{defn}  Ralf Jung committed Mar 15, 2016 40 41 Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.  Robbert Krebbers committed Aug 21, 2016 42 The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.  Ralf Jung committed Mar 07, 2016 43 44 45 46  \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn}  Ralf Jung committed Mar 11, 2016 47   Ralf Jung committed Aug 11, 2016 48 Note that $\COFEs$ is cartesian closed. In particular:  Ralf Jung committed Mar 11, 2016 49 50 51 52 53 54 \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 55 56  \begin{defn}  Ralf Jung committed Mar 11, 2016 57  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 58 59  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 11, 2016 60 The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.  Ralf Jung committed Mar 11, 2016 61 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 Aug 21, 2016 62 The reason contractive (bi)functors are interesting is that by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, they have a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.  Ralf Jung committed Mar 07, 2016 63 64 65  \subsection{RA}  Ralf Jung committed Mar 12, 2016 66 67 \begin{defn} A \emph{resource algebra} (RA) is a tuple \\  Ralf Jung committed Jul 25, 2016 68 69  $(\monoid, \mval \subseteq \monoid, \mcore{{-}}: \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:  Ralf Jung committed Mar 12, 2016 70 71 72  \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} \\  Ralf Jung committed Jul 25, 2016 73 74 75  \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\ \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\ \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\  Ralf Jung committed Mar 12, 2016 76 77  \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\ \text{where}\qquad %\qquad\\  Ralf Jung committed Jul 25, 2016 78  \maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\  Ralf Jung committed Jul 25, 2016 79  \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}  Ralf Jung committed Mar 12, 2016 80 81  \end{align*} \end{defn}  Ralf Jung committed Mar 15, 2016 82 83 84 \noindent RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences: \begin{enumerate}  Ralf Jung committed Jul 25, 2016 85 \item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset $\mval$ of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).  Ralf Jung committed Mar 15, 2016 86   Ralf Jung committed Jul 25, 2016 87 88 89 90 91 92 This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, CMRAs, in the next subsection. \item Instead of a single unit that is an identity to every element, we allow for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}. We further demand that $\mcore{{-}}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the \emph{extension order}, defined similarly to that for PCMs (\ruleref{ra-incl}).  Ralf Jung committed Jul 25, 2016 93  Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.  Ralf Jung committed Jul 25, 2016 94 95 96 97 98 99 100 % (This corresponds to the option type.) Thus, the core can be \emph{partial}: not all elements need to have a unit. We use the metavariable $\maybe\melt$ to indicate elements of $\maybe\monoid$. We also lift the composition $(\mtimes)$ to $\maybe\monoid$. Partial cores help us to build interesting composite RAs from smaller primitives. Notice also that the core of an RA is a strict generalization of the unit that any PCM must provide, since $\mcore{{-}}$ can always be picked as a constant function.  Ralf Jung committed Mar 15, 2016 101 102 \end{enumerate}  Ralf Jung committed Mar 12, 2016 103 104 105  \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 Jul 25, 2016 106  $\All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \maybe{\melt_\f} \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval$  Ralf Jung committed Mar 12, 2016 107 108 109  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn}  Ralf Jung committed Jul 25, 2016 110 The assertion $\melt \mupd \meltsB$ says that every element $\maybe{\melt_\f}$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.  Ralf Jung committed Jul 25, 2016 111 Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.  Ralf Jung committed Mar 15, 2016 112 113 Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions. Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.  Ralf Jung committed Mar 07, 2016 114   Ralf Jung committed Feb 29, 2016 115 116 117 \subsection{CMRA} \begin{defn}  Robbert Krebbers committed Oct 17, 2016 118  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:  Ralf Jung committed Feb 29, 2016 119  \begin{align*}  Ralf Jung committed Mar 10, 2016 120  \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 Jul 25, 2016 121  \All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\  Ralf Jung committed Feb 29, 2016 122 123  \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 Jul 25, 2016 124 125 126  \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\ \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\ \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\  Ralf Jung committed Mar 08, 2016 127  \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 128 129 130  \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 Jul 25, 2016 131  \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\  Ralf Jung committed Mar 12, 2016 132  \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}  Ralf Jung committed Feb 29, 2016 133 134 135  \end{align*} \end{defn}  Ralf Jung committed Mar 10, 2016 136 137 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 138 We define the plain $\mval$ as the limit'' of the $\mval_n$:  Robbert Krebbers committed Oct 17, 2016 139 $\mval \eqdef \bigcap_{n \in \nat} \mval_n$  Ralf Jung committed Feb 29, 2016 140 141 142 143 144  \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 145 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 146 147 148 149 150 151 152 153 154 155 156 157 158 159 \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$.  Ralf Jung committed Jul 25, 2016 160 This operation is needed to prove that $\later$ commutes with separating conjunction:  Ralf Jung committed Feb 29, 2016 161 \begin{mathpar}  Ralf Jung committed Jul 25, 2016 162  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}  Ralf Jung committed Feb 29, 2016 163 164 \end{mathpar}  Ralf Jung committed Mar 08, 2016 165 166 167 \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 168 169  \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 170  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Jul 25, 2016 171  \item $\munit$ is its own core: \\ $\mcore\munit = \munit$  Ralf Jung committed Mar 08, 2016 172 173 174  \end{enumerate} \end{defn}  Ralf Jung committed Jul 25, 2016 175 \begin{lem}\label{lem:cmra-unit-total-core}  Ralf Jung committed Jul 25, 2016 176 177 178  If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$. \end{lem}  Ralf Jung committed Mar 07, 2016 179 180 \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 Jul 25, 2016 181  $\All n, \maybe{\melt_\f}. \melt \mtimes \maybe{\melt_\f} \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval_n$  Ralf Jung committed Mar 07, 2016 182 183 184 185 186  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 187 188 189 190 \begin{defn} A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt] \item $\monoid$ is a discrete COFE  Ralf Jung committed Mar 16, 2016 191  \item $\mval$ ignores the step-index: \\  Ralf Jung committed Mar 08, 2016 192 193 194 195 196  $\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 197 198  \begin{defn}  Ralf Jung committed Mar 09, 2016 199  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 200  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 201 202  \item $f$ is non-expansive \item $f$ preserves validity: \\  Ralf Jung committed Mar 09, 2016 203  $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$  Ralf Jung committed Mar 07, 2016 204  \item $f$ preserves CMRA inclusion:\\  Ralf Jung committed Mar 11, 2016 205  $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$  Ralf Jung committed Mar 07, 2016 206 207 208 209 210 211  \end{enumerate} \end{defn} \begin{defn} The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows. \end{defn}  Ralf Jung committed Jul 25, 2016 212 Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.  Ralf Jung committed Mar 09, 2016 213 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Aug 04, 2016 214 %TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.  Ralf Jung committed Feb 29, 2016 215   Ralf Jung committed Jan 31, 2016 216 217 218 219 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: