algebra.tex 13.4 KB
Newer Older
 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]  Ralf Jung committed Mar 09, 2016 9  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 10 11 \end{defn}  Ralf Jung committed Feb 29, 2016 12 \begin{defn}  Ralf Jung committed Mar 09, 2016 13  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 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 Feb 29, 2016 18  \All n, c.& \lim(c) \nequiv{n} c(n+1) \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 Mar 09, 2016 38  $\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 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$.  Ralf Jung committed Mar 12, 2016 42 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 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 48 49 50 51 52 53 54  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 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 Mar 07, 2016 62 63 64  \subsection{RA}  Ralf Jung committed Mar 12, 2016 65 66 \begin{defn} A \emph{resource algebra} (RA) is a tuple \\  Ralf Jung committed Jul 25, 2016 67 68  $(\monoid, \mval \subseteq \monoid, \mcore{{-}}: \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:  Ralf Jung committed Mar 12, 2016 69 70 71  \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 72 73 74  \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 75 76  \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 77  \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 78  \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}  Ralf Jung committed Mar 12, 2016 79 80  \end{align*} \end{defn}  Ralf Jung committed Mar 15, 2016 81 82 83 \noindent RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences: \begin{enumerate}  Ralf Jung committed Jul 25, 2016 84 \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 85   Ralf Jung committed Jul 25, 2016 86 87 88 89 90 91 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 92  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 93 94 95 96 97 98 99 % (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 100 101 \end{enumerate}  Ralf Jung committed Mar 12, 2016 102 103 104  \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 105  $\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 106 107 108  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn}  Ralf Jung committed Jul 25, 2016 109 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 110 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 111 112 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 113   Ralf Jung committed Feb 29, 2016 114 115 116 \subsection{CMRA} \begin{defn}  Ralf Jung committed Jul 25, 2016 117  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:  Ralf Jung committed Feb 29, 2016 118  \begin{align*}  Ralf Jung committed Mar 10, 2016 119  \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 120  \All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\  Ralf Jung committed Feb 29, 2016 121 122  \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 123 124 125  \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 126  \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 127 128 129  \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 130  \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\  Ralf Jung committed Mar 12, 2016 131  \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}  Ralf Jung committed Feb 29, 2016 132 133 134  \end{align*} \end{defn}  Ralf Jung committed Mar 10, 2016 135 136 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 137 138 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 139 140 141 142 143  \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 144 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 145 146 147 148 149 150 151 152 153 154 155 156 157 158 \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 159 This operation is needed to prove that $\later$ commutes with separating conjunction:  Ralf Jung committed Feb 29, 2016 160 \begin{mathpar}  Ralf Jung committed Jul 25, 2016 161  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}  Ralf Jung committed Feb 29, 2016 162 163 \end{mathpar}  Ralf Jung committed Mar 08, 2016 164 165 166 \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 167 168  \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 169  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Mar 08, 2016 170  \item $\munit$ is a discrete COFE element  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 Jul 27, 2016 214 \ralf{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: