constructions.tex 17.9 KB
Newer Older
1
\section{OFE and COFE constructions}
2

3
4
\subsection{Trivial pointwise lifting}

5
The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
6
7
This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe + \cofe'$ and finite partial functions $K \fpfn \monoid$ (with $K$ infinite countable).

Ralf Jung's avatar
Ralf Jung committed
8
9
\subsection{Next (type-level later)}

10
Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
Ralf Jung's avatar
Ralf Jung committed
11
\begin{align*}
12
  \latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
Ralf Jung's avatar
Ralf Jung committed
13
14
  \latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
\end{align*}
15
16
Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a constructor (like the constructors in Coq), \ie this is short for $\setComp{\latertinj(x)}{x \in \cofe}$.

17
$\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
Ralf Jung's avatar
Ralf Jung committed
18

19

Ralf Jung's avatar
Ralf Jung committed
20
21
22
23
\subsection{Uniform Predicates}

Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\begin{align*}
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  \UPred(\monoid) \eqdef{} \setComp{\pred: \nat \times \monoid \to \mProp}{
Ralf Jung's avatar
Ralf Jung committed
25
26
27
28
29
30
31
32
33
34
  \begin{inbox}[c]
    (\All n, x, y. \pred(n, x) \land x \nequiv{n} y \Ra \pred(n, y)) \land {}\\
    (\All n, m, x, y. \pred(n, x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra \pred(m, y))
  \end{inbox}
}
\end{align*}
where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.

One way to understand this definition is to re-write it a little.
35
We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, the proposition either holds or does not hold.
Ralf Jung's avatar
Ralf Jung committed
36
\begin{align*}
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  \SProp \eqdef{}& \psetdown{\nat} \\
    \eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
Ralf Jung's avatar
Ralf Jung committed
39
  X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y
Ralf Jung's avatar
Ralf Jung committed
40
\end{align*}
41
Notice that this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
Ralf Jung's avatar
Ralf Jung committed
42
We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
Ralf Jung's avatar
Ralf Jung committed
43

Ralf Jung's avatar
Ralf Jung committed
44
45
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
46
  \UPred(\monoid) \cong{}& \monoid \monra \SProp \\
Ralf Jung's avatar
Ralf Jung committed
47
48
49
     \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)}
\end{align*}
The reason we chose the first definition is that it is easier to work with in Coq.
Ralf Jung's avatar
Ralf Jung committed
50
51

\clearpage
52
\section{RA and CMRA constructions}
53

Ralf Jung's avatar
Ralf Jung committed
54
55
56
\subsection{Product}
\label{sec:prodm}

57
Given a family $(M_i)_{i \in I}$ of CMRAs ($I$ finite), we construct a CMRA for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
Ralf Jung's avatar
Ralf Jung committed
58
59
60
61
62

Frame-preserving updates on the $M_i$ lift to the product:
\begin{mathpar}
  \inferH{prod-update}
  {\melt \mupd_{M_i} \meltsB}
63
  {\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
Ralf Jung's avatar
Ralf Jung committed
64
65
\end{mathpar}

66
67
68
\subsection{Sum}
\label{sec:summ}

69
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
70
\begin{align*}
71
72
73
  \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
  \mval_n \eqdef{}& \setComp{\cinl(\melt_1)}{\melt_1 \in \mval'_n}
    \cup \setComp{\cinr(\melt_2)}{\melt_2 \in \mval''_n}  \\
74
75
76
77
78
79
  \cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1)  \\
%  \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
%  \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
  \mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
\end{align*}
The composition and core for $\cinr$ are defined symmetrically.
80
The remaining cases of the composition and core are all $\mundef$.
81
82
Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.

83
84
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this CMRA just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.

85
86
87
88
89
90
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
  \infer{x \nequiv{n} y}{\cinl(x) \nequiv{n} \cinl(y)}

  \infer{x \nequiv{n} y}{\cinr(x) \nequiv{n} \cinr(y)}

91
  \axiom{\mundef \nequiv{n} \mundef}
92
93
94
\end{mathpar}


95
96
97
98
99
100
101
102
103
104
105
106
We obtain the following frame-preserving updates, as well as their symmetric counterparts:
\begin{mathpar}
  \inferH{sum-update}
  {\melt \mupd_{M_1} \meltsB}
  {\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}

  \inferH{sum-swap}
  {\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
  {\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.

107
108
109
110
111
112
113
114
\subsection{Option}

The definition of the (CM)RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$.
We can easily extend this to a full CMRA by defining a suitable core, namely
\begin{align*}
  \mcore{\mnocore} \eqdef{}& \mnocore & \\
  \mcore{\maybe\melt} \eqdef{}& \mcore\melt & \text{If $\maybe\melt \neq \mnocore$}
\end{align*}
115
Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\mathord{\maybe\monoid}}$).
116

Ralf Jung's avatar
Ralf Jung committed
117
118
119
\subsection{Finite partial function}
\label{sec:fpfnm}

120
Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a CMRA structure by lifting everything pointwise.
Ralf Jung's avatar
Ralf Jung committed
121
122
123
124
125

We obtain the following frame-preserving updates:
\begin{mathpar}
  \inferH{fpfn-alloc-strong}
  {\text{$G$ infinite} \and \melt \in \mval}
126
  {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
Ralf Jung's avatar
Ralf Jung committed
127
128
129

  \inferH{fpfn-alloc}
  {\melt \in \mval}
130
  {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
Ralf Jung's avatar
Ralf Jung committed
131
132

  \inferH{fpfn-update}
133
  {\melt \mupd_\monoid \meltsB}
134
  {\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
Ralf Jung's avatar
Ralf Jung committed
135
\end{mathpar}
136
Above, $\mval$ refers to the validity of $\monoid$.
137

Ralf Jung's avatar
Ralf Jung committed
138
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
Ralf Jung's avatar
Ralf Jung committed
139

140
141
\subsection{Agreement}

142
Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
Ralf Jung's avatar
Ralf Jung committed
143
\begin{align*}
144
145
146
147
  \agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{c \neq \emptyset} /\ {\sim} \\[-0.2em]
  \melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\
  \textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB  \\
~\\
148
%    \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
149
  \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ \All x, y \in \melt. x \nequiv{n} y } \\
Ralf Jung's avatar
Ralf Jung committed
150
  \mcore\melt \eqdef{}& \melt \\
151
  \melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
Ralf Jung's avatar
Ralf Jung committed
152
\end{align*}
153
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
154

155
$\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
Ralf Jung's avatar
Ralf Jung committed
156

157
158
We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
\[ \aginj(x) \eqdef \set{x} \]
Ralf Jung's avatar
Ralf Jung committed
159
160
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
161
  \axiomH{ag-val}{\aginj(x) \in \mval_n}
162

Ralf Jung's avatar
Ralf Jung committed
163
  \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
164
  
165
  \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Lra x \nequiv{n} y}
Ralf Jung's avatar
Ralf Jung committed
166
167
\end{mathpar}

168

Ralf Jung's avatar
Ralf Jung committed
169
170
\subsection{Exclusive CMRA}

171
Given an OFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
Ralf Jung's avatar
Ralf Jung committed
172
\begin{align*}
173
174
  \exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
  \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \mundef}
Ralf Jung's avatar
Ralf Jung committed
175
\end{align*}
176
All cases of composition go to $\mundef$.
Ralf Jung's avatar
Ralf Jung committed
177
\begin{align*}
178
  \mcore{\exinj(x)} \eqdef{}& \mnocore &
179
  \mcore{\mundef} \eqdef{}& \mundef
Ralf Jung's avatar
Ralf Jung committed
180
\end{align*}
181
182
Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.

Ralf Jung's avatar
Ralf Jung committed
183
184
185
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
  \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
186

187
  \axiom{\mundef \nequiv{n} \mundef}
Ralf Jung's avatar
Ralf Jung committed
188
\end{mathpar}
189
$\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
Ralf Jung's avatar
Ralf Jung committed
190
191
192
193
194
195
196
197
198
199

We obtain the following frame-preserving update:
\begin{mathpar}
  \inferH{ex-update}{}
  {\exinj(x) \mupd \exinj(y)}
\end{mathpar}



%TODO: These need syncing with Coq
200
201
202
203
204
205
206
207
208
209
210
211
212
213
% \subsection{Finite Powerset Monoid}

% Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
% \[
% \melt \cdot \meltB \;\eqdef\; \melt \cup \meltB \quad \mbox{if } \melt \cap \meltB = \emptyset
% \]

% We obtain:
% \begin{mathpar}
% 	\inferH{PowFinUpd}{}
% 		{\emptyset \mupd \{ \{x\} \mid x \in X  \}}
% \end{mathpar}

% \begin{proof}[Proof of \ruleref{PowFinUpd}]
Ralf Jung's avatar
Ralf Jung committed
214
% 	Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$.
215
216
217
218
219
% 	Pick that for the result.
% \end{proof}

% The powerset monoids is cancellative.
% \begin{proof}[Proof of cancellativity]
Ralf Jung's avatar
Ralf Jung committed
220
221
222
223
% 	Let $\melt_\f \mtimes \melt = \melt_\f \mtimes \meltB \neq \mzero$.
% 	So we have $\melt_\f \sep \melt$ and $\melt_\f \sep \meltB$, and we have to show $\melt = \meltB$.
% 	Assume $x \in \melt$. Hence $x \in \melt_\f \mtimes \melt$ and thus $x \in \melt_\f \mtimes \meltB$.
% 	By disjointness, $x \notin \melt_\f$ and hence $x \in meltB$.
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
% 	The other direction works the same way.
% \end{proof}


% \subsection{Fractional monoid}
% \label{sec:fracm}

% Given a monoid $M$, we define a monoid representing fractional ownership of some piece $\melt \in M$.
% The idea is to preserve all the frame-preserving update that $M$ could have, while additionally being able to do \emph{any} update if we own the full state (as determined by the fraction being $1$).
% Let $\fracm{M}$ be the monoid with carrier $(((0, 1] \cap \mathbb{Q}) \times M) \uplus \{\munit\}$ and multiplication
% \begin{align*}
%  (q, a) \mtimes (q', a') &\eqdef (q + q', a \mtimes a') \qquad \mbox{if $q+q'\le 1$} \\
%  (q, a) \mtimes \munit &\eqdef (q,a) \\
%  \munit \mtimes (q,a) &\eqdef (q,a).
% \end{align*}

% We get the following frame-preserving update.
% \begin{mathpar}
% 	\inferH{FracUpdFull}
% 		{a, b \in M}
% 		{(1, a) \mupd (1, b)}
%   \and\inferH{FracUpdLocal}
% 	  {a \mupd_M B}
% 	  {(q, a) \mupd \{q\} \times B}
% \end{mathpar}

% \begin{proof}[Proof of \ruleref{FracUpdFull}]
% Assume some $f \sep (1, a)$. This can only be $f = \munit$, so showing $f \sep (1, b)$ is trivial.
% \end{proof}

% \begin{proof}[Proof of \ruleref{FracUpdLocal}]
% 	Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$.
256
	
Ralf Jung's avatar
Ralf Jung committed
257
258
% 	In the interesting case, we have $f = (q_\f, a_\f)$.
% 	Obtain $b$ such that $b \in B \land b \sep a_\f$.
259
260
261
262
263
% 	Then $(q, b) \sep f$, and we are done.
% \end{proof}

% $\fracm{M}$ is cancellative if $M$ is cancellative.
% \begin{proof}[Proof of cancellativitiy]
Ralf Jung's avatar
Ralf Jung committed
264
265
% If $\melt_\f = \munit$, we are trivially done.
% So let $\melt_\f = (q_\f, \melt_\f')$.
266
267
268
269
% If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up.
% Again, we are trivially done.
% Similar so for $\meltB = \munit$.
% So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$.
Ralf Jung's avatar
Ralf Jung committed
270
% We have $(q_\f + q_a, \melt_\f' \mtimes \melt') = (q_\f + q_b, \melt_\f' \mtimes \meltB')$.
271
272
273
274
275
% We have to show $q_a = q_b$ and $\melt' = \meltB'$.
% The first is trivial, the second follows from cancellativitiy of $M$.
% \end{proof}


Ralf Jung's avatar
Ralf Jung committed
276
277
\subsection{Authoritative}
\label{sec:auth-cmra}
278

Ralf Jung's avatar
Ralf Jung committed
279
Given a CMRA $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$.
Ralf Jung's avatar
Ralf Jung committed
280
281
282
283
284
285
286
287
288
289
We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
\begin{align*}
\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
\mval_n \eqdef{}& \setComp{ (x, \meltB) \in \authm(M) }{ \meltB \in \mval_n \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
  (x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
  \mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
  (x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
\end{align*}
Note that $(\mnocore, \munit)$ is the unit and asserts no ownership whatsoever, but $(\exinj(\munit), \munit)$ asserts that the authoritative element is $\munit$.
290

Ralf Jung's avatar
Ralf Jung committed
291
292
Let $\melt, \meltB \in M$.
We write $\authfull \melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag \meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull \melt , \authfrag \meltB$ for combined ownership $(\exinj(\melt), \meltB)$.
293

Ralf Jung's avatar
Ralf Jung committed
294
295
296
297
298
299
300
The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
  It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
  \[ \All n, \maybe{\melt_\f}. x_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
301

Ralf Jung's avatar
Ralf Jung committed
302
303
304
305
306
307
We then obtain
\begin{mathpar}
  \inferH{auth-update}
  {(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)}
  {\authfull \melt_1 , \authfrag \meltB_1 \mupd \authfull \melt_2 , \authfrag \meltB_2}
\end{mathpar}
308

309
\subsection{STS with tokens}
Ralf Jung's avatar
Ralf Jung committed
310
\label{sec:sts-cmra}
311

Ralf Jung's avatar
Ralf Jung committed
312
Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
313

314
315
316
317
The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
\begin{align*}
 (s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
Ralf Jung's avatar
Ralf Jung committed
318
 s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \land (s, T_1) \stsstep (s', T_2)
319
\end{align*}
320

321
322
We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
323
\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \left(\All s'. s \stsfstep{T} s' \Ra s' \in S\right) \\
324
325
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*}
326

327
328
The STS RA is defined as follows
\begin{align*}
329
330
  \monoid \eqdef{}& \STSauth(s:\STSS, T:\wp(\STST) \mid \STSL(s) \disj T) \mid{}\\& \STSfrag(S: \wp(\STSS), T: \wp(\STST) \mid \STSclsd(S, T) \land S \neq \emptyset) \mid \mundef \\
  \mval \eqdef{}& \setComp{\melt\in\monoid}{\melt \neq \mundef} \\
Ralf Jung's avatar
Ralf Jung committed
331
332
  \STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
  \STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
333
334
335
  \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
  \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*}
336
The remaining cases are all $\mundef$.
337

338
339
340
341
We will need the following frame-preserving update:
\begin{mathpar}
  \inferH{sts-step}{(s, T) \ststrans (s', T')}
  {\STSauth(s, T) \mupd \STSauth(s', T')}
342

343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
  \inferH{sts-weaken}
  {\STSclsd(S_2, T_2) \and S_1 \subseteq S_2 \and T_2 \subseteq T_1}
  {\STSfrag(S_1, T_1) \mupd \STSfrag(S_2, T_2)}
\end{mathpar}

\paragraph{The core is not a homomorphism.}
The core of the STS construction is only satisfying the RA axioms because we are \emph{not} demanding the core to be a homomorphism---all we demand is for the core to be monotone with respect the \ruleref{ra-incl}.

In other words, the following does \emph{not} hold for the STS core as defined above:
\[ \mcore\melt \mtimes \mcore\meltB = \mcore{\melt\mtimes\meltB} \]

To see why, consider the following STS:
\newcommand\st{\textlog{s}}
\newcommand\tok{\textmon{t}}
\begin{center}
  \begin{tikzpicture}[sts]
    \node at (0,0)   (s1) {$\st_1$};
    \node at (3,0)  (s2) {$\st_2$};
    \node at (9,0) (s3) {$\st_3$};
    \node at (6,0)  (s4) {$\st_4$\\$[\tok_1, \tok_2]$};
    
    \path[sts_arrows] (s2) edge  (s4);
    \path[sts_arrows] (s3) edge  (s4);
  \end{tikzpicture}
\end{center}
Now consider the following two elements of the STS RA:
\[ \melt \eqdef \STSfrag(\set{\st_1,\st_2}, \set{\tok_1}) \qquad\qquad
  \meltB \eqdef \STSfrag(\set{\st_1,\st_3}, \set{\tok_2}) \]

We have:
\begin{mathpar}
  {\melt\mtimes\meltB = \STSfrag(\set{\st_1}, \set{\tok_1, \tok_2})}
375

376
377
378
379
380
381
382
  {\mcore\melt = \STSfrag(\set{\st_1, \st_2, \st_4}, \emptyset)}

  {\mcore\meltB = \STSfrag(\set{\st_1, \st_3, \st_4}, \emptyset)}

  {\mcore\melt \mtimes \mcore\meltB = \STSfrag(\set{\st_1, \st_4}, \emptyset) \neq
    \mcore{\melt \mtimes \meltB} = \STSfrag(\set{\st_1}, \emptyset)}
\end{mathpar}
383
384
385
386
387

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "iris"
%%% End: