constructions.tex 16.7 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).
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

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}
172

173
Given an OFE $\cofe$, we define a camera $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
174
\begin{align*}
175
  \exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
Ralf Jung's avatar
Ralf Jung committed
176
  \mval(\melt) \eqdef{}& \setComp{n}{\melt \notnequiv{n} \mundef}
177
\end{align*}
178
All cases of composition go to $\mundef$.
179
\begin{align*}
180
  \mcore{\exinj(x)} \eqdef{}& \mnocore &
181
  \mcore{\mundef} \eqdef{}& \mundef
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.

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}
190
\end{mathpar}
191
$\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
192 193 194 195 196 197 198

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

Ralf Jung's avatar
Ralf Jung committed
199
\subsection{Fractions}
200

Ralf Jung's avatar
Ralf Jung committed
201 202 203 204
We define an RA structure on the rational numbers in $(0, 1]$ as follows:
\begin{align*}
  \fracm \eqdef{}& \fracinj(\mathbb{Q} \cap (0, 1]) \mid \mundef \\
  \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
Ralf Jung's avatar
Ralf Jung committed
205
  \fracinj(q_1) \mtimes \fracinj(q_2) \eqdef{}& \fracinj(q_1 + q_2) \quad \text{if $q_1 + q_2 \leq 1$} \\
Ralf Jung's avatar
Ralf Jung committed
206 207 208 209 210 211 212 213 214 215 216 217
  \mcore{\fracinj(x)} \eqdef{}& \bot \\
  \mcore{\mundef} \eqdef{}& \mundef
\end{align*}
All remaining cases of composition go to $\mundef$.
Frequently, we will write just $x$ instead of $\fracinj(x)$.

The most important property of this RA is that $1$ has no frame.
This is useful in combination with \ruleref{sum-swap}, and also when used with pairs:
\begin{mathpar}
  \inferH{pair-frac-change}{}
  {(1, a) \mupd (1, b)}
\end{mathpar}
218 219

%TODO: These need syncing with Coq
220 221 222 223 224 225 226 227 228 229 230 231 232 233
% \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
234
% 	Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$.
235 236 237 238 239
% 	Pick that for the result.
% \end{proof}

% The powerset monoids is cancellative.
% \begin{proof}[Proof of cancellativity]
Ralf Jung's avatar
Ralf Jung committed
240 241 242 243
% 	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$.
244 245 246 247 248
% 	The other direction works the same way.
% \end{proof}



249
\subsection{Authoritative}
250
\label{sec:auth-camera}
251

252
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
253 254 255 256
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 \\
257
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ (x = \mnocore \land n \in \mval(\meltB)) \lor (\Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt \land n \in \mval(\melt)) } \\
Ralf Jung's avatar
Ralf Jung committed
258 259 260 261 262
  (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$.
263

Ralf Jung's avatar
Ralf Jung committed
264 265
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)$.
266

Ralf Jung's avatar
Ralf Jung committed
267 268 269 270
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
271
  \[ \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
272 273
\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$.
274

Ralf Jung's avatar
Ralf Jung committed
275 276 277 278 279 280
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}
281

Ralf Jung's avatar
Ralf Jung committed
282
\subsection{STS with Tokens}
283
\label{sec:sts-camera}
284

Ralf Jung's avatar
Ralf Jung committed
285
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.
286

287 288 289 290
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
291
 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)
292
\end{align*}
293

294 295
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
296
\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) \\
297 298
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*}
299

300 301
The STS RA is defined as follows
\begin{align*}
302
  \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 \\
303
  \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
Ralf Jung's avatar
Ralf Jung committed
304 305
  \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$} \\
306 307 308
  \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
  \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*}
309
The remaining cases are all $\mundef$.
310

311 312 313 314
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')}
315

316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
  \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})}
348

349 350 351 352 353 354 355
  {\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}
356 357 358 359 360

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