Commit a1579b6e by Ralf Jung

### Be explicit about the CMRA on option

parent dccb4153
 \section{COFE constructions} \section{COFE constructions} \subsection{Trivial pointwise lifting} The COFE structure on many types can be easily obtained by pointwise lifting of the structure of the components. 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). \subsection{Next (type-level later)} \subsection{Next (type-level later)} Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type): Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type): ... @@ -75,6 +80,16 @@ The composition and core for $\cinr$ are defined symmetrically. ... @@ -75,6 +80,16 @@ The composition and core for $\cinr$ are defined symmetrically. The remaining cases of the composition and core are all $\bot$. The remaining cases of the composition and core are all $\bot$. Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$. Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$. 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)} \axiom{\bot \nequiv{n} \bot} \end{mathpar} We obtain the following frame-preserving updates, as well as their symmetric counterparts: We obtain the following frame-preserving updates, as well as their symmetric counterparts: \begin{mathpar} \begin{mathpar} \inferH{sum-update} \inferH{sum-update} ... @@ -87,6 +102,16 @@ We obtain the following frame-preserving updates, as well as their symmetric cou ... @@ -87,6 +102,16 @@ We obtain the following frame-preserving updates, as well as their symmetric cou \end{mathpar} \end{mathpar} Crucially, the second rule allows us to \emph{swap} the side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}. Crucially, the second rule allows us to \emph{swap} the side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}. \subsection{Option} The definition of the (CM)RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$. We can easily extend this to a full CMRA by defining a suitable core, namely \begin{align*} \mcore{\mnocore} \eqdef{}& \mnocore & \\ \mcore{\maybe\melt} \eqdef{}& \mcore\melt & \text{If $\maybe\melt \neq \mnocore$} \end{align*} Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\maybe\monoid}$). \subsection{Finite partial function} \subsection{Finite partial function} \label{sec:fpfnm} \label{sec:fpfnm} ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!