extended-logic.tex 12.8 KB
 Ralf Jung committed Dec 10, 2017 1 \section{Extensions of the Base Logic}  Ralf Jung committed Oct 10, 2016 2   Ralf Jung committed Oct 22, 2016 3 In this section we discuss some additional constructions that we define within and on top of the base logic.  Ralf Jung committed Oct 10, 2016 4 5 These are not extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.  Ralf Jung committed Dec 10, 2017 6 \subsection{Derived Rules about Base Connectives}  Ralf Jung committed Oct 10, 2016 7 8 We collect here some important and frequently used derived proof rules. \begin{mathparpagebreakable}  Ralf Jung committed Jun 05, 2019 9 10 11 12  \inferhref{L{\"o}b}{Loeb} {} {(\later\prop\Ra\prop) \proves \prop}  Ralf Jung committed Oct 10, 2016 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39  \infer{} {\prop \Ra \propB \proves \prop \wand \propB} \infer{} {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB} \infer{} {\prop * \All\var.\propB \proves \All\var. \prop * \propB} \infer{} {\always(\prop*\propB) \provesIff \always\prop * \always\propB} \infer{} {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB} \infer{} {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB} \infer{} {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)} \infer{} {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB} \infer{} {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}  Ralf Jung committed Nov 28, 2017 40 41  \infer{} {\TRUE \proves \plainly\TRUE}  Ralf Jung committed Oct 10, 2016 42 43 \end{mathparpagebreakable}  Ralf Jung committed Jun 06, 2019 44 45 Noteworthy here is the fact that Löb induction can be derived from $\later$-introduction and the fact that we can take fixed-points of functions where the recursive occurrences are below $\later$~\cite{Loeb}.% \footnote{Also see \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}  Ralf Jung committed Jun 05, 2019 46 47 Furthermore, $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$. To derive that existential quantifiers commute with separating conjunction requires an intermediate step using a magic wand: From $P * \exists x, Q \vdash \Exists x. P * Q$ we can deduce $\Exists x. Q \vdash P \wand \Exists x. P * Q$ and then proceed via $\exists$-elimination.  Ralf Jung committed Nov 28, 2017 48   Robbert Krebbers committed Dec 10, 2017 49 50 \subsection{Persistent Propositions} We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.  Robbert Krebbers committed Dec 10, 2017 51 These are propositions that do not own anything'', so we can (and will) treat them like normal'' intuitionistic propositions.  Ralf Jung committed Oct 10, 2016 52 53 54 55 56 57 58  Of course, $\always\prop$ is persistent for any $\prop$. Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent. Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification and $\later$.  Ralf Jung committed Dec 10, 2017 59 \subsection{Timeless Propositions and Except-0}  Ralf Jung committed Oct 10, 2016 60 61 62  One of the troubles of working in a step-indexed logic is the later'' modality $\later$. It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:  Ralf Jung committed Dec 05, 2016 63 $\diamond \prop \eqdef \later\FALSE \lor \prop$  Ralf Jung committed Apr 29, 2019 64 Except-0 satisfies the usual laws of a monadic'' modality (similar to, \eg the update modalities):  Ralf Jung committed Oct 10, 2016 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 \begin{mathpar} \inferH{ex0-mono} {\prop \proves \propB} {\diamond\prop \proves \diamond\propB} \axiomH{ex0-intro} {\prop \proves \diamond\prop} \axiomH{ex0-idem} {\diamond\diamond\prop \proves \diamond\prop} \begin{array}[c]{rMcMl} \diamond{(\prop * \propB)} &\provesIff& \diamond\prop * \diamond\propB \\ \diamond{(\prop \land \propB)} &\provesIff& \diamond\prop \land \diamond\propB \\ \diamond{(\prop \lor \propB)} &\provesIff& \diamond\prop \lor \diamond\propB \end{array} \begin{array}[c]{rMcMl} \diamond{\All x. \prop} &\provesIff& \All x. \diamond{\prop} \\ \diamond{\Exists x. \prop} &\provesIff& \Exists x. \diamond{\prop} \\ \diamond\always{\prop} &\provesIff& \always\diamond{\prop} \\ \diamond\later\prop &\proves& \later{\prop} \end{array} \end{mathpar}  Ralf Jung committed Apr 29, 2019 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 In particular, from \ruleref{ex0-mono} and \ruleref{ex0-idem} we can derive a bind''-like elimination rule: \begin{mathpar} \inferH{ex0-elim} {\prop \proves \diamond\propB} {\diamond\prop \proves \diamond\propB} \end{mathpar} This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have $\timeless{\prop} \eqdef \later\prop \proves \diamond\prop$ In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions (using \ruleref{ex0-elim}): \begin{mathpar} \inferH{ex0-timeless-strip}{\timeless{\prop} \and \prop \proves \diamond\propB} {\later\prop \proves \diamond\propB} \end{mathpar} In fact, it turns out that we can strip away later from timeless propositions even when working under the later modality: \begin{mathpar} \inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB} {\later\prop \proves \later\propB} \end{mathpar} This follows from $\later \prop \proves \later\FALSE \lor \prop$, and then by straightforward disjunction elimination.  Ralf Jung committed Oct 10, 2016 111   Robbert Krebbers committed Dec 10, 2017 112 The following rules identify the class of timeless propositions:  Ralf Jung committed Oct 10, 2016 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 \begin{mathparpagebreakable} \infer {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}} {\vctx \proves \timeless{\prop \land \propB}} \infer {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}} {\vctx \proves \timeless{\prop \lor \propB}} \infer {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}} {\vctx \proves \timeless{\prop * \propB}} \infer {\vctx \proves \timeless{\prop}} {\vctx \proves \timeless{\always\prop}} \infer {\vctx \proves \timeless{\propB}} {\vctx \proves \timeless{\prop \Ra \propB}} \infer {\vctx \proves \timeless{\propB}} {\vctx \proves \timeless{\prop \wand \propB}} \infer {\vctx,\var:\type \proves \timeless{\prop}} {\vctx \proves \timeless{\All\var:\type.\prop}} \infer {\vctx,\var:\type \proves \timeless{\prop}} {\vctx \proves \timeless{\Exists\var:\type.\prop}} \axiom{\timeless{\TRUE}} \axiom{\timeless{\FALSE}} \infer  Ralf Jung committed Dec 05, 2016 151 {\text{$\term$ or $\term'$ is a discrete OFE element}}  Ralf Jung committed Oct 10, 2016 152 153 154 {\timeless{\term =_\type \term'}} \infer  Ralf Jung committed Dec 05, 2016 155 {\text{$\melt$ is a discrete OFE element}}  Ralf Jung committed Oct 10, 2016 156 157 158 {\timeless{\ownM\melt}} \infer  Robbert Krebbers committed Dec 10, 2017 159 {\text{$\melt$ is an element of a discrete camera}}  Ralf Jung committed Oct 10, 2016 160 161 162 {\timeless{\mval(\melt)}} \end{mathparpagebreakable}  Ralf Jung committed Oct 06, 2016 163   Ralf Jung committed Dec 11, 2017 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 \subsection{Dynamic Composeable Higher-Order Resources} \label{sec:composeable-resources} The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources. It turns out that we can generalize this further and permit picking cameras $\iFunc(\Prop)$'' that depend on the structure of propositions themselves. Of course, $\Prop$ is just the syntactic type of propositions; for this to make sense we have to look at the semantics. Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined. Finally, in many cases just having a single instance'' of a camera available for reasoning is not enough. For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance. While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution. The purpose of this section is to describe how we solve these issues. \paragraph{Picking the resources.} The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.  Robbert Krebbers committed Jun 04, 2019 181 To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.  Ralf Jung committed Dec 11, 2017 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 (This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.) From this, we construct the bifunctor defining the overall resources as follows: \begin{align*} \GName \eqdef{}& \nat \\ \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe) \end{align*} We will motivate both the use of a product and the finite partial function below. $\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial function). Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$. Now we can write down the recursive domain equation: $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp))$ Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}, so we obtain some object $\iPreProp$ such that: \begin{align*} \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\ \iProp &\eqdef \UPred(\Res) \\ \wIso &: \iProp \nfn \iPreProp \\ \wIso^{-1} &: \iPreProp \nfn \iProp \\ \wIso(\wIso^{-1}(x)) &\eqdef x \\ \wIso^{-1}(\wIso(x)) &\eqdef x \end{align*} Now we can instantiate the base logic described in \Sref{sec:base-logic} with $\Res$ as the chosen camera: $\Sem{\Prop} \eqdef \UPred(\Res)$ We obtain that $\Sem{\Prop} = \iProp$. Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$. We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic. \paragraph{Proof composability.} To make our proofs composeable, we \emph{generalize} our proofs over the family of functors. This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product pointwise''. So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}. Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors. Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors. Only when the top-level proof is completed we will close'' the proof by picking a concrete family that contains exactly those functors the proof needs. \paragraph{Dynamic resources.} Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for: Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state. This is best demonstrated by giving some proof rules. So let us first define the notion of ghost ownership that we use in this logic. Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define: $\ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)}$ This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function. We can show the following properties for this form of ownership: \begin{mathparpagebreakable} \inferH{res-alloc}{\text{$G$ infinite} \and \melt \in \mval_{M_i}} { \TRUE \proves \upd \Exists\gname\in G. \ownGhost\gname{\melt : M_i} } \and \inferH{res-update} {\melt \mupd_{M_i} B} {\ownGhost\gname{\melt : M_i} \proves \upd \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}} \inferH{res-empty} {\text{$\munit$ is a unit of $M_i$}} {\TRUE \proves \upd \ownGhost\gname\munit} \axiomH{res-op} {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \provesIff \ownGhost\gname{\melt\mtimes\meltB : M_i}} \axiomH{res-valid} {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)} \inferH{res-timeless} {\text{$\melt$ is a discrete OFE element}} {\timeless{\ownGhost\gname{\melt : M_i}}} \end{mathparpagebreakable} Below, we will always work within (an instance of) the logic as described here. Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors. We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.  Ralf Jung committed Oct 06, 2016 262 263 264 265 266  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: