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

3
4
\subsection{COFE}

Ralf Jung's avatar
Ralf Jung committed
5
\begin{defn}[Chain]
Ralf Jung's avatar
Ralf Jung committed
6
  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
7
8
\end{defn}

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

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

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

\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
28
29
  A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} if
  \[\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
30
  It is \emph{contractive} if
Ralf Jung's avatar
Ralf Jung committed
31
  \[ \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
32
33
34
35
36
37
38
39
40
41
42
\end{defn}

\begin{defn}
  The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
\end{defn}
Note that $\COFEs$ is cartesian closed.

\begin{defn}
  A functor $F : \COFEs \to COFEs$ is called \emph{locally non-expansive} if its actions $F_1$ on arrows is itself a non-expansive map.
  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
43
44
45
46

\subsection{RA}

\ralf{Define this, including frame-preserving updates.}
Ralf Jung's avatar
Ralf Jung committed
47

48
49
50
\subsection{CMRA}

\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
51
  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying
52
53
54
55
  \begin{align*}
    \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
56
57
58
59
    \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
    \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
    \All \melt, \meltB.& \melt \leq \meltB \Ra \mcore\melt \leq \mcore\meltB \tagH{cmra-core-mono} \\
    \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
60
61
62
63
64
65
66
67
68
69
    \All \melt, \meltB.& \melt \leq \meltB \Ra \melt \mtimes (\meltB \mdiv \melt) = \meltB \tagH{cmra-div-op} \\
    \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\\
    \melt \leq \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}
  \end{align*}
\end{defn}

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

Ralf Jung's avatar
wording    
Ralf Jung committed
70
\paragraph{The division operator $\mdiv$.}
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt \leq \meltB$, then $\melt \mdiv \meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}).
Otherwise, $\mdiv$ can have arbitrary behavior.
This means that, in classical logic, the division operator can be defined for any PCM using the axiom of choice, and it will trivially satisfy \ruleref{cmra-div-op}.
However, notice that the division operator also has to be \emph{non-expansive} --- so if the carrier $\monoid$ is equipped with a non-trivial $\nequiv{n}$, there is an additional proof obligation here.
This is crucial, for the following reason:
Considering that the extension order is defined using \emph{equality}, there is a natural notion of a \emph{step-indexed extension} order using the step-indexed equivalence of the underlying COFE:
\[ \melt \mincl{n} \meltB \eqdef \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclM} \]
One of the properties we would expect to hold is the usual correspondence between a step-indexed predicate and its non-step-indexed counterpart:
\[ \All \melt, \meltB. \melt \leq \meltB \Lra (\All n. \melt \mincl{n} \meltB) \tagH{cmra-incl-limit} \]
The right-to-left direction here is trick.
For every $n$, we obtain a proof that $\melt \mincl{n} \meltB$.
From this, we could extract a sequence of witnesses $(\meltC_m)_{m}$, and we need to arrive at a single witness $\meltC$ showing that $\melt \leq \meltB$.
Without the division operator, there is no reason to believe that such a witness exists.
However, since we can use the division operator, and since we know that this operator is \emph{non-expansive}, we can pick $\meltC \eqdef \meltB \mdiv \melt$, and then we can prove that this is indeed the desired witness.
\ralf{Do we actually need this property anywhere?}

\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{Needs some magic to fix the baseline of the $\nequiv{n}$, or so}
\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
108
  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}
109
110
  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
111
(This assumes that the type $\type$ is non-empty.)
112

113
114
115
\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
116
117
  \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
  \item $\munit$ is a left-identity of the operation: \\
118
    $\All \melt \in M. \munit \mtimes \melt = \melt$
Ralf Jung's avatar
Ralf Jung committed
119
  \item $\munit$ is a discrete COFE element
120
121
122
  \end{enumerate}
\end{defn}

123
124
125
126
127
128
129
130
\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
131
132
133
134
135
136
137
\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$
  \item $f$ preserves CMRA inclusion:\\
Ralf Jung's avatar
Ralf Jung committed
138
    $\All \melt \in \monoid, \meltB \in \monoid. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$
Ralf Jung's avatar
Ralf Jung committed
139
140
141
142
  \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
143
144

\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
145
  A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{monotone} if it satisfies the following conditions:
146
  \begin{enumerate}[itemsep=0pt]
Ralf Jung's avatar
Ralf Jung committed
147
148
  \item $f$ is non-expansive
  \item $f$ preserves validity: \\
Ralf Jung's avatar
Ralf Jung committed
149
    $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
Ralf Jung's avatar
Ralf Jung committed
150
  \item $f$ preserves CMRA inclusion:\\
Ralf Jung's avatar
Ralf Jung committed
151
    $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$
Ralf Jung's avatar
Ralf Jung committed
152
153
154
155
156
157
158
159
160
  \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$.
The notion of a locally non-expansive (or contractive) functor naturally generalizes to functors between these categories.

161

162
163
164
165
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "iris"
%%% End: