base-logic.tex 12.6 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 29 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 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.} Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$). 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 06, 2016 211 212  {\prop \proves \propB \\ \prop \proves \term =_\type \term'} {\prop \proves \propB[\term'/\term]}  Ralf Jung committed Oct 04, 2016 213 214 215 \and \infer[Refl] {}  Ralf Jung committed Oct 06, 2016 216  {\prop \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 04, 2016 267 268 \and \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 292 293 294 295 296 297 298 299 300 301 302 303 304 305 % \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 \\ \prop * \propB &\provesIff& \propB * \prop \\ (\prop * \propB) * \propC &\provesIff& \prop * (\propB * \propC) \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 04, 2016 312 \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 06, 2016 313  \TRUE &\proves& \always{\TRUE} \\  Ralf Jung committed Oct 04, 2016 314 315 316 317  \always{\prop} &\proves& \prop \\ \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB \end{array}  Ralf Jung committed Oct 04, 2016 318 \and  Ralf Jung committed Oct 04, 2016 319 320 321 322 \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 323 324 325 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 326   Ralf Jung committed Oct 04, 2016 327 328 329 \paragraph{Laws for the later modality.} \begin{mathpar} \infer[$\later$-mono]  Ralf Jung committed Oct 04, 2016 330 331  {\prop \proves \propB} {\later\prop \proves \later{\propB}}  Ralf Jung committed Oct 04, 2016 332 333 334 335 336 337 \and \infer[L{\"o}b] {} {(\later\prop\Ra\prop) \proves \prop} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 338 339 340  \All x. \later\prop &\proves& \later{\All x.\prop} \\ \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\ \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \\  Ralf Jung committed Oct 04, 2016 341 342 343 \end{array} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 344 345  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\ \always{\later\prop} &\provesIff& \later\always{\prop} \\  Ralf Jung committed Oct 04, 2016 346 347 348 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 349 350  \paragraph{Laws for ghosts and validity.}  Ralf Jung committed Oct 04, 2016 351 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 352 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 353 354 355 356 \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 357 358 \end{array} \and  Ralf Jung committed Oct 04, 2016 359 360 361 \infer[valid-intro] {\melt \in \mval} {\TRUE \vdash \mval(\melt)}  Ralf Jung committed Oct 04, 2016 362 \and  Ralf Jung committed Oct 04, 2016 363 364 365 \infer[valid-elim] {\melt \notin \mval_0} {\mval(\melt) \proves \FALSE}  Ralf Jung committed Oct 04, 2016 366 \and  Ralf Jung committed Oct 04, 2016 367 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 368 \ownM{\melt} &\proves& \mval(\melt) \\  Ralf Jung committed Oct 04, 2016 369 370 371 \mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\ \mval(\melt) &\proves& \always\mval(\melt) \end{array}  Ralf Jung committed Oct 04, 2016 372 373 \end{mathpar}  Ralf Jung committed Oct 04, 2016 374   Ralf Jung committed Oct 04, 2016 375 376 \paragraph{Laws for the update modality.} \begin{mathpar}  Ralf Jung committed Oct 04, 2016 377 378 379 380 \infer[upd-mono] {\prop \proves \propB} {\upd\prop \proves \upd\propB}  Ralf Jung committed Oct 04, 2016 381 382 383 384 385 386 387 388 389 390 391 392 \infer[upd-intro] {}{\prop \proves \upd \prop} \infer[upd-trans] {} {\upd \upd \prop \proves \upd \prop} \infer[upd-frame] {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update} {\melt \mupd \meltsB}  Ralf Jung committed Oct 04, 2016 393 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Oct 04, 2016 394 395 396 397 \end{mathpar} \subsection{Soundness}  Ralf Jung committed Oct 04, 2016 398 399 400 401 402 The soundness statement of the logic reads as follows: For any $n$, we have \begin{align*} \lnot(\TRUE \vdash (\upd\later)^n \FALSE) \end{align*} where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.  Ralf Jung committed Oct 04, 2016 403 404 405 406 407 408  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: