From a1579b6efda2d6f98d55f93374ab0869cfa0b653 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Oct 2016 11:25:05 +0200
Subject: [PATCH] Be explicit about the CMRA on option
---
docs/constructions.tex | 25 +++++++++++++++++++++++++
1 file changed, 25 insertions(+)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index ddfc4a7f9..7d8e50d4d 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -1,5 +1,10 @@
\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)}
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.
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$.
+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:
\begin{mathpar}
\inferH{sum-update}
@@ -87,6 +102,16 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
\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}.
+\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}
\label{sec:fpfnm}
--
GitLab