logic.tex 16.5 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
\section{Language}
2

Ralf Jung's avatar
Ralf Jung committed
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
4
\begin{itemize}
Ralf Jung's avatar
Ralf Jung committed
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.
25 26
\end{itemize}

Ralf Jung's avatar
Ralf Jung committed
27 28 29
\subsection{The concurrent language}

For any language $\Lang$, we define the corresponding thread-pool semantics.
30 31 32

\paragraph{Machine syntax}
\[
Ralf Jung's avatar
Ralf Jung committed
33
	\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
34 35
\]

Ralf Jung's avatar
Ralf Jung committed
36 37
\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
  \cfg{\tpool'}{\state'}}
38 39
\begin{mathpar}
\infer
Ralf Jung's avatar
Ralf Jung committed
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'}}
47 48 49
\end{mathpar}


Ralf Jung's avatar
Ralf Jung committed
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}
57

Ralf Jung's avatar
Ralf Jung committed
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:
61
\[
Ralf Jung's avatar
Ralf Jung committed
62
	\SigType \supseteq \{ \textsort{Val}, \textsort{Expr}, \textsort{State}, \textsort{M}, \textsort{InvName}, \textsort{InvMask}, \Prop \}
63
\]
Ralf Jung's avatar
Ralf Jung committed
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$).
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's avatar
Ralf Jung committed
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}
78 79

\paragraph{Syntax.}
Ralf Jung's avatar
Ralf Jung committed
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$):
81

82
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
83 84 85 86 87 88
  \type ::={}&
      \sigtype \mid
      \unitsort \mid
      \type \times \type \mid
      \type \to \type
\\[0.4em]
89 90 91
  \term, \prop, \pred ::={}&
      x \mid
      \sigfn(\term_1, \dots, \term_n) \mid
92
      \unitval \mid
93 94 95
      (\term, \term) \mid
      \pi_i\; \term \mid
      \Lam x.\term \mid
Ralf Jung's avatar
Ralf Jung committed
96
      \term(\term)  \mid
97 98 99 100 101 102
      \mzero \mid
      \munit \mid
      \term \mtimes \term \mid
\\&
    \FALSE \mid
    \TRUE \mid
Ralf Jung's avatar
Ralf Jung committed
103
    \term =_\type \term \mid
104 105 106 107 108 109
    \prop \Ra \prop \mid
    \prop \land \prop \mid
    \prop \lor \prop \mid
    \prop * \prop \mid
    \prop \wand \prop \mid
\\&
Ralf Jung's avatar
Ralf Jung committed
110
    \MU \var. \pred  \mid
Ralf Jung's avatar
Ralf Jung committed
111 112
    \Exists \var:\type. \prop \mid
    \All \var:\type. \prop \mid
113 114 115 116 117 118 119
\\&
    \knowInv{\term}{\prop} \mid
    \ownGGhost{\term} \mid
    \ownPhys{\term} \mid
    \always\prop \mid
    {\later\prop} \mid
    \pvsA{\prop}{\term}{\term} \mid
Ralf Jung's avatar
Ralf Jung committed
120
    \dynA{\term}{\pred}{\term}
121
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
122
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
123 124

\paragraph{Metavariable conventions.}
Ralf Jung's avatar
Ralf Jung committed
125
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
126 127
\[
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
128
 \text{metavariable} & \text{type} \\\hline
129 130 131 132 133 134 135
  \term, \termB & \text{arbitrary} \\
  \val, \valB & \textsort{Val} \\
  \expr & \textsort{Exp} \\
  \state & \textsort{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
136
 \text{metavariable} & \text{type} \\\hline
137 138
  \iname & \textsort{InvName} \\
  \mask & \textsort{InvMask} \\
Ralf Jung's avatar
Ralf Jung committed
139
  \melt, \meltB & \textsort{M} \\
140
  \prop, \propB, \propC & \Prop \\
Ralf Jung's avatar
Ralf Jung committed
141
  \pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
142 143 144 145
\end{array}
\]

\paragraph{Variable conventions.}
146
We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
147
We omit type annotations in binders, when the type is clear from context.
Ralf Jung's avatar
Ralf Jung committed
148
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.
149 150 151 152 153


\subsection{Types}\label{sec:types}

Iris terms are simply-typed.
Ralf Jung's avatar
Ralf Jung committed
154
The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$.
155

Ralf Jung's avatar
Ralf Jung committed
156 157
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$.
158

Ralf Jung's avatar
Ralf Jung committed
159
\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
160 161
\begin{mathparpagebreakable}
%%% variables and function symbols
Ralf Jung's avatar
Ralf Jung committed
162
	\axiom{x : \type \proves \wtt{x}{\type}}
163
\and
Ralf Jung's avatar
Ralf Jung committed
164 165
	\infer{\vctx \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term}{\type}}
166
\and
Ralf Jung's avatar
Ralf Jung committed
167 168
	\infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}
169
\and
Ralf Jung's avatar
Ralf Jung committed
170 171
	\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}}
172 173 174 175 176 177 178 179 180 181 182
\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
183
	\axiom{\vctx \proves \wtt{\unitval}{\unitsort}}
184
\and
Ralf Jung's avatar
Ralf Jung committed
185 186
	\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
		{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
187
\and
Ralf Jung's avatar
Ralf Jung committed
188 189
	\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
		{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
190 191
%%% functions
\and
Ralf Jung's avatar
Ralf Jung committed
192 193
	\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
		{\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}
194 195
\and
	\infer
Ralf Jung's avatar
Ralf Jung committed
196 197
	{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
	{\vctx \proves \wtt{\term(\termB)}{\type'}}
198 199
%%% monoids
\and
Ralf Jung's avatar
Ralf Jung committed
200
	\infer{\vctx \proves \wtt{\term}{\textsort{M}}}{\vctx \proves \wtt{\munit(\term)}{\textsort{M}}}
201
\and
Ralf Jung's avatar
Ralf Jung committed
202 203
	\infer{\vctx \proves \wtt{\melt}{\textsort{M}} \and \vctx \proves \wtt{\meltB}{\textsort{M}}}
		{\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{M}}}
204 205 206 207 208 209
%%% props and predicates
\\
	\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
\and
	\axiom{\vctx \proves \wtt{\TRUE}{\Prop}}
\and
Ralf Jung's avatar
Ralf Jung committed
210 211
	\infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}}
		{\vctx \proves \wtt{\term =_\type \termB}{\Prop}}
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
\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's avatar
Ralf Jung committed
229
		\vctx, \var:\type\to\Prop \proves \wtt{\pred}{\type\to\Prop} \and
Ralf Jung's avatar
Ralf Jung committed
230
		\text{$\var$ is guarded in $\pred$}
231
	}{
Ralf Jung's avatar
Ralf Jung committed
232
		\vctx \proves \wtt{\MU \var. \pred}{\type\to\Prop}
233 234
	}
\and
Ralf Jung's avatar
Ralf Jung committed
235 236
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}
237
\and
Ralf Jung's avatar
Ralf Jung committed
238 239
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
240 241 242 243 244 245 246 247
\and
	\infer{
		\vctx \proves \wtt{\prop}{\Prop} \and
		\vctx \proves \wtt{\iname}{\textsort{InvName}}
	}{
		\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
	}
\and
Ralf Jung's avatar
Ralf Jung committed
248
	\infer{\vctx \proves \wtt{\melt}{\textsort{M}}}
249 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
		{\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's avatar
Ralf Jung committed
277
\subsection{Timeless propositions}
Ralf Jung's avatar
Ralf Jung committed
278 279 280

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.
281

Ralf Jung's avatar
Ralf Jung committed
282
\judgment{Timeless Propositions}{\timeless{P}}
283

Ralf Jung's avatar
Ralf Jung committed
284 285
\ralf{Define a judgment that defines them.}

Ralf Jung's avatar
Ralf Jung committed
286
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
287 288

\ralf{Go on checking below.}
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's avatar
Ralf Jung committed
294
\paragraph{Laws of intuitionistic higher-order logic.}
295
This is entirely standard.
296 297 298 299 300 301 302 303 304 305

\begin{mathpar}
\inferH{Asm}
  {\prop \in \pfctx}
  {\pfctx \proves \prop}
\and
\inferH{Eq}
  {\pfctx \proves \prop(\term) \\ \pfctx \proves \term = \term'}
  {\pfctx \proves \prop(\term')}
\and
306
\infer[$\wedge$I]
307 308 309
  {\pfctx \proves \prop \\ \pfctx \proves \propB}
  {\pfctx \proves \prop \wedge \propB}
\and
310
\infer[$\wedge$EL]
311 312 313
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \prop}
\and
314
\infer[$\wedge$ER]
315 316 317
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \propB}
\and
318
\infer[$\vee$E]
319 320 321 322 323
  {\pfctx \proves \prop \vee \propB \\
   \pfctx, \prop \proves \propC \\
   \pfctx, \propB \proves \propC}
  {\pfctx \proves \propC}
\and
324
\infer[$\vee$IL]
325 326 327
  {\pfctx \proves \prop }
  {\pfctx \proves \prop \vee \propB}
\and
328
\infer[$\vee$IR]
329 330 331
  {\pfctx \proves \propB}
  {\pfctx \proves \prop \vee \propB}
\and
332
\infer[$\Ra$I]
333 334 335
  {\pfctx, \prop \proves \propB}
  {\pfctx \proves \prop \Ra \propB}
\and
336
\infer[$\Ra$E]
337 338 339
  {\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
  {\pfctx \proves \propB}
\and
340
\infer[$\forall_1$I]
341 342 343
  {\pfctx, x : \sort \proves \prop}
  {\pfctx \proves \forall x: \sort.\; \prop}
\and
344
\infer[$\forall_1$E]
345 346 347 348
  {\pfctx \proves \forall X \in \sort.\; \prop \\
   \pfctx \proves \term: \sort}
  {\pfctx \proves \prop[\term/X]}
\and
349
\infer[$\exists_1$E]
350 351 352 353
  {\pfctx \proves \exists X\in \sort.\; \prop \\
   \pfctx, X : \sort, \prop \proves \propB}
  {\pfctx \proves \propB}
\and
354
\infer[$\exists_1$I]
355 356 357 358
  {\pfctx \proves \prop[\term/X] \\
   \pfctx \proves \term: \sort}
  {\pfctx \proves \exists X: \sort. \prop}
\and
359
\infer[$\forall_2$I]
Ralf Jung's avatar
Ralf Jung committed
360 361
  {\pfctx, \var: \Pred(\sort) \proves \prop}
  {\pfctx \proves \forall \var\in \Pred(\sort).\; \prop}
362
\and
363
\infer[$\forall_2$E]
Ralf Jung's avatar
Ralf Jung committed
364
  {\pfctx \proves \forall \var. \prop \\
365
   \pfctx \proves \propB: \Prop}
Ralf Jung's avatar
Ralf Jung committed
366
  {\pfctx \proves \prop[\propB/\var]}
367
\and
368
\infer[$\exists_2$E]
Ralf Jung's avatar
Ralf Jung committed
369 370
  {\pfctx \proves \exists \var \in \Pred(\sort).\prop \\
   \pfctx, \var : \Pred(\sort), \prop \proves \propB}
371 372
  {\pfctx \proves \propB}
\and
373
\infer[$\exists_2$I]
Ralf Jung's avatar
Ralf Jung committed
374
  {\pfctx \proves \prop[\propB/\var] \\
375
   \pfctx \proves \propB: \Prop}
Ralf Jung's avatar
Ralf Jung committed
376
  {\pfctx \proves \exists \var. \prop}
377
\and
378
\inferB[Elem]
379 380 381
  {\pfctx \proves \term \in (X \in \sort). \prop}
  {\pfctx \proves \prop[\term/X]}
\and
382
\inferB[Elem-$\mu$]
Ralf Jung's avatar
Ralf Jung committed
383 384
  {\pfctx \proves \term \in (\mu\var \in \Pred(\sort). \pred)}
  {\pfctx \proves \term \in \pred[\mu\var \in \Pred(\sort). \pred/\var]}
385 386
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
387
\paragraph{Laws of (affine) bunched implications.}
388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417
\begin{mathpar}
\begin{array}{rMcMl}
  \prop * \propB &\Lra& \propB * \prop \\
  (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC) \\
  \prop * \propB &\Ra& \prop
\end{array}
\and
\begin{array}{rMcMl}
  (\prop \vee \propB) * \propC &\Lra& 
    (\prop * \propC) \vee (\propB * \propC)  \\
  (\prop \wedge \propB) * \propC &\Ra& 
    (\prop * \propC) \wedge (\propB * \propC)  \\
  (\Exists x. \prop) * \propB &\Lra& \Exists x. (\prop * \propB) \\
  (\All x. \prop) * \propB &\Ra& \All x. (\prop * \propB) 
\end{array}
\and
\infer
  {\pfctx, \prop_1 \proves \propB_1 \and
   \pfctx, \prop_2 \proves \propB_2}
  {\pfctx, \prop_1 * \prop_2 \proves \propB_1 * \propB_2}
\and
\infer
  {\pfctx, \prop * \propB \proves \propC}
  {\pfctx, \prop \proves \propB \wand \propC}
\and
\infer
  {\pfctx, \prop \proves \propB \wand \propC}
  {\pfctx, \prop * \propB \proves \propC}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
418
\paragraph{Laws for ghosts and physical resources.}
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433

\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra&  \ownGGhost{\melt \mtimes \meltB} \\
\TRUE &\Ra&  \ownGGhost{\munit}\\
\ownGGhost{\mzero} &\Ra& \FALSE\\
\multicolumn{3}{c}{\timeless{\ownGGhost{\melt}}}
\end{array}
\and
\begin{array}{c}
\ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE \\
\timeless{\ownPhys{\state}}
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
434
\paragraph{Laws for the later modality.}
435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457

\begin{mathpar}
\inferH{Mono}
  {\pfctx \proves \prop}
  {\pfctx \proves \later{\prop}}
\and
\inferhref{L{\"o}b}{Loeb}
  {\pfctx, \later{\prop} \proves \prop}
  {\pfctx \proves \prop}
\and
\begin{array}[b]{rMcMl}
  \later{\always{\prop}} &\Lra& \always{\later{\prop}} \\
  \later{(\prop \wedge \propB)} &\Lra& \later{\prop} \wedge \later{\propB}  \\
  \later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\
\end{array}
\and
\begin{array}[b]{rMcMl}
  \later{\All x.\prop} &\Lra& \All x. \later\prop \\
  \later{\Exists x.\prop} &\Lra& \Exists x. \later\prop \\
  \later{(\prop * \propB)} &\Lra& \later\prop * \later\propB
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
458
\paragraph{Laws for the always modality.}
459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482

\begin{mathpar}
\axiomH{Necessity}
  {\always{\prop} \Ra \prop}
\and
\inferhref{$\always$I}{AlwaysIntro}
  {\always{\pfctx} \proves \prop}
  {\always{\pfctx} \proves \always{\prop}}
\and
\begin{array}[b]{rMcMl}
  \always(\term =_\sort \termB) &\Lra& \term=_\sort \termB \\
  \always{\prop} * \propB &\Lra& \always{\prop} \land \propB \\
  \always{(\prop \Ra \propB)} &\Ra& \always{\prop} \Ra \always{\propB} \\
\end{array}
\and
\begin{array}[b]{rMcMl}
  \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}
Note that $\always$ binds more tightly than $*$, $\land$, $\lor$, and $\Ra$.

Ralf Jung's avatar
Ralf Jung committed
483
\paragraph{Laws of primitive view shifts.}
484

Ralf Jung's avatar
Ralf Jung committed
485
\paragraph{Laws of weakest preconditions.}
486

487 488 489 490 491

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: