Commit 9e98ff8b authored by Ralf Jung's avatar Ralf Jung

docs: describe the unit of a CMRA and how the logic demands one

parent fa0ed70a
Pipeline #286 passed with stage
......@@ -112,6 +112,16 @@ This operation is needed to prove that $\later$ commutes with existential quanti
\end{mathpar}
(This assumes that the type $\type$ is non-empty.)
\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: \\
$\All \melt \in M. \munit \mtimes \melt = \melt$
\item $\munit$ is discrete
\end{enumerate}
\end{defn}
\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 \]
......@@ -124,7 +134,7 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update
\begin{defn}
A function $f : M \to N$ between two CMRAs is \emph{monotone} if it satisfies the following conditions:
\begin{enumerate}
\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$
......
......@@ -129,6 +129,7 @@
\newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
\newcommand{\munit}{\varepsilon}
\newcommand{\mcore}[1]{\lfloor#1\rfloor}
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mdiv}{\mathbin{\div}}
......
......@@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression.
\begin{defn}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}
\begin{enumerate}[itemsep=0pt]
\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$:\\
......@@ -64,8 +64,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
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.}
\item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
\end{itemize}
\noindent
......@@ -107,6 +106,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
\munit \mid
\mcore\term \mid
\term \mtimes \term \mid
\\&
......@@ -213,6 +213,8 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
\infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
\and
\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
......@@ -416,7 +418,7 @@ This is entirely standard.
\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra& \ownGGhost{\melt \mtimes \meltB} \\
%\TRUE &\Ra& \ownGGhost{\munit}\\
\TRUE &\Ra& \ownGGhost{\munit}\\
\ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}
\end{array}
\and
......
......@@ -22,7 +22,7 @@
\usepackage{xcolor} % for print version
\usepackage{graphicx}
\usepackage{enumitem}
\usepackage{semantic}
\usepackage{csquotes}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment