Commit aae046b8 authored by Ralf Jung's avatar Ralf Jung

docs: address Lars' remaining comments

parent a2b62737
......@@ -211,7 +211,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\end{defn}
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
\ralf{Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.}
%%% Local Variables:
%%% mode: latex
......
......@@ -3,7 +3,7 @@
\subsection{Next (type-level later)}
Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
......@@ -62,7 +62,7 @@ Frame-preserving updates on the $M_i$ lift to the product:
\subsection{Sum}
\label{sec:summ}
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as:
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
\begin{align*}
\monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \bot \\
\mval_n \eqdef{}& \setComp{\cinl(\melt_1)\!}{\!\melt_1 \in \mval'_n}
......@@ -104,36 +104,35 @@ We obtain the following frame-preserving updates:
{\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd \meltsB}
{\melt \mupd_\monoid \meltsB}
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
Remember that $\mval$ is the set of elements of a CMRA that are valid at \emph{all} step-indices.
Above, $\mval$ refers to the validity of $\monoid$.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\newcommand{\aginjc}{\mathrm{c}} % the "c" field of an agreement element
\newcommand{\aginjV}{\mathrm{V}} % the "V" field of an agreement element
\begin{align*}
\agm(\cofe) \eqdef{}& \record{\aginjc : \mathbb{N} \to \cofe , \aginjV : \SProp} \\
& \text{quotiented by} \\
\melt \equiv \meltB \eqdef{}& \melt.\aginjV = \meltB.\aginjV \land \All n. n \in \melt.\aginjV \Ra \melt.\aginjc(n) \nequiv{n} \meltB.\aginjc(n) \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\aginjV \Lra m \in \meltB.\aginjV) \land (\All m \leq n. m \in \melt.\aginjV \Ra \melt.\aginjc(m) \nequiv{m} \meltB.\aginjc(m)) \\
\mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
\agm(\cofe) \eqdef{}& \set{(c, V) \in (\mathbb{N} \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
\textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land
\All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n) \\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
\mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB })
\melt \mtimes \meltB \eqdef{}& \left(\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V \land \melt \nequiv{n} \meltB }\right)
\end{align*}
Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $\aginjc$ and $\aginjV$.
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ steps.
You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
However, given such a chain, we cannot constructively define its limit: Clearly, the $\aginjV$ of the limit is the limit of the $\aginjV$ of the chain.
However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
But what to pick for the actual data, for the element of $\cofe$?
Only if $\aginjV = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\aginjV$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin \aginjV$.
Only if $V = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
......
......@@ -134,7 +134,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion about propositions, defined as follows:
......@@ -382,15 +382,17 @@ This is entirely standard.
{\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
\vctx,\var : \type\mid\pfctx , \prop \proves \propB}
{\vctx\mid\pfctx \proves \propB}
\and
\infer[$\lambda$]
{}
{\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
\and
\infer[$\mu$]
{}
{\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
% \and
% \infer[$\lambda$]
% {}
% {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
% \and
% \infer[$\mu$]
% {}
% {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
\paragraph{Laws of (affine) bunched implications.}
\begin{mathpar}
......@@ -449,6 +451,7 @@ This is entirely standard.
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
\end{array}
\end{mathpar}
A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
\begin{mathpar}
\infer
......
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