constructions.tex 18 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
\section{OFE and COFE Constructions}
2

Ralf Jung's avatar
Ralf Jung committed
3
\subsection{Trivial Pointwise Lifting}
4

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
\subsection{Next (Type-Level Later)}
Ralf Jung's avatar
Ralf Jung committed
9

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

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

22
Given a camera $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
Ralf Jung's avatar
Ralf Jung committed
23
\begin{align*}
24 25 26 27 28
\monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}
{\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\
  \UPred(\monoid) \eqdef{}&  \faktor{\monoid \monnra \SProp}{\equiv} \\
  \pred \equiv \predB \eqdef{}& \All m, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff  m \in \predB(\melt)) \\
  \pred \nequiv{n} \predB \eqdef{}& \All m \le n, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff  m \in \predB(\melt))
Ralf Jung's avatar
Ralf Jung committed
29
\end{align*}
30
You can think of uniform predicates as monotone, step-indexed predicates over a camera that ``ignore'' invalid elements (as defined by the quotient).
Ralf Jung's avatar
Ralf Jung committed
31

32
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
Ralf Jung's avatar
Ralf Jung committed
33

Ralf Jung's avatar
Ralf Jung committed
34 35 36
It is worth noting that the above quotient admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element $P_0$ such that:
Ralf Jung's avatar
Ralf Jung committed
37 38 39
\begin{align*}
  \All n, \melt.  (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt)  \tagH{UPred-canonical}
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
40 41 42 43 44 45 46 47 48 49 50 51 52
Intuitively, this says that $P_0$ trivially holds whenever the resource is invalid.
Starting from any element $P$, one can find this canonical
representative by choosing $P_0(\melt) := \setComp{n}{n \in \mval(\melt) \Ra n \in P(\melt)}$.

Hence, as an alternative definition of $\UPred$, we could use the set
of canonical representatives. This alternative definition would
save us from using a quotient. However, the definitions of the various
connectives would get more complicated, because we have to make sure
they all verify \ruleref{UPred-canonical}, which sometimes requires some adjustments. We
would moreover need to prove one more property for every logical
connective.


Ralf Jung's avatar
Ralf Jung committed
53
\clearpage
54
\section{RA and Camera Constructions}
55

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

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

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

68 69 70
\subsection{Sum}
\label{sec:summ}

71
The \emph{sum camera} $\monoid_1 \csumm \monoid_2$ for any cameras $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
72
\begin{align*}
73
  \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
74 75
  \mval(\mundef) \eqdef{}& \emptyset \\
  \mval(\cinl(\melt)) \eqdef{}& \mval_1(\melt)  \\
76 77 78 79 80
  \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*}
81 82
Above, $\mval_1$ refers to the validity of $\monoid_1$.
The validity, composition and core for $\cinr$ are defined symmetrically.
83
The remaining cases of the composition and core are all $\mundef$.
84

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

87 88 89 90 91 92
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)}

93
  \axiom{\mundef \nequiv{n} \mundef}
94 95 96
\end{mathpar}


97 98 99 100 101 102 103
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}
104
  {\All \melt_\f \in M, n. n  \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)}
105 106
  {\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
107
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the camera is on if $\mval$ has \emph{no possible frame}.
108

109 110
\subsection{Option}

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

Ralf Jung's avatar
Ralf Jung committed
119
\subsection{Finite Partial Functions}
Ralf Jung's avatar
Ralf Jung committed
120 121
\label{sec:fpfnm}

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

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

  \inferH{fpfn-alloc}
131
  {\mvalFull(\melt)}
132
  {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
Ralf Jung's avatar
Ralf Jung committed
133 134

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

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

142 143
\subsection{Agreement}

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

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

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

Ralf Jung's avatar
Ralf Jung committed
165
  \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
166
  
167
  \axiomH{ag-agree}{n \in \mval(\aginj(x) \mtimes \aginj(y)) \Ra x \nequiv{n} y}
Ralf Jung's avatar
Ralf Jung committed
168 169
\end{mathpar}

170

171
\subsection{Exclusive Camera}
Ralf Jung's avatar
Ralf Jung committed
172

173
Given an OFE $\cofe$, we define a camera $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
Ralf Jung's avatar
Ralf Jung committed
174
\begin{align*}
175
  \exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
176
  \mval(\melt) \eqdef{}& \setComp{n}{\melt \neq \mundef}
Ralf Jung's avatar
Ralf Jung committed
177
\end{align*}
178
All cases of composition go to $\mundef$.
Ralf Jung's avatar
Ralf Jung committed
179
\begin{align*}
180
  \mcore{\exinj(x)} \eqdef{}& \mnocore &
181
  \mcore{\mundef} \eqdef{}& \mundef
Ralf Jung's avatar
Ralf Jung committed
182
\end{align*}
183 184
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
185 186 187
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
  \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
188

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

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
202 203 204 205 206 207 208 209 210 211 212 213 214 215
% \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
216
% 	Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$.
217 218 219 220 221
% 	Pick that for the result.
% \end{proof}

% The powerset monoids is cancellative.
% \begin{proof}[Proof of cancellativity]
Ralf Jung's avatar
Ralf Jung committed
222 223 224 225
% 	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$.
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 256 257
% 	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$.
258
	
Ralf Jung's avatar
Ralf Jung committed
259 260
% 	In the interesting case, we have $f = (q_\f, a_\f)$.
% 	Obtain $b$ such that $b \in B \land b \sep a_\f$.
261 262 263 264 265
% 	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
266 267
% If $\melt_\f = \munit$, we are trivially done.
% So let $\melt_\f = (q_\f, \melt_\f')$.
268 269 270 271
% 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
272
% We have $(q_\f + q_a, \melt_\f' \mtimes \melt') = (q_\f + q_b, \melt_\f' \mtimes \meltB')$.
273 274 275 276 277
% 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
278
\subsection{Authoritative}
279
\label{sec:auth-camera}
280

281
Given a camera $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
282 283 284 285
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 \\
286
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ n \in \mval(\meltB) \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
Ralf Jung's avatar
Ralf Jung committed
287 288 289 290 291
  (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$.
292

Ralf Jung's avatar
Ralf Jung committed
293 294
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)$.
295

Ralf Jung's avatar
Ralf Jung committed
296 297 298 299
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
300
  \[ \All n, \maybe{\melt_\f}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \in \mval(\melt_2) \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
Ralf Jung's avatar
Ralf Jung committed
301 302
\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$.
303

Ralf Jung's avatar
Ralf Jung committed
304 305 306 307 308 309
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}
310

Ralf Jung's avatar
Ralf Jung committed
311
\subsection{STS with Tokens}
312
\label{sec:sts-camera}
313

Ralf Jung's avatar
Ralf Jung committed
314
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.
315

316 317 318 319
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
320
 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)
321
\end{align*}
322

323 324
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
325
\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) \\
326 327
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*}
328

329 330
The STS RA is defined as follows
\begin{align*}
331
  \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 \\
332
  \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
Ralf Jung's avatar
Ralf Jung committed
333 334
  \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$} \\
335 336 337
  \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
  \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*}
338
The remaining cases are all $\mundef$.
339

340 341 342 343
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')}
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 375 376
  \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})}
377

378 379 380 381 382 383 384
  {\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}
385 386 387 388 389

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