algebra.tex 13.6 KB
Newer Older
1
\section{Algebraic Structures}
2

3 4
\subsection{COFE}

5
The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
6
This definition varies slightly from the original one in~\cite{catlogic}.
7

8
\begin{defn}[Chain]
Robbert Krebbers's avatar
Robbert Krebbers committed
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)$.
10 11
\end{defn}

12
\begin{defn}
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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's avatar
Ralf Jung committed
18
    \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
19 20 21
  \end{align*}
\end{defn}

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}).
25

26
\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
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\]
29
  A COFE $A$ is called \emph{discrete} if all its elements are discrete.
30 31
  For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$

32 33 34
\end{defn}

\begin{defn}
35
  A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
Ralf Jung's avatar
Ralf Jung committed
36
  \[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
37
  It is \emph{contractive} if
Ralf Jung's avatar
Ralf Jung committed
38
  \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
39
\end{defn}
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$.
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))$.
43 44 45 46

\begin{defn}
  The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
\end{defn}
Ralf Jung's avatar
Ralf Jung committed
47

Ralf Jung's avatar
Ralf Jung committed
48
Note that $\COFEs$ is cartesian closed. In particular:
Ralf Jung's avatar
Ralf Jung committed
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}
55 56

\begin{defn}
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.
58 59
  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
Ralf Jung's avatar
Ralf Jung committed
60
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Ralf Jung's avatar
Ralf Jung committed
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.
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.
63 64 65

\subsection{RA}

Ralf Jung's avatar
Ralf Jung committed
66 67
\begin{defn}
  A \emph{resource algebra} (RA) is a tuple \\
68 69
  $(\monoid, \mval \subseteq \monoid, \mcore{{-}}:
  \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
Ralf Jung's avatar
Ralf Jung committed
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} \\
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's avatar
Ralf Jung committed
76 77
    \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
    \text{where}\qquad %\qquad\\
78
    \maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
79
    \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
Ralf Jung's avatar
Ralf Jung committed
80 81
  \end{align*}
\end{defn}
82 83 84
\noindent
RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
\begin{enumerate}
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}).
86

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}).

93
  Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.
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.
101 102
\end{enumerate}

Ralf Jung's avatar
Ralf Jung committed
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
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's avatar
Ralf Jung committed
107 108 109

  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
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$.
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.
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's avatar
Ralf Jung committed
114

115 116 117
\subsection{CMRA}

\begin{defn}
Robbert Krebbers's avatar
Robbert Krebbers committed
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:
119
  \begin{align*}
Ralf Jung's avatar
Ralf Jung committed
120
    \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
121
    \All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
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} \\
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's avatar
Ralf Jung committed
127
    \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
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\\
131
    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\
132
    \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}
133 134 135
  \end{align*}
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
138
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
Robbert Krebbers's avatar
Robbert Krebbers committed
139
\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
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's avatar
Ralf Jung committed
145
% RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so
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$.
160
This operation is needed to prove that $\later$ commutes with separating conjunction:
161
\begin{mathpar}
162
  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
163 164
\end{mathpar}

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's avatar
Ralf Jung committed
168 169
  \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
  \item $\munit$ is a left-identity of the operation: \\
170
    $\All \melt \in M. \munit \mtimes \melt = \melt$
171
  \item $\munit$ is its own core: \\ $\mcore\munit = \munit$
172 173 174
  \end{enumerate}
\end{defn}

175
\begin{lem}\label{lem:cmra-unit-total-core}
176 177 178
  If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
\end{lem}

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
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 \]
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
191
  \item $\mval$ ignores the step-index: \\
Ralf Jung's avatar
Ralf Jung committed
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$.
197 198

\begin{defn}
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:
200
  \begin{enumerate}[itemsep=0pt]
201 202
  \item $f$ is non-expansive
  \item $f$ preserves validity: \\
Ralf Jung's avatar
Ralf Jung committed
203
    $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
204
  \item $f$ preserves CMRA inclusion:\\
205
    $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
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}
212
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
Ralf Jung's avatar
Ralf Jung committed
213
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
Ralf Jung's avatar
Ralf Jung committed
214
%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
215

216 217 218 219
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "iris"
%%% End: