base-logic.tex 13.3 KB
 Ralf Jung committed Oct 04, 2016 1 2 3 \section{Base Logic} \label{sec:base-logic}  Ralf Jung committed Oct 06, 2016 4 The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.  Ralf Jung committed Oct 06, 2016 5 By \lemref{lem:cmra-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.  Ralf Jung committed Oct 04, 2016 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 This defines the structure of resources that can be owned. As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language. You have to make sure that $\SigType$ includes the base types: $\SigType \supseteq \{ \textlog{M}, \Prop \}$ Elements of $\SigType$ are ranged over by $\sigtype$. Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$). We write $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$ to express that $\sigfn$ is a function symbol with the indicated arity. Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$. Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$. Elements of $\SigAx$ are ranged over by $\sigax$. \subsection{Grammar}\label{sec:grammar} \paragraph{Syntax.}  Robbert Krebbers committed Oct 17, 2016 29 Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$).  Ralf Jung committed Oct 04, 2016 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \begin{align*} \type \bnfdef{}& \sigtype \mid 1 \mid \type \times \type \mid \type \to \type \\[0.4em] \term, \prop, \pred \bnfdef{}& \var \mid \sigfn(\term_1, \dots, \term_n) \mid () \mid (\term, \term) \mid \pi_i\; \term \mid \Lam \var:\type.\term \mid \term(\term) \mid \melt \mid \mcore\term \mid \term \mtimes \term \mid \\& \FALSE \mid \TRUE \mid \term =_\type \term \mid \prop \Ra \prop \mid \prop \land \prop \mid \prop \lor \prop \mid \prop * \prop \mid \prop \wand \prop \mid \\& \MU \var:\type. \term \mid \Exists \var:\type. \prop \mid \All \var:\type. \prop \mid \\&  Ralf Jung committed Oct 04, 2016 64  \ownM{\term} \mid \mval(\term) \mid  Ralf Jung committed Oct 04, 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 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 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 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170  \always\prop \mid {\later\prop} \mid \upd \prop\mid \end{align*} Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$. \paragraph{Variable conventions.} We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence. \subsection{Types}\label{sec:types} Iris terms are simply-typed. The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$. A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types. In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$. \judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}} \begin{mathparpagebreakable} %%% variables and function symbols \axiom{x : \type \proves \wtt{x}{\type}} \and \infer{\vctx \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term}{\type}} \and \infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}} \and \infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}} {\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}} \and \infer{ \vctx \proves \wtt{\term_1}{\type_1} \and \cdots \and \vctx \proves \wtt{\term_n}{\type_n} \and \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn }{ \vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}} } %%% products \and \axiom{\vctx \proves \wtt{()}{1}} \and \infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}} {\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}} \and \infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}} {\vctx \proves \wtt{\pi_i\,\term}{\type_i}} %%% functions \and \infer{\vctx, x:\type \proves \wtt{\term}{\type'}} {\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}} \and \infer {\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 \infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}} {\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}} %%% props and predicates \\ \axiom{\vctx \proves \wtt{\FALSE}{\Prop}} \and \axiom{\vctx \proves \wtt{\TRUE}{\Prop}} \and \infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}} {\vctx \proves \wtt{\term =_\type \termB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \Ra \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \land \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \lor \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop * \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \wand \propB}{\Prop}} \and \infer{ \vctx, \var:\type \proves \wtt{\term}{\type} \and \text{$\var$ is guarded in $\term$} }{ \vctx \proves \wtt{\MU \var:\type. \term}{\type} } \and \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}} \and \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\All x:\type. \prop}{\Prop}} \and \infer{\vctx \proves \wtt{\melt}{\textlog{M}}}  Ralf Jung committed Oct 04, 2016 171  {\vctx \proves \wtt{\ownM{\melt}}{\Prop}}  Ralf Jung committed Oct 04, 2016 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 \and \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}} {\vctx \proves \wtt{\mval(\melt)}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\always\prop}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\later\prop}{\Prop}} \and \infer{ \vctx \proves \wtt{\prop}{\Prop} }{ \vctx \proves \wtt{\upd \prop}{\Prop} } \end{mathparpagebreakable} \subsection{Proof rules} \label{sec:proof-rules}  Ralf Jung committed Oct 06, 2016 192 193 194 195 196 The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds. Most of the rules will entirely omit the variable contexts $\vctx$. In this case, we assume the same arbitrary context is used for every constituent of the rules. %Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent. Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ are proof rules of the logic.  Ralf Jung committed Oct 04, 2016 197   Ralf Jung committed Oct 06, 2016 198 \judgment{\vctx \mid \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 199 200 201 202 \paragraph{Laws of intuitionistic higher-order logic with equality.} This is entirely standard. \begin{mathparpagebreakable} \infer[Asm]  Ralf Jung committed Oct 06, 2016 203 204 205 206 207 208  {} {\prop \proves \prop} \and \infer[Subst] {\prop \proves \propB \and \propB \proves \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 209 210 \and \infer[Eq]  Ralf Jung committed Oct 07, 2016 211 212  {\vctx,\var:\type \proves \wtt\propB\Prop \\ \vctx\mid\prop \proves \propB[\term/\var] \\ \vctx\mid\prop \proves \term =_\type \term'} {\vctx\mid\prop \proves \propB[\term'/\var]}  Ralf Jung committed Oct 04, 2016 213 214 215 \and \infer[Refl] {}  Ralf Jung committed Oct 07, 2016 216  {\TRUE \proves \term =_\type \term}  Ralf Jung committed Oct 04, 2016 217 218 \and \infer[$\bot$E]  Ralf Jung committed Oct 06, 2016 219 220  {} {\FALSE \proves \prop}  Ralf Jung committed Oct 04, 2016 221 222 223 \and \infer[$\top$I] {}  Ralf Jung committed Oct 06, 2016 224  {\prop \proves \TRUE}  Ralf Jung committed Oct 04, 2016 225 226 \and \infer[$\wedge$I]  Ralf Jung committed Oct 06, 2016 227 228  {\prop \proves \propB \\ \prop \proves \propC} {\prop \proves \propB \land \propC}  Ralf Jung committed Oct 04, 2016 229 230 \and \infer[$\wedge$EL]  Ralf Jung committed Oct 06, 2016 231 232  {\prop \proves \propB \land \propC} {\prop \proves \propB}  Ralf Jung committed Oct 04, 2016 233 234 \and \infer[$\wedge$ER]  Ralf Jung committed Oct 06, 2016 235 236  {\prop \proves \propB \land \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 237 238 \and \infer[$\vee$IL]  Ralf Jung committed Oct 06, 2016 239 240  {\prop \proves \propB } {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 241 242 \and \infer[$\vee$IR]  Ralf Jung committed Oct 06, 2016 243 244  {\prop \proves \propC} {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 245 246 \and \infer[$\vee$E]  Ralf Jung committed Oct 06, 2016 247 248 249  {\prop \proves \propC \\ \propB \proves \propC} {\prop \lor \propB \proves \propC}  Ralf Jung committed Oct 04, 2016 250 251 \and \infer[$\Ra$I]  Ralf Jung committed Oct 06, 2016 252 253  {\prop \land \propB \proves \propC} {\prop \proves \propB \Ra \propC}  Ralf Jung committed Oct 04, 2016 254 255 \and \infer[$\Ra$E]  Ralf Jung committed Oct 06, 2016 256 257  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 258 259 \and \infer[$\forall$I]  Ralf Jung committed Oct 06, 2016 260 261  { \vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\prop \proves \All \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 262 263 \and \infer[$\forall$E]  Ralf Jung committed Oct 06, 2016 264  {\vctx\mid\prop \proves \All \var :\type. \propB \\  Ralf Jung committed Oct 04, 2016 265  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 266  {\vctx\mid\prop \proves \propB[\term/\var]}  Ralf Jung committed Oct 07, 2016 267 \\  Ralf Jung committed Oct 04, 2016 268 \infer[$\exists$I]  Ralf Jung committed Oct 06, 2016 269  {\vctx\mid\prop \proves \propB[\term/\var] \\  Ralf Jung committed Oct 04, 2016 270  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 271  {\vctx\mid\prop \proves \exists \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 272 273 \and \infer[$\exists$E]  Ralf Jung committed Oct 06, 2016 274 275  {\vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\Exists \var: \type. \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 % \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} \begin{array}{rMcMl} \TRUE * \prop &\provesIff& \prop \\  Robbert Krebbers committed Oct 14, 2016 292 293  \prop * \propB &\proves& \propB * \prop \\ (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)  Ralf Jung committed Oct 04, 2016 294 295 296 297 298 299 300 301 302 303 304 305 \end{array} \and \infer[$*$-mono] {\prop_1 \proves \propB_1 \and \prop_2 \proves \propB_2} {\prop_1 * \prop_2 \proves \propB_1 * \propB_2} \and \inferB[$\wand$I-E] {\prop * \propB \proves \propC} {\prop \proves \propB \wand \propC} \end{mathpar}  Ralf Jung committed Oct 04, 2016 306 \paragraph{Laws for the always modality.}  Ralf Jung committed Oct 04, 2016 307 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 308 309 310 \infer[$\always$-mono] {\prop \proves \propB} {\always{\prop} \proves \always{\propB}}  Ralf Jung committed Oct 04, 2016 311 \and  Ralf Jung committed Oct 10, 2016 312 313 314 \infer[$\always$-E]{} {\always\prop \proves \prop} \and  Ralf Jung committed Oct 04, 2016 315 \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 06, 2016 316  \TRUE &\proves& \always{\TRUE} \\  Ralf Jung committed Oct 04, 2016 317 318 319  \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB \end{array}  Ralf Jung committed Oct 04, 2016 320 \and  Ralf Jung committed Oct 04, 2016 321 322 323 324 \begin{array}[c]{rMcMl} \always{\prop} &\proves& \always\always\prop \\ \All x. \always{\prop} &\proves& \always{\All x. \prop} \\ \always{\Exists x. \prop} &\proves& \Exists x. \always{\prop}  Ralf Jung committed Oct 04, 2016 325 326 327 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 328   Ralf Jung committed Oct 04, 2016 329 330 331 \paragraph{Laws for the later modality.} \begin{mathpar} \infer[$\later$-mono]  Ralf Jung committed Oct 04, 2016 332 333  {\prop \proves \propB} {\later\prop \proves \later{\propB}}  Ralf Jung committed Oct 04, 2016 334 335 336 337 338 339 \and \infer[L{\"o}b] {} {(\later\prop\Ra\prop) \proves \prop} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 340 341  \All x. \later\prop &\proves& \later{\All x.\prop} \\ \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\  Ralf Jung committed Oct 14, 2016 342  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)  Ralf Jung committed Oct 04, 2016 343 344 345 \end{array} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 346  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\  Ralf Jung committed Oct 14, 2016 347  \always{\later\prop} &\provesIff& \later\always{\prop}  Ralf Jung committed Oct 04, 2016 348 349 350 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 351   Ralf Jung committed Oct 13, 2016 352 \paragraph{Laws for resources and validity.}  Ralf Jung committed Oct 04, 2016 353 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 354 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 355 356 357 358 \ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\ \ownM\melt &\proves& \always{\ownM{\mcore\melt}} \\ \TRUE &\proves& \ownM{\munit} \\ \later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)  Ralf Jung committed Oct 04, 2016 359 \end{array}  Ralf Jung committed Oct 13, 2016 360 361 362 363 364 365 366 367 % \and % \infer[valid-intro] % {\melt \in \mval} % {\TRUE \vdash \mval(\melt)} % \and % \infer[valid-elim] % {\melt \notin \mval_0} % {\mval(\melt) \proves \FALSE}  Ralf Jung committed Oct 04, 2016 368 \and  Ralf Jung committed Oct 04, 2016 369 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 370 \ownM{\melt} &\proves& \mval(\melt) \\  Ralf Jung committed Oct 04, 2016 371 372 373 \mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\ \mval(\melt) &\proves& \always\mval(\melt) \end{array}  Ralf Jung committed Oct 04, 2016 374 375 \end{mathpar}  Ralf Jung committed Oct 04, 2016 376   Ralf Jung committed Oct 06, 2016 377 \paragraph{Laws for the resource update modality.}  Ralf Jung committed Oct 04, 2016 378 \begin{mathpar}  Ralf Jung committed Oct 14, 2016 379 \inferH{upd-mono}  Ralf Jung committed Oct 04, 2016 380 381 382 {\prop \proves \propB} {\upd\prop \proves \upd\propB}  Ralf Jung committed Oct 14, 2016 383 \inferH{upd-intro}  Ralf Jung committed Oct 04, 2016 384 385 {}{\prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 386 \inferH{upd-trans}  Ralf Jung committed Oct 04, 2016 387 388 389 {} {\upd \upd \prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 390 \inferH{upd-frame}  Ralf Jung committed Oct 04, 2016 391 392 393 394 {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update} {\melt \mupd \meltsB}  Ralf Jung committed Oct 04, 2016 395 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Oct 04, 2016 396 \end{mathpar}  Ralf Jung committed Oct 13, 2016 397 398 The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$. \ralf{Trouble is, we don't actually have $\in$ inside the logic...}  Ralf Jung committed Oct 04, 2016 399   Ralf Jung committed Oct 07, 2016 400 \subsection{Consistency}  Ralf Jung committed Oct 04, 2016 401   Ralf Jung committed Oct 07, 2016 402 The consistency statement of the logic reads as follows: For any $n$, we have  Ralf Jung committed Oct 04, 2016 403 \begin{align*}  Ralf Jung committed Oct 07, 2016 404  \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)  Ralf Jung committed Oct 04, 2016 405 406 \end{align*} where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.  Ralf Jung committed Oct 04, 2016 407   Ralf Jung committed Oct 07, 2016 408 409 410 411 The reason we want a stronger consistency than the usual $\lnot(\TRUE \proves \FALSE)$ is our modalities: it should be impossible to derive a contradiction below the modalities. For $\always$, this follows from the elimination rule, but the other two modalities do not have an elimination rule. Hence we declare that it is impossible to derive a contradiction below any combination of these two modalities.  Ralf Jung committed Oct 04, 2016 412 413 414 415 416  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: