logic.tex 15.7 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
  \term, \prop, \pred ::={}&
90
      \var \mid
91
      \sigfn(\term_1, \dots, \term_n) \mid
92
      \unitval \mid
93 94
      (\term, \term) \mid
      \pi_i\; \term \mid
95
      \Lam \var:\type.\term \mid
Ralf Jung's avatar
Ralf Jung committed
96
      \term(\term)  \mid
97 98 99 100 101
      \munit \mid
      \term \mtimes \term \mid
\\&
    \FALSE \mid
    \TRUE \mid
Ralf Jung's avatar
Ralf Jung committed
102
    \term =_\type \term \mid
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
\\&
109
    \MU \var:\type. \pred  \mid
Ralf Jung's avatar
Ralf Jung committed
110 111
    \Exists \var:\type. \prop \mid
    \All \var:\type. \prop \mid
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's avatar
Ralf Jung committed
119
    \dynA{\term}{\pred}{\term}
120
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
121
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
122 123

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

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


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

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

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

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

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

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

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

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

287 288 289 290 291
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.)

292
\judgment{}{\vctx \mid \pfctx \proves \prop}
Ralf Jung's avatar
Ralf Jung committed
293
\paragraph{Laws of intuitionistic higher-order logic.}
294
This is entirely standard.
295

296 297
\begin{mathparpagebreakable}
\infer[Asm]
298 299 300
  {\prop \in \pfctx}
  {\pfctx \proves \prop}
\and
301 302
\infer[Eq]
  {\pfctx \proves \prop(\term) \\ \pfctx \proves \term =_\type \term'}
303 304
  {\pfctx \proves \prop(\term')}
\and
305 306 307 308 309 310 311 312 313 314 315 316
\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
317
\infer[$\wedge$I]
318 319 320
  {\pfctx \proves \prop \\ \pfctx \proves \propB}
  {\pfctx \proves \prop \wedge \propB}
\and
321
\infer[$\wedge$EL]
322 323 324
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \prop}
\and
325
\infer[$\wedge$ER]
326 327 328
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \propB}
\and
329
\infer[$\vee$IL]
330 331 332
  {\pfctx \proves \prop }
  {\pfctx \proves \prop \vee \propB}
\and
333
\infer[$\vee$IR]
334 335 336
  {\pfctx \proves \propB}
  {\pfctx \proves \prop \vee \propB}
\and
337 338 339 340 341 342
\infer[$\vee$E]
  {\pfctx \proves \prop \vee \propB \\
   \pfctx, \prop \proves \propC \\
   \pfctx, \propB \proves \propC}
  {\pfctx \proves \propC}
\and
343
\infer[$\Ra$I]
344 345 346
  {\pfctx, \prop \proves \propB}
  {\pfctx \proves \prop \Ra \propB}
\and
347
\infer[$\Ra$E]
348 349 350
  {\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
  {\pfctx \proves \propB}
\and
351 352 353
\infer[$\forall$I]
  { \vctx,\var : \type\mid\pfctx \proves \prop}
  {\vctx\mid\pfctx \proves \forall \var: \type.\; \prop}
354
\and
355 356 357 358
\infer[$\forall$E]
  {\vctx\mid\pfctx \proves \forall \var :\type.\; \prop \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \prop[\term/\var]}
359
\and
360 361 362 363
\infer[$\exists$I]
  {\vctx\mid\pfctx \proves \prop[\term/\var] \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \exists \var: \type. \prop}
364
\and
365 366 367 368
\infer[$\exists$E]
  {\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
   \vctx,\var : \type\mid\pfctx , \prop \proves \propB}
  {\vctx\mid\pfctx \proves \propB}
369
\and
370 371 372
\infer[$\lambda$]
  {}
  {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
373
\and
374 375 376 377
\infer[$\mu$]
  {}
  {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
378

Ralf Jung's avatar
Ralf Jung committed
379
\paragraph{Laws of (affine) bunched implications.}
380 381
\begin{mathpar}
\begin{array}{rMcMl}
382
  \TRUE * \prop &\Lra& \prop \\
383
  \prop * \propB &\Lra& \propB * \prop \\
384
  (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC)
385 386 387
\end{array}
\and
\infer
388 389 390
  {\prop_1 \proves \propB_1 \and
   \prop_2 \proves \propB_2}
  {\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
391
\and
392 393 394
\inferB
  {\prop * \propB \proves \propC}
  {\prop \proves \propB \wand \propC}
395 396
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
397
\paragraph{Laws for ghosts and physical resources.}
398 399 400 401

\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra&  \ownGGhost{\melt \mtimes \meltB} \\
402 403
%\TRUE &\Ra&  \ownGGhost{\munit}\\
\ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}
404 405 406
\end{array}
\and
\begin{array}{c}
407
\ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE
408 409 410
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
411
\paragraph{Laws for the later modality.}
412 413
~\\\ralf{Go on checking below.}

414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436

\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
437
\paragraph{Laws for the always modality.}
438 439 440 441 442 443 444 445 446 447

\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}
448
  \always(\term =_\type \termB) &\Lra& \term=_\type \termB \\
449 450 451 452 453 454 455 456 457 458 459 460 461
  \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
462
\paragraph{Laws of primitive view shifts.}
463

Ralf Jung's avatar
Ralf Jung committed
464
\paragraph{Laws of weakest preconditions.}
465

466 467 468 469 470

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