From 9e98ff8be4b4ca516a497d328aaf31cbae186a6c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 14:55:31 +0100
Subject: [PATCH] docs: describe the unit of a CMRA and how the logic demands
one
---
docs/algebra.tex | 12 +++++++++++-
docs/iris.sty | 1 +
docs/logic.tex | 10 ++++++----
docs/setup.tex | 2 +-
4 files changed, 19 insertions(+), 6 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 9fde12b07..63cb6f818 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -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$
diff --git a/docs/iris.sty b/docs/iris.sty
index b761d4cf4..ea1ef7760 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -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}}
diff --git a/docs/logic.tex b/docs/logic.tex
index fb80799be..6c46bea0c 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -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
diff --git a/docs/setup.tex b/docs/setup.tex
index c43a68e75..849e83626 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -22,7 +22,7 @@
\usepackage{xcolor} % for print version
\usepackage{graphicx}
-
+\usepackage{enumitem}
\usepackage{semantic}
\usepackage{csquotes}
--
GitLab