algebra.tex 15.1 KB
 Robbert Krebbers committed Dec 10, 2017 1 \section{Algebraic structures}  Ralf Jung committed Jan 31, 2016 2   Ralf Jung committed Dec 05, 2016 3 \subsection{OFE}  Ralf Jung committed Feb 29, 2016 4   Ralf Jung committed Dec 05, 2016 5 The model of Iris lives in the category of \emph{Ordered Families of Equivalences} (OFEs).  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}  Ralf Jung committed Dec 05, 2016 9  An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying  Ralf Jung committed Feb 29, 2016 10  \begin{align*}  Ralf Jung committed Dec 05, 2016 11 12 13  \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{ofe-equiv} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{ofe-mono} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{ofe-limit}  Ralf Jung committed Feb 29, 2016 14 15 16  \end{align*} \end{defn}  Ralf Jung committed Dec 05, 2016 17 18 The key intuition behind OFEs 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{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).  Ralf Jung committed Feb 29, 2016 19   Ralf Jung committed Mar 07, 2016 20 \begin{defn}  Ralf Jung committed Dec 05, 2016 21 22 23 24  An element $x \in \ofe$ of an OFE is called \emph{discrete} if $\All y \in \ofe. x \nequiv{0} y \Ra x = y$ An OFE $A$ is called \emph{discrete} if all its elements are discrete. For a set $X$, we write $\Delta X$ for the discrete OFE with $x \nequiv{n} x' \eqdef x = x'$  Ralf Jung committed Mar 07, 2016 25 26 27 \end{defn} \begin{defn}  Ralf Jung committed Dec 05, 2016 28 29  A function $f : \ofe \to \ofeB$ between two OFEs is \emph{non-expansive} (written $f : \ofe \nfn \ofeB$) if $\All n, x \in \ofe, y \in \ofe. 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 Dec 05, 2016 31  $\All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y)$  Ralf Jung committed Mar 07, 2016 32 \end{defn}  Ralf Jung committed Mar 15, 2016 33 34 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 07, 2016 35 36  \begin{defn}  Ralf Jung committed Dec 05, 2016 37  The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.  Ralf Jung committed Mar 07, 2016 38 \end{defn}  Ralf Jung committed Mar 11, 2016 39   Ralf Jung committed Nov 28, 2017 40 41 Note that $\OFEs$ is bicartesian closed, \ie it has all sums, products and exponentials as well as an initial and a terminal object. In particular:  Ralf Jung committed Mar 11, 2016 42 \begin{defn}  Ralf Jung committed Dec 05, 2016 43  Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with  Ralf Jung committed Mar 11, 2016 44  \begin{align*}  Ralf Jung committed Dec 05, 2016 45  f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)  Ralf Jung committed Mar 11, 2016 46 47  \end{align*} \end{defn}  Ralf Jung committed Mar 07, 2016 48 49  \begin{defn}  Ralf Jung committed Dec 05, 2016 50  A (bi)functor $F : \OFEs \to \OFEs$ 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 51 52  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 11, 2016 53 The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.  Ralf Jung committed Mar 11, 2016 54 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 Dec 05, 2016 55   Ralf Jung committed Dec 08, 2017 56 57 58 59 60 61 62 63 64 65 One very important OFE is the OFE of \emph{step-indexed propositions}: For every step-index, such a proposition either holds or does not hold. Moreover, if a propositions holds for some $n$, it also has to hold for all smaller step-indices. \begin{align*} \SProp \eqdef{}& \psetdown{\nat} \\ \eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\ X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \\ X \nincl{n} Y \eqdef{}& \All m \leq n. m \in X \Ra m \in Y \end{align*}  Ralf Jung committed Dec 05, 2016 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 \subsection{COFE} COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains. \begin{defn}[Chain] 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)$. \end{defn} \begin{defn} A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \chain(\cofe) \to \cofe)$ satisfying \begin{align*} \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl} \end{align*} \end{defn} \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn} The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).  Robbert Krebbers committed Dec 10, 2017 86 $\SProp$ as defined above is complete, \ie it is a COFE.  Ralf Jung committed Dec 05, 2016 87 88 89  Completeness is necessary to take fixed-points.  Robbert Krebbers committed Dec 10, 2017 90 91 92 \begin{thm}[Banach's fixed-point] \label{thm:banach} Given an inhabited COFE $\ofe$ and a contractive function $f : \ofe \to \ofe$, there exists a unique fixed-point $\fixp_T f$ such that $f(\fixp_T f) = \fixp_T f$.  93 Moreover, this theorem also holds if $f$ is just non-expansive, and $f^k$ is contractive for an arbitrary $k$.  Robbert Krebbers committed Dec 10, 2017 94 95 96 97 98 99 100 101 \end{thm} \begin{thm}[America and Rutten~\cite{America-Rutten:JCSS89,birkedal:metric-space}] \label{thm:america_rutten} Let $1$ be the discrete COFE on the unit type: $1 \eqdef \Delta \{ () \}$. Given a locally contractive bifunctor $G : \COFEs^{\textrm{op}} \times \COFEs \to \COFEs$, and provided that $$G(1, 1)$$ is inhabited, then there exists a unique\footnote{Uniqueness is not proven in Coq.} COFE $\ofe$ such that $G(\ofe^{\textrm{op}}, \ofe) \cong \ofe$ (\ie the two are isomorphic in $\COFEs$). \end{thm}  Ralf Jung committed Mar 07, 2016 102 103 104  \subsection{RA}  Ralf Jung committed Mar 12, 2016 105 106 \begin{defn} A \emph{resource algebra} (RA) is a tuple \\  Ralf Jung committed Dec 08, 2017 107  $(\monoid, \mvalFull : \monoid \to \mProp, \mcore{{-}}:  Ralf Jung committed Jul 25, 2016 108  \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:  Ralf Jung committed Mar 12, 2016 109 110 111  \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 112 113 114  \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 Dec 08, 2017 115  \All \melt, \meltB.& \mvalFull(\melt \mtimes \meltB) \Ra \mvalFull(\melt) \tagH{ra-valid-op} \\  Ralf Jung committed Mar 12, 2016 116  \text{where}\qquad %\qquad\\  Ralf Jung committed Jul 25, 2016 117  \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 118  \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}  Ralf Jung committed Mar 12, 2016 119 120  \end{align*} \end{defn}  Ralf Jung committed Dec 08, 2017 121 122 123 Here, $\mProp$ is the set of (meta-level) propositions. Think of \texttt{Prop} in Coq or $\mathbb{B}$ in classical mathematics.  Ralf Jung committed Mar 15, 2016 124 125 RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences: \begin{enumerate}  Ralf Jung committed Dec 08, 2017 126 127 \item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}). These valid elements are identified by the \emph{validity predicate} $\mvalFull$.  Ralf Jung committed Mar 15, 2016 128   Ralf Jung committed Jul 25, 2016 129 130 131 132 133 134 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 135  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 136 137 138 139 140 141 142 % (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 143 144 \end{enumerate}  Ralf Jung committed Mar 12, 2016 145 146 147  \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 Dec 08, 2017 148  $\All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \mvalFull(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \mvalFull(\maybe{\melt_\f})$  Ralf Jung committed Mar 12, 2016 149 150 151  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn}  Ralf Jung committed Jul 25, 2016 152 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 153 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 154 155 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 156   Ralf Jung committed Feb 29, 2016 157 158 159 \subsection{CMRA} \begin{defn}  Ralf Jung committed Dec 08, 2017 160  A \emph{CMRA} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:  Ralf Jung committed Feb 29, 2016 161 162 163  \begin{align*} \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 164 165 166  \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 Dec 08, 2017 167 168  \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{cmra-valid-op} \\ \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\  Ralf Jung committed Feb 29, 2016 169 170  &\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 171  \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\  Ralf Jung committed Mar 12, 2016 172  \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}  Ralf Jung committed Feb 29, 2016 173 174 175  \end{align*} \end{defn}  Ralf Jung committed Dec 05, 2016 176 This is a natural generalization of RAs over OFEs.  Ralf Jung committed Mar 10, 2016 177 All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.  Ralf Jung committed Dec 08, 2017 178 179 We define the plain $\mvalFull$ as the limit'' of the step-indexed approximation: $\mvalFull(\melt) \eqdef \All n. n \in \mval(\melt)$  Ralf Jung committed Feb 29, 2016 180 181 182 183 184  \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 185 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 186 187 188 189 190 191 192 193 194 195 196 197 198 199 \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 200 This operation is needed to prove that $\later$ commutes with separating conjunction:  Ralf Jung committed Feb 29, 2016 201 \begin{mathpar}  Ralf Jung committed Jul 25, 2016 202  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}  Ralf Jung committed Feb 29, 2016 203 204 \end{mathpar}  Ralf Jung committed Mar 08, 2016 205 206 207 \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 Dec 08, 2017 208  \item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$  Ralf Jung committed Mar 08, 2016 209  \item $\munit$ is a left-identity of the operation: \\  Ralf Jung committed Mar 08, 2016 210  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Jul 25, 2016 211  \item $\munit$ is its own core: \\ $\mcore\munit = \munit$  Ralf Jung committed Mar 08, 2016 212 213 214  \end{enumerate} \end{defn}  Ralf Jung committed Jul 25, 2016 215 \begin{lem}\label{lem:cmra-unit-total-core}  Ralf Jung committed Jul 25, 2016 216 217 218  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 219 220 \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 Dec 08, 2017 221  $\All n, \maybe{\melt_\f}. n \in \mval(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. n \in\mval(\meltB \mtimes \maybe{\melt_\f})$  Ralf Jung committed Mar 07, 2016 222 223 224 225 226  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 227 228 229 230 \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 231  \item $\mval$ ignores the step-index: \\  Ralf Jung committed Dec 08, 2017 232  $\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$  Ralf Jung committed Mar 08, 2016 233 234 235 236  \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 237   Ralf Jung committed Nov 23, 2017 238 239 \begin{defn}[CMRA homomorphism] A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{a CMRA homomorphism} if it satisfies the following conditions:  Ralf Jung committed Mar 08, 2016 240  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 241  \item $f$ is non-expansive  Ralf Jung committed Nov 23, 2017 242 243 244 245  \item $f$ commutes with composition:\\ $\All \melt_1 \in \monoid_1, \melt_2 \in \monoid_1. f(\melt_1) \mtimes f(\melt_2) = f(\melt_1 \mtimes \melt_2)$ \item $f$ commutes with the core:\\ $\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$  Ralf Jung committed Mar 07, 2016 246  \item $f$ preserves validity: \\  Ralf Jung committed Dec 08, 2017 247  $\All n, \melt \in \monoid_1. n \in \mval(\melt) \Ra n \in \mval(f(\melt))$  Ralf Jung committed Mar 07, 2016 248 249 250 251 252 253  \end{enumerate} \end{defn} \begin{defn} The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows. \end{defn}  Ralf Jung committed Dec 05, 2016 254 Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.  Ralf Jung committed Mar 09, 2016 255 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Aug 04, 2016 256 %TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.  Ralf Jung committed Feb 29, 2016 257   Ralf Jung committed Jan 31, 2016 258 259 260 261 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: