logic.tex 15.8 KB
 Ralf Jung committed Mar 06, 2016 1 \section{Language}  Ralf Jung committed Jan 31, 2016 2   Ralf Jung committed Mar 06, 2016 3 A \emph{language} $\Lang$ consists of a set \textdom{Exp} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that  Ralf Jung committed Jan 31, 2016 4 \begin{itemize}  Ralf Jung committed Mar 06, 2016 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 \item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that \begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val} \end{mathpar} \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{()})$ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$. \\ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ is forked off. \item All values are stuck: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \item There is a predicate defining \emph{atomic} expressions satisfying \let\oldcr\cr \begin{mathpar} {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {{ \begin{inbox} \All\expr_1, \state_1, \expr_2, \state_2, \expr'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 \end{inbox} }} \end{mathpar} In other words, atomic expression \emph{reduce in one step to a value}. It does not matter whether they fork off an arbitrary expression.  Ralf Jung committed Jan 31, 2016 25 26 \end{itemize}  Ralf Jung committed Mar 06, 2016 27 28 29 \subsection{The concurrent language} For any language $\Lang$, we define the corresponding thread-pool semantics.  Ralf Jung committed Jan 31, 2016 30 31 32  \paragraph{Machine syntax} $ Ralf Jung committed Mar 06, 2016 33  \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n  Ralf Jung committed Jan 31, 2016 34 35 $  Ralf Jung committed Mar 06, 2016 36 37 \judgment{Machine reduction} {\cfg{\tpool}{\state} \step \cfg{\tpool'}{\state'}}  Ralf Jung committed Jan 31, 2016 38 39 \begin{mathpar} \infer  Ralf Jung committed Mar 06, 2016 40 41 42 43 44 45 46  {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}} \and\infer {\expr_1, \state_1 \step \expr_2, \state_2} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state'}}  Ralf Jung committed Jan 31, 2016 47 48 49 \end{mathpar}  Ralf Jung committed Mar 06, 2016 50 51 52 53 54 55 56 \section{The logic} To instantiate Iris, you need to define the following parameters: \begin{itemize} \item A language $\Lang$ \item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state \end{itemize}  Ralf Jung committed Jan 31, 2016 57   Ralf Jung committed Mar 06, 2016 58 59 60 \noindent 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:  Ralf Jung committed Jan 31, 2016 61 $ Ralf Jung committed Mar 06, 2016 62  \SigType \supseteq \{ \textsort{Val}, \textsort{Expr}, \textsort{State}, \textsort{M}, \textsort{InvName}, \textsort{InvMask}, \Prop \}  Ralf Jung committed Jan 31, 2016 63 $  Ralf Jung committed Mar 06, 2016 64 65 66 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$).  Ralf Jung committed Jan 31, 2016 67 68 69 70 71 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.  Ralf Jung committed Mar 06, 2016 72 73 74 75 76 77  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}  Ralf Jung committed Jan 31, 2016 78 79  \paragraph{Syntax.}  Ralf Jung committed Jan 31, 2016 80 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$):  Ralf Jung committed Feb 02, 2016 81   Ralf Jung committed Jan 31, 2016 82 \begin{align*}  Ralf Jung committed Mar 06, 2016 83 84 85 86 87 88  \type ::={}& \sigtype \mid \unitsort \mid \type \times \type \mid \type \to \type \0.4em]  Ralf Jung committed Jan 31, 2016 89  \term, \prop, \pred ::={}&  Ralf Jung committed Mar 06, 2016 90  \var \mid  Ralf Jung committed Jan 31, 2016 91  \sigfn(\term_1, \dots, \term_n) \mid  Ralf Jung committed Feb 02, 2016 92  \unitval \mid  Ralf Jung committed Jan 31, 2016 93 94  (\term, \term) \mid \pi_i\; \term \mid  Ralf Jung committed Mar 06, 2016 95  \Lam \var:\type.\term \mid  Ralf Jung committed Mar 06, 2016 96  \term(\term) \mid  Ralf Jung committed Jan 31, 2016 97 98 99 100 101  \munit \mid \term \mtimes \term \mid \\& \FALSE \mid \TRUE \mid  Ralf Jung committed Mar 06, 2016 102  \term =_\type \term \mid  Ralf Jung committed Jan 31, 2016 103 104 105 106 107 108  \prop \Ra \prop \mid \prop \land \prop \mid \prop \lor \prop \mid \prop * \prop \mid \prop \wand \prop \mid \\&  Ralf Jung committed Mar 06, 2016 109  \MU \var:\type. \pred \mid  Ralf Jung committed Mar 06, 2016 110 111  \Exists \var:\type. \prop \mid \All \var:\type. \prop \mid  Ralf Jung committed Jan 31, 2016 112 113 114 115 116 117 118 \\& \knowInv{\term}{\prop} \mid \ownGGhost{\term} \mid \ownPhys{\term} \mid \always\prop \mid {\later\prop} \mid \pvsA{\prop}{\term}{\term} \mid  Ralf Jung committed Mar 06, 2016 119  \dynA{\term}{\pred}{\term}  Ralf Jung committed Jan 31, 2016 120 \end{align*}  Ralf Jung committed Jan 31, 2016 121 Recursive predicates must be \emph{guarded}: in \MU \var. \pred, the variable \var can only appear under the later \later modality.  Ralf Jung committed Jan 31, 2016 122   Ralf Jung committed Mar 06, 2016 123 124 Note that \always and \later bind more tightly than *, \wand, \land, \lor, and \Ra.  Ralf Jung committed Jan 31, 2016 125 \paragraph{Metavariable conventions.}  Ralf Jung committed Mar 06, 2016 126 We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:  Ralf Jung committed Jan 31, 2016 127 128 \[ \begin{array}{r|l}  Ralf Jung committed Mar 06, 2016 129  \text{metavariable} & \text{type} \\\hline  Ralf Jung committed Jan 31, 2016 130 131 132 133 134 135 136  \term, \termB & \text{arbitrary} \\ \val, \valB & \textsort{Val} \\ \expr & \textsort{Exp} \\ \state & \textsort{State} \\ \end{array} \qquad\qquad \begin{array}{r|l}  Ralf Jung committed Mar 06, 2016 137  \text{metavariable} & \text{type} \\\hline  Ralf Jung committed Jan 31, 2016 138 139  \iname & \textsort{InvName} \\ \mask & \textsort{InvMask} \\  Ralf Jung committed Mar 06, 2016 140  \melt, \meltB & \textsort{M} \\  Ralf Jung committed Jan 31, 2016 141  \prop, \propB, \propC & \Prop \\  Ralf Jung committed Mar 06, 2016 142  \pred, \predB, \predC & \type\to\Prop \text{ (when \type is clear from context)} \\  Ralf Jung committed Jan 31, 2016 143 144 145 146 \end{array} \paragraph{Variable conventions.}  Ralf Jung committed Feb 02, 2016 147 We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.  Ralf Jung committed Jan 31, 2016 148 We omit type annotations in binders, when the type is clear from context.  Ralf Jung committed Mar 06, 2016 149 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.  Ralf Jung committed Jan 31, 2016 150 151 152 153 154  \subsection{Types}\label{sec:types} Iris terms are simply-typed.  Ralf Jung committed Mar 06, 2016 155 The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$.  Ralf Jung committed Jan 31, 2016 156   Ralf Jung committed Mar 06, 2016 157 158 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$.  Ralf Jung committed Jan 31, 2016 159   Ralf Jung committed Mar 06, 2016 160 \judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}  Ralf Jung committed Jan 31, 2016 161 162 \begin{mathparpagebreakable} %%% variables and function symbols  Ralf Jung committed Mar 06, 2016 163  \axiom{x : \type \proves \wtt{x}{\type}}  Ralf Jung committed Jan 31, 2016 164 \and  Ralf Jung committed Mar 06, 2016 165 166  \infer{\vctx \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term}{\type}}  Ralf Jung committed Jan 31, 2016 167 \and  Ralf Jung committed Mar 06, 2016 168 169  \infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}  Ralf Jung committed Jan 31, 2016 170 \and  Ralf Jung committed Mar 06, 2016 171 172  \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}}  Ralf Jung committed Jan 31, 2016 173 174 175 176 177 178 179 180 181 182 183 \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  Ralf Jung committed Feb 02, 2016 184  \axiom{\vctx \proves \wtt{\unitval}{\unitsort}}  Ralf Jung committed Jan 31, 2016 185 \and  Ralf Jung committed Mar 06, 2016 186 187  \infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}} {\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}  Ralf Jung committed Jan 31, 2016 188 \and  Ralf Jung committed Mar 06, 2016 189 190  \infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}} {\vctx \proves \wtt{\pi_i\,\term}{\type_i}}  Ralf Jung committed Jan 31, 2016 191 192 %%% functions \and  Ralf Jung committed Mar 06, 2016 193 194  \infer{\vctx, x:\type \proves \wtt{\term}{\type'}} {\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}  Ralf Jung committed Jan 31, 2016 195 196 \and \infer  Ralf Jung committed Mar 06, 2016 197 198  {\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}} {\vctx \proves \wtt{\term(\termB)}{\type'}}  Ralf Jung committed Jan 31, 2016 199 200 %%% monoids \and  Ralf Jung committed Mar 06, 2016 201  \infer{\vctx \proves \wtt{\term}{\textsort{M}}}{\vctx \proves \wtt{\munit(\term)}{\textsort{M}}}  Ralf Jung committed Jan 31, 2016 202 \and  Ralf Jung committed Mar 06, 2016 203 204  \infer{\vctx \proves \wtt{\melt}{\textsort{M}} \and \vctx \proves \wtt{\meltB}{\textsort{M}}} {\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{M}}}  Ralf Jung committed Jan 31, 2016 205 206 207 208 209 210 %%% props and predicates \\ \axiom{\vctx \proves \wtt{\FALSE}{\Prop}} \and \axiom{\vctx \proves \wtt{\TRUE}{\Prop}} \and  Ralf Jung committed Mar 06, 2016 211 212  \infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}} {\vctx \proves \wtt{\term =_\type \termB}{\Prop}}  Ralf Jung committed Jan 31, 2016 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 \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{  Ralf Jung committed Mar 06, 2016 230 231  \vctx, \var:\type \proves \wtt{\term}{\type} \and \text{$\var$ is guarded in $\term$}  Ralf Jung committed Jan 31, 2016 232  }{  Ralf Jung committed Mar 06, 2016 233  \vctx \proves \wtt{\MU \var:\type. \term}{\type}  Ralf Jung committed Jan 31, 2016 234 235  } \and  Ralf Jung committed Mar 06, 2016 236 237  \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}  Ralf Jung committed Jan 31, 2016 238 \and  Ralf Jung committed Mar 06, 2016 239 240  \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}  Ralf Jung committed Jan 31, 2016 241 242 243 244 245 246 247 248 \and \infer{ \vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\iname}{\textsort{InvName}} }{ \vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop} } \and  Ralf Jung committed Mar 06, 2016 249  \infer{\vctx \proves \wtt{\melt}{\textsort{M}}}  Ralf Jung committed Jan 31, 2016 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277  {\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}} \and \infer{\vctx \proves \wtt{\state}{\textsort{State}}} {\vctx \proves \wtt{\ownPhys{\state}}{\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} \and \vctx \proves \wtt{\mask}{\textsort{InvMask}} \and \vctx \proves \wtt{\mask'}{\textsort{InvMask}} }{ \vctx \proves \wtt{\pvsA{\prop}{\mask}{\mask'}}{\Prop} } \and \infer{ \vctx \proves \wtt{\expr}{\textsort{Exp}} \and \vctx \proves \wtt{\pred}{\textsort{Val} \to \Prop} \and \vctx \proves \wtt{\mask}{\textsort{InvMask}} }{ \vctx \proves \wtt{\dynA{\expr}{\pred}{\mask}}{\Prop} } \end{mathparpagebreakable}  Ralf Jung committed Mar 06, 2016 278 \subsection{Timeless propositions}  Ralf Jung committed Mar 06, 2016 279 280 281  Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them. This is a \emph{meta-level} assertions about propositions, defined by the following judgment.  Ralf Jung committed Jan 31, 2016 282   Ralf Jung committed Mar 06, 2016 283 \judgment{Timeless Propositions}{\timeless{P}}  Ralf Jung committed Jan 31, 2016 284   Ralf Jung committed Mar 06, 2016 285 286 \ralf{Define a judgment that defines them.}  Ralf Jung committed Mar 06, 2016 287 \subsection{Proof rules}  Ralf Jung committed Mar 06, 2016 288   Ralf Jung committed Jan 31, 2016 289 290 291 292 293 The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold. We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules. Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions. (Bi-implications are analogous.)  Ralf Jung committed Mar 06, 2016 294 \judgment{}{\vctx \mid \pfctx \proves \prop}  Ralf Jung committed Mar 06, 2016 295 \paragraph{Laws of intuitionistic higher-order logic.}  Ralf Jung committed Jan 31, 2016 296 This is entirely standard.  Ralf Jung committed Mar 06, 2016 297 298 \begin{mathparpagebreakable} \infer[Asm]  Ralf Jung committed Jan 31, 2016 299 300 301  {\prop \in \pfctx} {\pfctx \proves \prop} \and  Ralf Jung committed Mar 06, 2016 302 303 \infer[Eq] {\pfctx \proves \prop(\term) \\ \pfctx \proves \term =_\type \term'}  Ralf Jung committed Jan 31, 2016 304 305  {\pfctx \proves \prop(\term')} \and  Ralf Jung committed Mar 06, 2016 306 307 308 309 310 311 312 313 314 315 316 317 \infer[Refl] {} {\pfctx \proves \term =_\type \term} \and \infer[$\bot$E] {\pfctx \proves \FALSE} {\pfctx \proves \prop} \and \infer[$\top$I] {} {\pfctx \proves \TRUE} \and  Ralf Jung committed Jan 31, 2016 318 \infer[$\wedge$I]  Ralf Jung committed Jan 31, 2016 319 320 321  {\pfctx \proves \prop \\ \pfctx \proves \propB} {\pfctx \proves \prop \wedge \propB} \and  Ralf Jung committed Jan 31, 2016 322 \infer[$\wedge$EL]  Ralf Jung committed Jan 31, 2016 323 324 325  {\pfctx \proves \prop \wedge \propB} {\pfctx \proves \prop} \and  Ralf Jung committed Jan 31, 2016 326 \infer[$\wedge$ER]  Ralf Jung committed Jan 31, 2016 327 328 329  {\pfctx \proves \prop \wedge \propB} {\pfctx \proves \propB} \and  Ralf Jung committed Jan 31, 2016 330 \infer[$\vee$IL]  Ralf Jung committed Jan 31, 2016 331 332 333  {\pfctx \proves \prop } {\pfctx \proves \prop \vee \propB} \and  Ralf Jung committed Jan 31, 2016 334 \infer[$\vee$IR]  Ralf Jung committed Jan 31, 2016 335 336 337  {\pfctx \proves \propB} {\pfctx \proves \prop \vee \propB} \and  Ralf Jung committed Mar 06, 2016 338 339 340 341 342 343 \infer[$\vee$E] {\pfctx \proves \prop \vee \propB \\ \pfctx, \prop \proves \propC \\ \pfctx, \propB \proves \propC} {\pfctx \proves \propC} \and  Ralf Jung committed Jan 31, 2016 344 \infer[$\Ra$I]  Ralf Jung committed Jan 31, 2016 345 346 347  {\pfctx, \prop \proves \propB} {\pfctx \proves \prop \Ra \propB} \and  Ralf Jung committed Jan 31, 2016 348 \infer[$\Ra$E]  Ralf Jung committed Jan 31, 2016 349 350 351  {\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop} {\pfctx \proves \propB} \and  Ralf Jung committed Mar 06, 2016 352 353 354 \infer[$\forall$I] { \vctx,\var : \type\mid\pfctx \proves \prop} {\vctx\mid\pfctx \proves \forall \var: \type.\; \prop}  Ralf Jung committed Jan 31, 2016 355 \and  Ralf Jung committed Mar 06, 2016 356 357 358 359 \infer[$\forall$E] {\vctx\mid\pfctx \proves \forall \var :\type.\; \prop \\ \vctx \proves \wtt\term\type} {\vctx\mid\pfctx \proves \prop[\term/\var]}  Ralf Jung committed Jan 31, 2016 360 \and  Ralf Jung committed Mar 06, 2016 361 362 363 364 \infer[$\exists$I] {\vctx\mid\pfctx \proves \prop[\term/\var] \\ \vctx \proves \wtt\term\type} {\vctx\mid\pfctx \proves \exists \var: \type. \prop}  Ralf Jung committed Jan 31, 2016 365 \and  Ralf Jung committed Mar 06, 2016 366 367 368 369 \infer[$\exists$E] {\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\ \vctx,\var : \type\mid\pfctx , \prop \proves \propB} {\vctx\mid\pfctx \proves \propB}  Ralf Jung committed Jan 31, 2016 370 \and  Ralf Jung committed Mar 06, 2016 371 372 373 \infer[$\lambda$] {} {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}  Ralf Jung committed Jan 31, 2016 374 \and  Ralf Jung committed Mar 06, 2016 375 376 377 378 \infer[$\mu$] {} {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]} \end{mathparpagebreakable}  Ralf Jung committed Jan 31, 2016 379   Ralf Jung committed Mar 06, 2016 380 \paragraph{Laws of (affine) bunched implications.}  Ralf Jung committed Jan 31, 2016 381 382 \begin{mathpar} \begin{array}{rMcMl}  Ralf Jung committed Mar 06, 2016 383  \TRUE * \prop &\Lra& \prop \\  Ralf Jung committed Jan 31, 2016 384  \prop * \propB &\Lra& \propB * \prop \\  Ralf Jung committed Mar 06, 2016 385  (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC)  Ralf Jung committed Jan 31, 2016 386 387 \end{array} \and  Ralf Jung committed Mar 06, 2016 388 \infer[$*$-mono]  Ralf Jung committed Mar 06, 2016 389 390 391  {\prop_1 \proves \propB_1 \and \prop_2 \proves \propB_2} {\prop_1 * \prop_2 \proves \propB_1 * \propB_2}  Ralf Jung committed Jan 31, 2016 392 \and  Ralf Jung committed Mar 06, 2016 393 \inferB[$\wand$I-E]  Ralf Jung committed Mar 06, 2016 394 395  {\prop * \propB \proves \propC} {\prop \proves \propB \wand \propC}  Ralf Jung committed Jan 31, 2016 396 397 \end{mathpar}  Ralf Jung committed Mar 06, 2016 398 \paragraph{Laws for ghosts and physical resources.}  Ralf Jung committed Jan 31, 2016 399 400 401 \begin{mathpar} \begin{array}{rMcMl} \ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra& \ownGGhost{\melt \mtimes \meltB} \\  Ralf Jung committed Mar 06, 2016 402 403 %\TRUE &\Ra& \ownGGhost{\munit}\\ \ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}  Ralf Jung committed Jan 31, 2016 404 405 406 \end{array} \and \begin{array}{c}  Ralf Jung committed Mar 06, 2016 407 \ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE  Ralf Jung committed Jan 31, 2016 408 409 410 \end{array} \end{mathpar}  Ralf Jung committed Mar 06, 2016 411 \paragraph{Laws for the later modality.}  Ralf Jung committed Jan 31, 2016 412 \begin{mathpar}  Ralf Jung committed Mar 06, 2016 413 \infer[$\later$-mono]  Ralf Jung committed Jan 31, 2016 414 415 416  {\pfctx \proves \prop} {\pfctx \proves \later{\prop}} \and  Ralf Jung committed Mar 06, 2016 417 418 419 \infer[L{\"o}b] {} {(\later\prop\Ra\prop) \proves \prop}  Ralf Jung committed Jan 31, 2016 420 \and  Ralf Jung committed Mar 06, 2016 421 422 423 424 425 \infer[$\later$-$\exists$] {\text{$\type$ is inhabited}} {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop} \\\\ \begin{array}[c]{rMcMl}  Ralf Jung committed Jan 31, 2016 426 427 428 429  \later{(\prop \wedge \propB)} &\Lra& \later{\prop} \wedge \later{\propB} \\ \later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\ \end{array} \and  Ralf Jung committed Mar 06, 2016 430 \begin{array}[c]{rMcMl}  Ralf Jung committed Jan 31, 2016 431  \later{\All x.\prop} &\Lra& \All x. \later\prop \\  Ralf Jung committed Mar 06, 2016 432  \Exists x. \later\prop &\Ra& \later{\Exists x.\prop} \\  Ralf Jung committed Jan 31, 2016 433 434 435 436  \later{(\prop * \propB)} &\Lra& \later\prop * \later\propB \end{array} \end{mathpar}  Ralf Jung committed Mar 06, 2016 437 \paragraph{Laws for the always modality.}  Ralf Jung committed Jan 31, 2016 438 \begin{mathpar}  Ralf Jung committed Mar 06, 2016 439 \infer[$\always$I]  Ralf Jung committed Jan 31, 2016 440 441 442  {\always{\pfctx} \proves \prop} {\always{\pfctx} \proves \always{\prop}} \and  Ralf Jung committed Mar 06, 2016 443 444 445 446 447 448 449 \infer[$\always$E]{} {\always{\prop} \Ra \prop} \and \begin{array}[c]{rMcMl} \always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\ \always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\ \always{\later\prop} &\Lra& \later\always{\prop} \\  Ralf Jung committed Jan 31, 2016 450 451 \end{array} \and  Ralf Jung committed Mar 06, 2016 452 \begin{array}[c]{rMcMl}  Ralf Jung committed Jan 31, 2016 453 454 455 456 457 458 459  \always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\ \always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\ \always{\All x. \prop} &\Lra& \All x. \always{\prop} \\ \always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\ \end{array} \end{mathpar}  Ralf Jung committed Mar 06, 2016 460 \paragraph{Laws of primitive view shifts.}  Ralf Jung committed Mar 06, 2016 461 ~\\\ralf{Add these.}  Ralf Jung committed Jan 31, 2016 462   Ralf Jung committed Mar 06, 2016 463 \paragraph{Laws of weakest preconditions.}  Ralf Jung committed Mar 06, 2016 464 ~\\\ralf{Add these.}  Ralf Jung committed Jan 31, 2016 465 466 467 468 469  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: