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

3
4
\subsection{COFE}

5
This definition varies slightly from the original one in~\cite{catlogic}.
Ralf Jung's avatar
Ralf Jung committed
6
\begin{defn}[Chain]
Ralf Jung's avatar
Ralf Jung committed
7
  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's avatar
Ralf Jung committed
8
9
\end{defn}

10
\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
11
  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
12
13
14
15
  \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
16
    \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}
17
18
19
20
21
  \end{align*}
\end{defn}

\ralf{Copy the explanation from the paper, when that one is more polished.}

Ralf Jung's avatar
Ralf Jung committed
22
\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
23
24
  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's avatar
Ralf Jung committed
25
26
27
28
  A COFE $A$ is called \emph{discrete} if all its elements are discrete.
\end{defn}

\begin{defn}
29
  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
30
  \[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
Ralf Jung's avatar
Ralf Jung committed
31
  It is \emph{contractive} if
Ralf Jung's avatar
Ralf Jung committed
32
  \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
Ralf Jung's avatar
Ralf Jung committed
33
34
35
36
37
\end{defn}

\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
38
39
40
41
42
43
44
45

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's avatar
Ralf Jung committed
46
47

\begin{defn}
48
  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's avatar
Ralf Jung committed
49
50
  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
Ralf Jung's avatar
Ralf Jung committed
51
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Ralf Jung's avatar
Ralf Jung committed
52
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.
53
54
55

\subsection{RA}

Ralf Jung's avatar
Ralf Jung committed
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
\begin{defn}
  A \emph{resource algebra} (RA) is a tuple \\
  $(\monoid, \mval \subseteq \monoid, \mcore{-}:
  \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying
  \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} \\
    \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
    \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
    \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
    \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
    \text{where}\qquad %\qquad\\
    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
  \end{align*}
\end{defn}

\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 \melt_f. \melt \mtimes \melt_f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval \]

  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}


\ralf{Copy the explanation from the paper, when that one is more polished.}
Ralf Jung's avatar
Ralf Jung committed
81

82
83
84
\subsection{CMRA}

\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
85
  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)$ satisfying
86
  \begin{align*}
Ralf Jung's avatar
Ralf Jung committed
87
    \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
88
89
90
    \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's avatar
Ralf Jung committed
91
92
    \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
    \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
93
    \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
Ralf Jung's avatar
Ralf Jung committed
94
    \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
95
96
97
    \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\\
98
99
    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}\\
    \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}
100
101
102
  \end{align*}
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
103
104
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
105
106
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\[ \mval \eqdef \bigcap_{n \in \mathbb{N}} \mval_n \]
107
108
109
110
111

\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
112
% RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
\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's avatar
Ralf Jung committed
129
  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}
130
131
  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
132
(This assumes that the type $\type$ is non-empty.)
133

134
135
136
\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
137
138
  \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
  \item $\munit$ is a left-identity of the operation: \\
139
    $\All \melt \in M. \munit \mtimes \melt = \melt$
Ralf Jung's avatar
Ralf Jung committed
140
  \item $\munit$ is a discrete COFE element
141
142
143
  \end{enumerate}
\end{defn}

144
145
146
147
148
149
150
151
\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's avatar
Ralf Jung committed
152
153
154
155
156
157
158
159
160
161
\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$
  \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's avatar
Ralf Jung committed
162
163

\begin{defn}
164
  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:
165
  \begin{enumerate}[itemsep=0pt]
Ralf Jung's avatar
Ralf Jung committed
166
167
  \item $f$ is non-expansive
  \item $f$ preserves validity: \\
Ralf Jung's avatar
Ralf Jung committed
168
    $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
Ralf Jung's avatar
Ralf Jung committed
169
  \item $f$ preserves CMRA inclusion:\\
170
    $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
Ralf Jung's avatar
Ralf Jung committed
171
172
173
174
175
176
177
  \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's avatar
Ralf Jung committed
178
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
Ralf Jung's avatar
Ralf Jung committed
179

180

181
182
183
184
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "iris"
%%% End: