diff --git a/docs/algebra.tex b/docs/algebra.tex index 8f278074f4f9aacd3d1c5206cedda70c6c675fcc..6d738187e0f1c4c42484357cdc9ef04bb06b03fe 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -23,6 +23,8 @@ This definition varies slightly from the original one in~\cite{catlogic}. An element $x \in \cofe$ of a COFE is called \emph{discrete} if $\All y \in \cofe. x \nequiv{0} y \Ra x = y$ A COFE $A$ is called \emph{discrete} if all its elements are discrete. + For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$ + \end{defn} \begin{defn} @@ -31,6 +33,7 @@ This definition varies slightly from the original one in~\cite{catlogic}. It is \emph{contractive} if $\All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x)$ \end{defn} +The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. diff --git a/docs/constructions.tex b/docs/constructions.tex index e7763440eddea9a1023c11e6d4b9859cbf36d5aa..d5849d53e2917a6937da71c99d5fa29997d67664 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: For every ste \end{align*} Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a monotone'' function here is a little funny. \begin{align*} - \UPred(\monoid) \approx{}& \monoid \monra \SProp \\ + \UPred(\monoid) \cong{}& \monoid \monra \SProp \\ \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)} \end{align*} The reason we chose the first definition is that it is easier to work with in Coq. @@ -77,35 +77,35 @@ $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{\agc}{\mathrm{c}} % the "c" field of an agreement element -\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element +\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{\agc : \mathbb{N} \to \cofe , \agV : \SProp} \\ + \agm(\cofe) \eqdef{}& \record{\aginjc : \mathbb{N} \to \cofe , \aginjV : \SProp} \\ & \text{quotiented by} \\ - \melt \equiv \meltB \eqdef{}& \melt.\agV = \meltB.\agV \land \All n. n \in \melt.\agV \Ra \melt.\agc(n) \nequiv{n} \meltB.\agc(n) \\ - \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\agV \Lra m \in \meltB.\agV) \land (\All m \leq n. m \in \melt.\agV \Ra \melt.\agc(m) \nequiv{m} \meltB.\agc(m)) \\ - \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\agV \land \All m \leq n. \melt.\agc(n) \nequiv{m} \melt.\agc(m) } \\ + \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 \monoid}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\ \mcore\melt \eqdef{}& \melt \\ - \melt \mtimes \meltB \eqdef{}& (\melt.\agc, \setComp{n}{n \in \melt.\agV \land n \in \meltB.\agV \land \melt \nequiv{n} \meltB }) + \melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB }) \end{align*} $\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$. -You can think of the $\agc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \agV$ steps. +You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ 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 $\agV$ of the limit is the limit of the $\agV$ of the chain. +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. But what to pick for the actual data, for the element of $\cofe$? -Only if $\agV = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\agV$ is smaller, the chain cancels'', \ie stops converging as we reach indices $n \notin \agV$. +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$. 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 $\ag$ into $\agm(\cofe)$ as follows: -$\ag(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}}$ +We define an injection $\aginj$ into $\agm(\cofe)$ as follows: +$\aginj(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}}$ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following: \begin{mathpar} - \axiomH{ag-val}{\ag(x) \in \mval_n} + \axiomH{ag-val}{\aginj(x) \in \mval_n} - \axiomH{ag-dup}{\ag(x) = \ag(x)\mtimes\ag(x)} + \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)} - \axiomH{ag-agree}{\ag(x) \mtimes \ag(y) \in \mval_n \Ra x \nequiv{n} y} + \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y} \end{mathpar} \subsection{One-shot} @@ -115,17 +115,17 @@ Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows: \begin{align*} \oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\ \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n} -\end{align*} -\begin{align*} - \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\ - \mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot -\end{align*} -\begin{align*} +\\%\end{align*} +%\begin{align*} \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\ \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\ \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) -\end{align*} +\end{align*}% The remaining cases of composition go to $\bot$. +\begin{align*} + \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\ + \mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot +\end{align*} The step-indexed equivalence is inductively defined as follows: \begin{mathpar} \axiom{\ospending \nequiv{n} \ospending} @@ -149,34 +149,38 @@ We obtain the following frame-preserving updates: {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}} \end{mathpar} -%TODO: These need syncing with Coq -% \subsection{Exclusive monoid} +\subsection{Exclusive CMRA} -% Given a set $X$, we define a monoid such that at most one $x \in X$ can be owned. -% Let $\exm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication -% $-% \melt \cdot \meltB \;\eqdef\; -% \begin{cases} -% \melt & \mbox{if } \meltB = \munit \\ -% \meltB & \mbox{if } \melt = \munit -% \end{cases} -%$ +Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned: +\begin{align*} + \exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\ + \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\ + \munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x) +\end{align*} +The remaining cases of composition go to $\bot$. +\begin{align*} + \mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit & + \mcore{\bot} \eqdef{}& \bot +\end{align*} +The step-indexed equivalence is inductively defined as follows: +\begin{mathpar} + \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)} -% The frame-preserving update -% \begin{mathpar} -% \inferH{ExUpd} -% {x \in X} -% {x \mupd \melt} -% \end{mathpar} -% is easily shown, as the only possible frame for $x$ is $\munit$. + \axiom{\munit \nequiv{n} \munit} -% Exclusive monoids are cancellative. -% \begin{proof}[Proof of cancellativity] -% If $\melt_f = \munit$, then the statement is trivial. -% If $\melt_f \neq \munit$, then we must have $\melt = \meltB = \munit$, as otherwise one of the two products would be $\mzero$. -% \end{proof} + \axiom{\bot \nequiv{n} \bot} +\end{mathpar} +$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$. + +We obtain the following frame-preserving update: +\begin{mathpar} + \inferH{ex-update}{} + {\exinj(x) \mupd \exinj(y)} +\end{mathpar} + +%TODO: These need syncing with Coq % \subsection{Finite Powerset Monoid} % Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows: diff --git a/docs/iris.sty b/docs/iris.sty index 644b63455f5460666c5af8c1820dedc5af3b45e4..3370db61803d4cf51099d725cfb1d498ab767657 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -86,13 +86,15 @@ \newcommand{\rs}{r} \newcommand{\rsB}{s} +\newcommand{\rss}{R} \newcommand{\pres}{\pi} \newcommand{\wld}{w} \newcommand{\ghostRes}{g} %% Various pieces of syntax -\newcommand{\wsat}[4]{#1 \models_{#2} #3; #4} +\newcommand{\wsat}[3]{#1 \models_{#2} #3} +\newcommand{\wsatpre}{\textdom{pre-wsat}} \newcommand{\wtt}[2]{#1 : #2} % well-typed term @@ -114,6 +116,7 @@ \newcommand{\UPred}{\textdom{UPred}} \newcommand{\mProp}{\textdom{Prop}} % meta-level prop \newcommand{\iProp}{\textdom{iProp}} +\newcommand{\iPreProp}{\textdom{iPreProp}} \newcommand{\Wld}{\textdom{Wld}} \newcommand{\Res}{\textdom{Res}} @@ -121,6 +124,7 @@ \newcommand{\cofeB}{U} \newcommand{\COFEs}{\mathcal{U}} % category of COFEs \newcommand{\iFunc}{\Sigma} +\newcommand{\fix}{\textdom{fix}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS @@ -136,6 +140,8 @@ \newcommand{\melts}{A} \newcommand{\meltsB}{B} +\newcommand{\f}{\mathrm{f}} % for "frame" + \newcommand{\mcar}[1]{|#1|} \newcommand{\mcarp}[1]{\mcar{#1}^{+}} \newcommand{\munit}{\varepsilon} @@ -321,13 +327,14 @@ % Agreement \newcommand{\agm}{\ensuremath{\textmon{Ag}}} -\newcommand{\ag}{\textlog{ag}} +\newcommand{\aginj}{\textlog{ag}} % Fraction \newcommand{\fracm}{\ensuremath{\textmon{Frac}}} % Exclusive \newcommand{\exm}{\ensuremath{\textmon{Ex}}} +\newcommand{\exinj}{\textlog{ex}} % Auth \newcommand{\authm}{\textmon{Auth}} diff --git a/docs/logic.tex b/docs/logic.tex index 1010939ad83c5f36baac6cfa0cd1fb905353c0ef..2c8a49da5615064e4faf17191d85438fc4dd2536 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -124,7 +124,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t \prop * \prop \mid \prop \wand \prop \mid \\& - \MU \var:\type. \pred \mid + \MU \var:\type. \term \mid \Exists \var:\type. \prop \mid \All \var:\type. \prop \mid \\& @@ -136,7 +136,7 @@ Iris syntax is built up from a signature$\Sig$and a countably infinite set$\t \pvs[\term][\term] \prop\mid \wpre{\term}[\term]{\Ret\var.\term} \end{align*} -Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality. +Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. 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$. diff --git a/docs/model.tex b/docs/model.tex index 341deb1a8cba17c36064ff5bf3eee666666e665c..d1af61a1eb409fc183f1b142d0d02aba703d00c1 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -3,10 +3,11 @@ The semantics closely follows the ideas laid out in~\cite{catlogic}. \subsection{Generic model of base logic} +\label{sec:upred-logic} The base logic including equality, later, always, and a notion of ownership is defined on $\UPred(\monoid)$ for any CMRA $\monoid$. -\typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \to \UPred(\monoid)} +\typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)} Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$. We are thus going to define the assertions as mapping CMRA elements to sets of step-indices. @@ -42,410 +43,165 @@ We introduce an additional logical connective $\ownM\melt$, which will later be \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\melt \in \mval_n} \\ \end{align*} +For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone. -%\subsection{Iris model} -% \subsection{Semantic structures: propositions} -% \ralf{This needs to be synced with the Coq development again.} +\subsection{Iris model} -% $-% \begin{array}[t]{rcl} -% % \protStatus &::=& \enabled \ALT \disabled \\[0.4em] -% \textdom{Res} &\eqdef& -% \{\, \rs = (\pres, \ghostRes) \mid -% \pres \in \textdom{State} \uplus \{\munit\} \land \ghostRes \in \mcarp{\monoid} \,\} \\[0.5em] -% (\pres, \ghostRes) \rtimes -% (\pres', \ghostRes') &\eqdef& -% \begin{cases} -% (\pres, \ghostRes \mtimes \ghostRes') & \mbox{if \pres' = \munit and \ghostRes \mtimes \ghostRes' \neq \mzero} \\ -% (\pres', \ghostRes \mtimes \ghostRes') & \mbox{if \pres = \munit and \ghostRes \mtimes \ghostRes' \neq \mzero} -% \end{cases} -% \\[0.5em] -% % -% \rs \leq \rs' & \eqdef & -% \Exists \rs''. \rs' = \rs \rtimes \rs''\\[1em] -% % -% \UPred(\textdom{Res}) &\eqdef& -% \{\, p \subseteq \mathbb{N} \times \textdom{Res} \mid -% \All (k,\rs) \in p. -% \All j\leq k. -% \All \rs' \geq \rs. -% (j,\rs')\in p \,\}\\[0.5em] -% \restr{p}{k} &\eqdef& -% \{\, (j, \rs) \in p \mid j < k \,\}\\[0.5em] -% p \nequiv{n} q & \eqdef & \restr{p}{n} = \restr{q}{n}\\[1em] -% % -% \textdom{PreProp} & \cong & -% \latert\big( \textdom{World} \monra \UPred(\textdom{Res}) -% \big)\\[0.5em] -% % -% \textdom{World} & \eqdef & -% \mathbb{N} \fpfn \textdom{PreProp}\\[0.5em] -% % -% w \nequiv{n} w' & \eqdef & -% n = 0 \lor -% \bigl(\dom(w) = \dom(w') \land \All i\in\dom(w). w(i) \nequiv{n} w'(i)\bigr) -% \\[0.5em] -% % -% w \leq w' & \eqdef & -% \dom(w) \subseteq \dom(w') \land \All i \in \dom(w). w(i) = w'(i) -% \\[0.5em] -% % -% \textdom{Prop} & \eqdef & \textdom{World} \monra \UPred(\textdom{Res}) -% \end{array} -%$ - -% For $p,q\in\UPred(\textdom{Res})$ with $p \nequiv{n} q$ defined -% as above, $\UPred(\textdom{Res})$ is a -% c.o.f.e. - -% $\textdom{Prop}$ is a c.o.f.e., which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}. -% We do not need to consider how the object is constructed. -% We only need the isomorphism, given by maps -% \begin{align*} -% \wIso &: \latert \bigl(World \monra \UPred(\textdom{Res})\bigr) \to \textdom{PreProp} \\ -% \wIso^{-1} &: \textdom{PreProp} \to \latert \bigl(World \monra \UPred(\textdom{Res})\bigr) -% \end{align*} -% which are inverses to each other. -% Note: this is an isomorphism in $\cal U$, i.e., $\wIso$ and -% $\wIso^{-1}$ are both non-expansive. - -% $\textdom{World}$ is a c.o.f.e.\ with the family of equivalence -% relations defined as shown above. - -% \subsection{Semantic structures: types and environments} - -% For a set $X$, write $\Delta X$ for the discrete c.o.f.e.\ with $x \nequiv{n} -% x'$ iff $n = 0$ or $x = x'$ -% $-% \begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -% \Sem{\textsort{Unit}} &\eqdef& \Delta \{ \star \} \\ -% \Sem{\textsort{InvName}} &\eqdef& \Delta \mathbb{N} \\ -% \Sem{\textsort{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ -% \Sem{\textsort{Monoid}} &\eqdef& \Delta |\monoid| -% \end{array} -% \qquad\qquad -% \begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -% \Sem{\textsort{Val}} &\eqdef& \Delta \textdom{Val} \\ -% \Sem{\textsort{Exp}} &\eqdef& \Delta \textdom{Exp} \\ -% \Sem{\textsort{Ectx}} &\eqdef& \Delta \textdom{Ectx} \\ -% \Sem{\textsort{State}} &\eqdef& \Delta \textdom{State} \\ -% \end{array} -% \qquad\qquad -% \begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -% \Sem{\sort \times \sort'} &\eqdef& \Sem{\sort} \times \Sem{\sort} \\ -% \Sem{\sort \to \sort'} &\eqdef& \Sem{\sort} \to \Sem{\sort} \\ -% \Sem{\Prop} &\eqdef& \textdom{Prop} \\ -% \end{array} -%$ - -% The balance of our signature $\Sig$ is interpreted as follows. -% For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define -% $-% \Sem{\type} \eqdef X_\type -%$ -% For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick an arrow $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \to \Sem{\type_{n+1}}$ in $\cal U$. - -% An environment $\vctx$ is interpreted as the set of -% maps $\rho$, with $\dom(\rho) = \dom(\vctx)$ and -% $\rho(x)\in\Sem{\vctx(x)}$, -% and -% $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land -% \All x\in\dom(\rho). \rho(x) \nequiv{n} \rho'(x)\bigr)$. - -% \ralf{Re-check all the following definitions with the Coq development.} -% %\typedsection{Validity}{valid : \pset{\textdom{Prop}} \in Sets} -% % -% %\begin{align*} -% %valid(p) &\iff \All n \in \mathbb{N}. \All \rs \in \textdom{Res}. \All W \in \textdom{World}. (n, \rs) \in p(W) -% %\end{align*} - -% \typedsection{Later modality}{\later : \textdom{Prop} \to \textdom{Prop} \in {\cal U}} - -% \begin{align*} -% \later p &\eqdef \Lam W. \{\, (n + 1, r) \mid (n, r) \in p(W) \,\} \cup \{\, (0, r) \mid r \in \textdom{Res} \,\} -% \end{align*} -% \begin{lem} -% $\later{}$ is well-defined: $\later {p}$ is a valid proposition (this amounts to showing non-expansiveness), and $\later{}$ itself is a \emph{contractive} map. -% \end{lem} - -% \typedsection{Always modality}{\always{} : \textdom{Prop} \to \textdom{Prop} \in {\cal U}} - -% \begin{align*} -% \always{p} \eqdef \Lam W. \{\, (n, r) \mid (n, \munit) \in p(W) \,\} -% \end{align*} -% \begin{lem} -% $\always{}$ is well-defined: $\always{p}$ is a valid proposition (this amounts to showing non-expansiveness), and $\always{}$ itself is a non-expansive map. -% \end{lem} - -% % PDS: p \Rightarrow q not defined. -% %\begin{lem}\label{lem:always-impl-valid} -% %\begin{align*} -% %&\forall p, q \in \textdom{Prop}.~\\ -% %&\qquad -% % (\forall n \in \mathbb{N}.~\forall \rs \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \rs) \in p(W) \Rightarrow (n, \rs) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)}) -% %\end{align*} -% %\end{lem} - -% \typedsection{Invariant definition}{inv : \Delta(\mathbb{N}) \times \textdom{Prop} \to \textdom{Prop} \in {\cal U}} -% \begin{align*} -% \mathit{inv}(\iota, p) &\eqdef \Lam W. \{\, (n, r) \mid \iota\in\dom(W) \land W(\iota) \nequiv{n+1}_{\textdom{PreProp}} \wIso(p) \,\} -% \end{align*} -% \begin{lem} -% $\mathit{inv}$ is well-defined: $\mathit{inv}(\iota, p)$ is a valid proposition (this amounts to showing non-expansiveness), and $\mathit{inv}$ itself is a non-expansive map. -% \end{lem} - -% \typedsection{World satisfaction}{\wsat{-}{-}{-}{-} : -% \textdom{State} \times -% \pset{\mathbb{N}} \times -% \textdom{Res} \times -% \textdom{World} \to \psetdown{\mathbb{N}} \in {\cal U}} -% \ralf{Make this Dave-compatible: Explicitly compose all the things in $s$} -% \begin{align*} -% \wsat{\state}{\mask}{\rs}{W} &= -% \begin{aligned}[t] -% \{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rtimes \rsB).\pres = \state \land{}\\ -% &\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\ -% &\quad\quad \iota \in \mask \ra (n, \rsB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \} -% \end{aligned} -% \end{align*} -% \begin{lem}\label{lem:fullsat-nonexpansive} -% $\wsat{-}{-}{-}{-}$ is well-defined: It maps into $\psetdown{\mathbb{N}}$. (There is no need for it to be a non-expansive map, it doesn't itself live in $\cal U$.) -% \end{lem} - -% \begin{lem}\label{lem:fullsat-weaken-mask} -% \begin{align*} -% \MoveEqLeft -% \All \state \in \Delta(\textdom{State}). -% \All \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}). -% \All \rs, \rsB \in \Delta(\textdom{Res}). -% \All W \in \textdom{World}. \\& -% \mask_1 \subseteq \mask_2 \implies (\wsat{\state}{\mask_2}{\rs}{W}) \subseteq (\wsat{\state}{\mask_1}{\rs}{W}) -% \end{align*} -% \end{lem} - -% \begin{lem}\label{lem:nequal_ext_world} -% \begin{align*} -% & -% \All n \in \mathbb{N}. -% \All W_1, W_1', W_2 \in \textdom{World}. -% W_1 \nequiv{n} W_2 \land W_1 \leq W_1' \implies \Exists W_2' \in \textdom{World}. W_1' \nequiv{n} W_2' \land W_2 \leq W_2' -% \end{align*} -% \end{lem} - -% \typedsection{Timeless}{\textit{timeless} : \textdom{Prop} \to \textdom{Prop}} - -% \begin{align*} -% \textit{timeless}(p) \eqdef -% \begin{aligned}[t] -% \Lam W. -% \{\, (n, r) &\mid \All W' \geq W. \All k \leq n. \All r' \in \textdom{Res}. \\ -% &\qquad -% k > 0 \land (k - 1, r') \in p(W') \implies (k, r') \in p(W') \,\} -% \end{aligned} -% \end{align*} - -% \begin{lem} -% \textit{timeless} is well-defined: \textit{timeless}(p) is a valid proposition, and \textit{timeless} itself is a non-expansive map. -% \end{lem} - -% % PDS: \Ra undefined. -% %\begin{lem} -% %\begin{align*} -% %& -% % \All p \in \textdom{Prop}. -% % \All \mask \in \pset{\mathbb{N}}. -% %valid(\textit{timeless}(p) \Ra (\later p \vs[\mask][\mask] p)) -% %\end{align*} -% %\end{lem} - -% \typedsection{View-shift}{\mathit{vs} : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \textdom{Prop} \to \textdom{Prop} \in {\cal U}} -% \begin{align*} -% \mathit{vs}_{\mask_1}^{\mask_2}(q) &= \Lam W. -% \begin{aligned}[t] -% \{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\ -% &\qquad -% k \in (\wsat{\state}{\mask_1 \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\ -% &\qquad -% \Exists W' \geq W_F. \Exists \rs'. k \in (\wsat{\state}{\mask_2 \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(W') -% \,\} -% \end{aligned} -% \end{align*} -% \begin{lem} -% $\mathit{vs}$ is well-defined: $\mathit{vs}_{\mask_1}^{\mask_2}(q)$ is a valid proposition, and $\mathit{vs}$ is a non-expansive map. -% \end{lem} - - -% %\begin{lem}\label{lem:prim_view_shift_trans} -% %\begin{align*} -% %\MoveEqLeft -% % \All \mask_1, \mask_2, \mask_3 \in \Delta(\pset{\mathbb{N}}). -% % \All p, q \in \textdom{Prop}. \All W \in \textdom{World}. -% % \All n \in \mathbb{N}.\\ -% %& -% % \mask_2 \subseteq \mask_1 \cup \mask_3 \land -% % \bigl(\All W' \geq W. \All r \in \textdom{Res}. \All k \leq n. (k, r) \in p(W') \implies (k, r) \in vs_{\mask_2}^{\mask_3}(q)(W')\bigr) \\ -% %&\qquad -% % {}\implies \All r \in \textdom{Res}. (n, r) \in vs_{\mask_1}^{\mask_2}(p)(W) \implies (n, r) \in vs_{\mask_1}^{\mask_3}(q)(W) -% %\end{align*} -% %\end{lem} - -% % PDS: E_1 ==>> E_2 undefined. -% %\begin{lem} -% %\begin{align*} -% %& -% % \forall \mask_1, \mask_2, \mask_3 \in \Delta(\pset{\mathbb{N}}).~ -% % \forall p_1, p_2, p_3 \in \textdom{Prop}.~\\ -% %&\qquad -% % \mask_2 \subseteq \mask_1 \cup \mask_3 \Rightarrow -% % valid(((p_1 \vs[\mask_1][\mask_2] p_2) \land (p_2 \vs[\mask_2][\mask_3] p_3)) \Rightarrow (p_1 \vs[\mask_1][\mask_3] p_3)) -% %\end{align*} -% %\end{lem} - -% %\begin{lem} -% %\begin{align*} -% %\MoveEqLeft -% % \All \iota \in \mathbb{N}. -% % \All p \in \textdom{Prop}. -% % \All W \in \textdom{World}. -% % \All \rs \in \textdom{Res}. -% % \All n \in \mathbb{N}. \\ -% %& -% % (n, \rs) \in inv(\iota, p)(W) \implies (n, \rs) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W) -% %\end{align*} -% %\end{lem} - -% % PDS: * undefined. -% %\begin{lem} -% %\begin{align*} -% %& -% % \forall \iota \in \mathbb{N}.~ -% % \forall p \in \textdom{Prop}.~ -% % \forall W \in \textdom{World}.~ -% % \forall \rs \in \textdom{Res}.~ -% % \forall n \in \mathbb{N}.~\\ -% %&\qquad -% % (n, \rs) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \rs) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W) -% %\end{align*} -% %\end{lem} - -% % \begin{lem} -% % \begin{align*} -% % & -% % \forall \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}).~ -% % valid(\bot \vs[\mask_1][\mask_2] \bot) -% % \end{align*} -% % \end{lem} - -% % PDS: E_1 ==>> E_2 undefined. -% %\begin{lem} -% %\begin{align*} -% %& -% % \forall p, q \in \textdom{Prop}.~ -% % \forall \mask \in \pset{\mathbb{N}}.~ -% %valid(\always{(p \Rightarrow q)} \Rightarrow (p \vs[\mask][\mask] q)) -% %\end{align*} -% %\end{lem} +\paragraph{Semantic domain of assertions.} +The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$. +We start by defining the functor that assembles the CMRAs we need to the global resource CMRA: +\begin{align*} + \textdom{ResF}(\cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: F(\cofe)} +\end{align*} +where $F$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$. +$\textdom{ResF}(\cofe)$ is a CMRA by lifting the individual CMRAs pointwise. +Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$. + +Now we can write down the recursive domain equation: +$\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp))$ +$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}. +We do not need to consider how the object is constructed. +We only need the isomorphism, given by +\begin{align*} + \Res &\eqdef \textdom{ResF}(\iPreProp) \\ + \iProp &\eqdef \UPred(\Res) \\ + \wIso &: \iProp \nfn \iPreProp \\ + \wIso^{-1} &: \iPreProp \nfn \iProp +\end{align*} -% % PDS: E # E' and E_1 ==>> E_2 undefined. -% %\begin{lem} -% %\begin{align*} -% %& -% % \forall p_1, p_2, p_3 \in \textdom{Prop}.~ -% % \forall \mask_1, \mask_2, \mask \in \pset{\mathbb{N}}.~ -% %valid(\mask \sep \mask_1 \Ra \mask \sep \mask_2 \Ra (p_1 \vs[\mask_1][\mask_2] p_2) \Rightarrow (p_1 * p_3 \vs[\mask_1 \cup \mask][\mask_2 \cup \mask] p_2 * p_3)) -% %\end{align*} -% %\end{lem} +We then pick $\iProp$ as the interpretation of $\Prop$: +$\Sem{\Prop} \eqdef \iProp$ -% \typedsection{Weakest precondition}{\mathit{wp} : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \to \textdom{Prop}) \to \textdom{Prop} \in {\cal U}} -% % \begin{align*} -% % \mathit{wp}_\mask(\expr, q) &\eqdef \Lam W. -% % \begin{aligned}[t] -% % \{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\wsat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\ -% % &\qquad -% % (\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\ -% % &\qquad\qquad -% % k \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\ -% % &\qquad -% % (\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\ -% % &\qquad\qquad -% % k - 1 \in (\wsat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\ -% % &\qquad -% % (\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\ -% % &\qquad\qquad -% % k - 1 \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\ -% % &\qquad\qquad -% % (k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land -% % (k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W')) -% % \,\} -% % \end{aligned} -% % \end{align*} -% \begin{lem} -% $\mathit{wp}$ is well-defined: $\mathit{wp}_{\mask}(\expr, q)$ is a valid proposition, and $\mathit{wp}$ is a non-expansive map. Besides, the dependency on the recursive occurrence is contractive, so $\mathit{wp}$ has a fixed-point. -% \end{lem} +\paragraph{Interpretation of assertions.} +$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply. +We only have to define the missing connectives, the most interesting bits being are primitive view shifts and weakest preconditions. -% \begin{lem} -% $\mathit{wp}$ on values and non-mask-changing $\mathit{vs}$ agree: -% $\mathit{wp}_\mask(\val, q) = \mathit{vs}_{\mask}^{\mask}(q \: \val)$ -% \end{lem} +\typedsection{World satisfaction}{\wsat{-}{-}{-} : + \Delta\textdom{State} \times + \Delta\pset{\mathbb{N}} \times + \textdom{Res} \nfn \SProp } +\begin{align*} + \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t] + \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land + \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\ + \All\iname \in \mask, \prop. \rs.\wld(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname)) + \end{inbox}\\ + \wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))} +\end{align*} -% \begin{align*} -% \Sem{\vctx \proves x : \sort}_\gamma &= \gamma(x) \\ -% \Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &= \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \ \WHEN \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn \\ -% \Sem{\vctx \proves \Lam x. \term : \sort \to \sort'}_\gamma &= -% \Lam v : \Sem{\sort}. \Sem{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\ -% \Sem{\vctx \proves \term~\termB : \sort'}_\gamma &= -% \Sem{\vctx \proves \term : \sort \to \sort'}_\gamma(\Sem{\vctx \proves \termB : \sort}_\gamma) \\ -% \Sem{\vctx \proves \unitval : \unitsort}_\gamma &= \star \\ -% \Sem{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\Sem{\vctx \proves \term_1 : \sort_1}_\gamma, \Sem{\vctx \proves \term_2 : \sort_2}_\gamma) \\ -% \Sem{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\Sem{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma) -% \end{align*} -% % -% \begin{align*} -% \Sem{\vctx \proves \mzero : \textsort{Monoid}}_\gamma &= \mzero \\ -% \Sem{\vctx \proves \munit : \textsort{Monoid}}_\gamma &= \munit \\ -% \Sem{\vctx \proves \melt \mtimes \meltB : \textsort{Monoid}}_\gamma &= -% \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textsort{Monoid}}_\gamma -% \end{align*} -% % -% \Sem{\vctx \proves \MU x. \pred : \sort \to \Prop}_\gamma &\eqdef -% \mathit{fix}(\Lam v : \Sem{\sort \to \Prop}. \Sem{\vctx, x : \sort \to \Prop \proves \pred : \sort \to \Prop}_{\gamma[x \mapsto v]}) \\ +\typedsection{Primitive view-shift}{\mathit{pvs} : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} +\begin{align*} + \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} + \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& + \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} + \end{aligned}} +\end{align*} +\typedsection{Weakest precondition}{\mathit{wp} : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp} - % \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &= - % inv(\Sem{\vctx \proves \iname : \textsort{InvName}}_\gamma, \Sem{\vctx \proves \prop : \Prop}_\gamma) \\ - % \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &= - % \Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\ - % \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &= - % \Lam W. \{\, (n, \rs) \mid \rs.\pres = \Sem{\vctx \proves \state : \textsort{State}}_\gamma \,\} +$\textdom{wp}$ is defined as the fixed-point of a contractive function. +\begin{align*} + \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} + \All &\rs_\f, m, \mask_f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ + &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\ + &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ + &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ + &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2)) + \end{aligned}} \\ + \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred) +\end{align*} -% % -% \begin{align*} -% \Sem{\vctx \proves \pvsA{\prop}{\mask_1}{\mask_2} : \Prop}_\gamma &= -% \textdom{vs}^{\Sem{\vctx \proves \mask_2 : \textsort{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\ -% \Sem{\vctx \proves \dynA{\expr}{\pred}{\mask} : \Prop}_\gamma &= -% \textdom{wp}_{\Sem{\vctx \proves \mask : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textsort{Exp}}_\gamma, \Sem{\vctx \proves \pred : \textsort{Val} \to \Prop}_\gamma) \\ -% \Sem{\vctx \proves \wtt{\timeless{\prop}}{\Prop}}_\gamma &= -% \textdom{timeless}(\Sem{\vctx \proves \prop : \Prop}_\gamma) -% \end{align*} +\typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp} -% \typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2 \in \mathit{Sets}} +\begin{align*} + \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\ + \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &\eqdef \ownM{\munit, \munit, \melt} \\ + \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &\eqdef \ownM{\munit, \exinj(\state), \munit} \\ + \Sem{\vctx \proves \pvs[\mask_1][\mask_2] \prop : \Prop}_\gamma &\eqdef + \textdom{pvs}^{\Sem{\vctx \proves \mask_2 : \textlog{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\ + \Sem{\vctx \proves \wpre{\expr}[\mask]{\Ret\var.\prop} : \Prop}_\gamma &\eqdef + \textdom{wp}_{\Sem{\vctx \proves \mask : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textlog{Expr}}_\gamma, \Lam\val. \Sem{\vctx \proves \prop : \Prop}_{\gamma[\var\mapsto\val]}) +\end{align*} -% -% \Sem{\vctx \mid \pfctx \proves \propB} \eqdef -% \begin{aligned}[t] -% \MoveEqLeft -% \forall n \in \mathbb{N}.\; -% \forall W \in \textdom{World}.\; -% \forall \rs \in \textdom{Res}.\; -% \forall \gamma \in \Sem{\vctx},\; -% \\& -% \bigl(\All \propB \in \pfctx. (n, \rs) \in \Sem{\vctx \proves \propB : \Prop}_\gamma(W)\bigr) -% \implies (n, \rs) \in \Sem{\vctx \proves \prop : \Prop}_\gamma(W) -% \end{aligned} -% +\paragraph{Remaining semantic domains, and interpretation of non-assertion terms.} + +The remaining domains are interpreted as follows: +$+\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{\textlog{InvName}} &\eqdef& \Delta \mathbb{N} \\ +\Sem{\textlog{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ +\Sem{\textlog{M}} &\eqdef& F(\iProp) +\end{array} +\qquad\qquad +\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{\textlog{Val}} &\eqdef& \Delta \textdom{Val} \\ +\Sem{\textlog{Expr}} &\eqdef& \Delta \textdom{Expr} \\ +\Sem{\textlog{State}} &\eqdef& \Delta \textdom{State} \\ +\end{array} +\qquad\qquad +\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{1} &\eqdef& \Delta \{ () \} \\ +\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\ +\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\ +\end{array} +$ + +The balance of our signature $\Sig$ is interpreted as follows. +For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define +$+\Sem{\type} \eqdef X_\type +$ +For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick a function $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \nfn \Sem{\type_{n+1}}$. + +\typedsection{Interpretation of non-propositional terms}{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}} +\begin{align*} + \Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\ + \Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\ + \Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef + \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\ + \Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef + \Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\ + \Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef + \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\ + ~\\ + \Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\ + \Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\ + \Sem{\vctx \proves \pi_i(\term) : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\ + ~\\ + \Sem{\vctx \proves \munit : \textlog{M}}_\gamma &\eqdef \munit \\ + \Sem{\vctx \proves \mcore\melt : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma} \\ + \Sem{\vctx \proves \melt \mtimes \meltB : \textlog{M}}_\gamma &\eqdef + \Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textlog{M}}_\gamma +\end{align*} +% + +An environment $\vctx$ is interpreted as the set of +finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and +$\rho(x)\in\Sem{\vctx(x)}$. + +\paragraph{Logical entailment.} +We can now define \emph{semantic} logical entailment. + +\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2} + ++\Sem{\vctx \mid \pfctx \proves \propB} \eqdef +\begin{aligned}[t] +\MoveEqLeft +\forall n \in \mathbb{N}.\; +\forall \rs \in \textdom{Res}.\; +\forall \gamma \in \Sem{\vctx},\; +\\& +\bigl(\All \propB \in \pfctx. n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)\bigr) +\Ra n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs) +\end{aligned} + + +The soundness statement of the logic reads +$\vctx \mid \pfctx \proves \prop \Ra \Sem{\vctx \mid \pfctx \proves \prop}$ %%% Local Variables: %%% mode: latex