@@ -189,7 +189,8 @@ The first is trivial, the second follows from cancellativitiy of $M$.
\label{sec:fpfunm}
Given a countable set $X$ and a monoid $M$, we construct a monoid representing finite partial functions from $X$ to (non-unit, non-zero elements of) $M$.
Let $\fpfunm{X}{M}$ be the product monoid $\prod_{x \in X} M$, as defined in \secref{sec:prodm} but restricting the carrier to functions $f$ where the set $\dom(f)\eqdef\{ x \mid f(x)\neq\munit_M \}$ is finite.
\ralf{all outdated}
Let ${X}\fpfn{M}$ be the product monoid $\prod_{x \in X} M$, as defined in \secref{sec:prodm} but restricting the carrier to functions $f$ where the set $\dom(f)\eqdef\{ x \mid f(x)\neq\munit_M \}$ is finite.
This is well-defined as the set of these $f$ contains the unit and is closed under multiplication.
(We identify finite partial functions from $X$ to $\mcarp{M}\setminus\{\munit_M\}$ and total functions from $X$ to $\mcarp{M}$ with finite $\munit_M$-support.)
...
...
@@ -303,7 +304,7 @@ Frame-preserving updates are also possible if we assume $M$ cancellative:
By combining the fractional, finite partial function, and authoritative monoids, we construct two flavors of heaps with fractional permissions and mention their important frame-preserving updates.
Hereinafter, we assume the set $\textdom{Val}$ of values is countable.
Given a set $Y$, define $\FHeap(Y)\eqdef\fpfunm{\textdom{Val}}{\fracm{Y}}$ representing a fractional heap with codomain $Y$.
Given a set $Y$, define $\FHeap(Y)\eqdef\textdom{Val}\fpfn\fracm(Y)$ representing a fractional heap with codomain $Y$.
From \S\S\ref{sec:fracm} and~\ref{sec:fpfunm} we obtain the following frame-preserving updates as well as the fact that $\FHeap(Y)$ is cancellative.
@@ -5,7 +5,7 @@ In this section we describe some constructions that we will use throughout the r
\subsection{Global monoid}
Hereinafter we assume the global monoid (served up as a parameter to Iris) is obtained from a family of monoids $(M_i)_{i \in I}$ by first applying the construction for finite partial functions to each~(\Sref{sec:fpfunm}), and then applying the product construction~(\Sref{sec:prodm}):
\[ M \eqdef\prod_{i \in I}\fpfunm{\textdom{GhName}}{M_i}\]
\[ M \eqdef\prod_{i \in I}\textdom{GhName}\fpfnM_i \]
We don't care so much about what concretely $\textdom{GhName}$ is, as long as it is countable and infinite.
We write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto[\gname\mapsto\melt]]}$ when $\melt\in\mcarp{M_i}$, and for $\FALSE$ when $\melt=\mzero_{M_i}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the name $\gname$ is allocated and has at least value $\melt$.
