diff --git a/docs/algebra.tex b/docs/algebra.tex index 568a937c306d5aade9cbcba1c58b0028165ddd65..0537b8a8418cf3a5b7166c58ffdf2ab6f291ebf9 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -51,7 +51,7 @@ Note that $\COFEs$ is cartesian closed. \begin{defn} A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid, (\mdiv) : \monoid \times \monoid \nfn \monoid)$ satisfying \begin{align*} - \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-nonexp} \\ + \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\ \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} \\ \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\ @@ -67,7 +67,8 @@ Note that $\COFEs$ is cartesian closed. \end{align*} \end{defn} -\ralf{Copy the rest of the explanation from the paper, when that one is more polished.} +This is a natural generalization of RAs over COFEs. +All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index. \paragraph{The division operator $\mdiv$.} One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt \leq \meltB$, then $\melt \mdiv \meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}). @@ -84,13 +85,13 @@ For every $n$, we obtain a proof that $\melt \mincl{n} \meltB$. From this, we could extract a sequence of witnesses $(\meltC_m)_{m}$, and we need to arrive at a single witness $\meltC$ showing that $\melt \leq \meltB$. Without the division operator, there is no reason to believe that such a witness exists. However, since we can use the division operator, and since we know that this operator is \emph{non-expansive}, we can pick $\meltC \eqdef \meltB \mdiv \melt$, and then we can prove that this is indeed the desired witness. -\ralf{The only reason we actually have division is that we are working constructively \emph{and}, at the same time, remain compatible with a classic interpretation of the existential. This is pretty silly.} +\ralf{The only reason we actually have division is that we are working constructively in an impredicative universe. This is pretty silly.} \paragraph{The extension axiom (\ruleref{cmra-extend}).} Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq. The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square: -\ralf{Needs some magic to fix the baseline of the $\nequiv{n}$, or so} +% RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so \begin{center} \begin{tikzpicture}[every edge/.style={draw=none}] \node (a) at (0, 0) {$\melt$}; diff --git a/docs/derived.tex b/docs/derived.tex index 1c832481e0c97d96a2bbcdddb2c0440bbf4a7810..738a87bef2ca24dc77447175b5bdde8753ccc517 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -204,7 +204,7 @@ We can derive some specialized forms of the lifting axioms for the operational s \ralf{Add these.} -\subsection{Global Functor and ghost ownership} +\subsection{Global functor and ghost ownership} \ralf{Describe this.} % \subsection{Global monoid} @@ -364,7 +364,7 @@ We can derive some specialized forms of the lifting axioms for the operational s % \subsection{Ghost heap} % \label{sec:ghostheap}% - +% FIXME use the finmap provided by the global ghost ownership, instead of adding our own % We define a simple ghost heap with fractional permissions. % Some modules require a few ghost names per module instance to properly manage ghost state, but would like to expose to clients a single logical name (avoiding clutter). % In such cases we use these ghost heaps.