From a7be766ab690dc5b5b3cbaf974a5687736530ccc Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 8 Mar 2016 16:28:53 +0100 Subject: [PATCH] add: discrete CMRAs --- docs/algebra.tex | 27 ++++++++++++++++++--------- docs/iris.sty | 1 + 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/docs/algebra.tex b/docs/algebra.tex index 63cb6f818..a83e99cdb 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -48,7 +48,7 @@ Note that $\COFEs$ is cartesian closed. \subsection{CMRA} \begin{defn} - A \emph{CMRA} is a tuple $(\monoid, (\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 + 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 \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} \\ @@ -65,8 +65,6 @@ Note that $\COFEs$ is cartesian closed. \end{align*} \end{defn} -Note that every RA is a CMRA, by picking the discrete COFE for the equivalence relation. - \ralf{Copy the rest of the explanation from the paper, when that one is more polished.} \paragraph{The division operator $\mdiv$.} @@ -115,10 +113,10 @@ This operation is needed to prove that $\later$ commutes with existential quanti \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] - \item $\munit$ is valid: \\ $\All n, \munit \in \mval_n$ - \item $\munit$ is left-identity of the operation: \\ + \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$ + \item $\munit$ is a left-identity of the operation: \\ $\All \melt \in M. \munit \mtimes \melt = \melt$ - \item $\munit$ is discrete + \item $\munit$ is a discrete element \end{enumerate} \end{defn} @@ -130,16 +128,27 @@ This operation is needed to prove that $\later$ commutes with existential quanti \end{defn} Note that for RAs, this and the RA-based definition of a frame-preserving update coincide. -\ralf{Describe discrete CMRAs, and how they correspond to RAs.} +\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:\\ + $\All \melt, \meltB. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$ + \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$. \begin{defn} A function $f : M \to N$ between two CMRAs is \emph{monotone} if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt] \item $f$ is non-expansive \item $f$ preserves validity: \\ - $\All n, x \in M. x \in \mval_n \Ra f(x) \in \mval_n$ + $\All n, \melt \in M. \melt \in \mval_n \Ra f(\melt) \in \mval_n$ \item $f$ preserves CMRA inclusion:\\ - $\All x, y. x \mincl y \Ra f(x) \mincl f(y)$ + $\All \melt, \meltB. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$ \end{enumerate} \end{defn} diff --git a/docs/iris.sty b/docs/iris.sty index ea1ef7760..25f12226b 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -70,6 +70,7 @@ \newcommand{\pset}[1]{\wp(#1)} % Powerset \newcommand{\psetdown}[1]{\wp^\downarrow(#1)} +\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)} \newcommand{\Func}{F} % functor -- GitLab