diff --git a/algebra/cofe.v b/algebra/cofe.v index ddf170fe7b5cace107f407599078039a67e0ef7c..b1bf310324209bec3d7716dfbc14e9642a5dff28 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -89,6 +89,8 @@ Section cofe_mixin. End cofe_mixin. (** Discrete COFEs and Timeless elements *) +(* TODO RJ: On paper, I called these "discrete elements". I think that makes + more sense. *) Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_} _ {_} _ _. Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x. diff --git a/docs/algebra.tex b/docs/algebra.tex index e96cd7e49a3b7e915f0705db1f45de3b378234f5..522d15e97846edf92de153da932554d854d1f928 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -18,7 +18,28 @@ \ralf{Copy the explanation from the paper, when that one is more polished.} -\ralf{Describe non-expansive, contractive, category $\COFEs$, later, locally non-expansive/contractive, black later, discrete elements, discrete CMRAs.} +\begin{defn} + An element $x \in A$ of a COFE is called \emph{discrete} if + $\All y \in A. x \nequiv{0} y \Ra x = y$ + A COFE $A$ is called \emph{discrete} if all its elements are discrete. +\end{defn} + +\begin{defn} + A function $f : A \to B$ between two COFEs is \emph{non-expansive} if + $\All n, x \in A, y \in A. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y)$ + It is \emph{contractive} if + $\All n, x \in A, y \in A. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x)$ +\end{defn} + +\begin{defn} + The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. +\end{defn} +Note that $\COFEs$ is cartesian closed. + +\begin{defn} + A functor $F : \COFEs \to COFEs$ is called \emph{locally non-expansive} if its actions $F_1$ on arrows is itself a non-expansive map. + Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. +\end{defn} \subsection{RA} @@ -91,17 +112,33 @@ This operation is needed to prove that $\later$ commutes with existential quanti \end{mathpar} (This assumes that the type $\type$ is non-empty.) -\ralf{Describe monotone, category $\CMRAs$.} - \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 n, \melt_f. \melt \mtimes \melt_f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval_n$ We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \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 function $f : M \to N$ between two CMRAs is \emph{monotone} if it satisfies the following conditions: + \begin{enumerate} + \item $f$ is non-expansive + \item $f$ preserves validity: \\ + $\All n, x \in M. x \in \mval_n \Ra f(x) \in \mval_n$ + \item $f$ preserves CMRA inclusion:\\ + $\All x, y. x \mincl y \Ra f(x) \mincl f(y)$ + \end{enumerate} +\end{defn} + +\begin{defn} + The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows. +\end{defn} +Note that $\CMRAs$ is a subcategory of $\COFEs$. +The notion of a locally non-expansive (or contractive) functor naturally generalizes to functors between these categories. + %%% Local Variables: %%% mode: latex diff --git a/docs/logic.tex b/docs/logic.tex index e12cdd02ca2e034d74cc66caa03e3af8bc92c15b..c1caf48a06b781457cb3865435553cd819d5f923 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -25,12 +25,15 @@ It does not matter whether they fork off an arbitrary expression. \end{itemize} \begin{defn}[Context] - A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied - \begin{align*} - \All\expr.& \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot \tagH{lang-ctx-not-val}\\ - \All \expr_1, \state_1, \expr_2, \state_2, \expr'.& \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' \tagH{lang-ctx-step}\\ - \All \expr_1', \state_1, \expr_2, \state_2, \expr'.& \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' \tagH{lang-ctx-step-inv} - \end{align*} + A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied: + \begin{enumerate} + \item $\lctx$ does not turn non-values into values:\\ + $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ + \item One can perform reductions below $\lctx$:\\ + $\All \expr_1, \state_1, \expr_2, \state_2, \expr'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr'$ + \item Reductions stay below $\lctx$ until there is a value in the hole:\\ + $\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr'$ + \end{enumerate} \end{defn} \subsection{The concurrent language} @@ -62,6 +65,7 @@ To instantiate Iris, you need to define the following parameters: \begin{itemize} \item A language $\Lang$ \item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state + \ralf{$\iFunc$ also needs to have a single-unit.} \end{itemize} \noindent diff --git a/docs/model.tex b/docs/model.tex index c3d8fd1685931cfc48d82576ab3df1521f2ed9e6..c2391766731ed2b0994a027670c68b55ee01ad4b 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -1,5 +1,7 @@ \section{Model and semantics} +\ralf{What also needs to be done here: Define uPred and its later function; define black later; define the resource CMRA} + The semantics closely follows the ideas laid out in~\cite{catlogic}. We just repeat some of the most important definitions here.