From a072e35570910a41b9aa1e50b4ce68dcd7cd9040 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 12 Mar 2016 09:08:56 +0100
Subject: [PATCH] docs: define RAs
---
docs/algebra.tex | 26 +++++++++++++++++++++++++-
1 file changed, 25 insertions(+), 1 deletion(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index a11f91ab1..41916aead 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -52,7 +52,31 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
\subsection{RA}
-\ralf{Copy this from the paper, when that one is more polished.}
+\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.}
\subsection{CMRA}
--
GitLab