base-logic.tex 14.2 KB
Newer Older
1
2
3
\section{Base Logic}
\label{sec:base-logic}

4
The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.
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.
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.}
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$).
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
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's avatar
Ralf Jung committed
63
%\\&
Ralf Jung's avatar
Ralf Jung committed
64
    \ownM{\term} \mid \mval(\term) \mid
65
    \always\prop \mid
Ralf Jung's avatar
Ralf Jung committed
66
    \plainly\prop \mid
67
    {\later\prop} \mid
Ralf Jung's avatar
Ralf Jung committed
68
    \upd \prop
69
70
71
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.

Ralf Jung's avatar
Ralf Jung committed
72
Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
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
171


\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's avatar
Ralf Jung committed
172
		{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
173
174
175
176
177
178
\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}}
Ralf Jung's avatar
Ralf Jung committed
179
180
181
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\plainly\prop}{\Prop}}
182
183
184
185
186
187
188
189
190
191
192
193
194
195
\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}

196
197
198
199
200
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.
201

202
\judgment{\vctx \mid \prop \proves \propB}
203
204
205
206
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
207
208
209
  {}
  {\prop \proves \prop}
\and
210
\infer[Cut]
211
212
  {\prop \proves \propB \and \propB \proves \propC}
  {\prop \proves \propC}
213
214
\and
\infer[Eq]
215
216
  {\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]}
217
218
219
\and
\infer[Refl]
  {}
220
  {\TRUE \proves \term =_\type \term}
221
222
\and
\infer[$\bot$E]
223
224
  {}
  {\FALSE \proves \prop}
225
226
227
\and
\infer[$\top$I]
  {}
228
  {\prop \proves \TRUE}
229
230
\and
\infer[$\wedge$I]
231
232
  {\prop \proves \propB \\ \prop \proves \propC}
  {\prop \proves \propB \land \propC}
233
234
\and
\infer[$\wedge$EL]
235
236
  {\prop \proves \propB \land \propC}
  {\prop \proves \propB}
237
238
\and
\infer[$\wedge$ER]
239
240
  {\prop \proves \propB \land \propC}
  {\prop \proves \propC}
241
242
\and
\infer[$\vee$IL]
243
244
  {\prop \proves \propB }
  {\prop \proves \propB \lor \propC}
245
246
\and
\infer[$\vee$IR]
247
248
  {\prop \proves \propC}
  {\prop \proves \propB \lor \propC}
249
250
\and
\infer[$\vee$E]
251
252
253
  {\prop \proves \propC \\
   \propB \proves \propC}
  {\prop \lor \propB \proves \propC}
254
255
\and
\infer[$\Ra$I]
256
257
  {\prop \land \propB \proves \propC}
  {\prop \proves \propB \Ra \propC}
258
259
\and
\infer[$\Ra$E]
260
261
  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB}
  {\prop \proves \propC}
262
263
\and
\infer[$\forall$I]
264
265
  { \vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\prop \proves \All \var: \type. \propB}
266
267
\and
\infer[$\forall$E]
268
  {\vctx\mid\prop \proves \All \var :\type. \propB \\
269
   \vctx \proves \wtt\term\type}
270
  {\vctx\mid\prop \proves \propB[\term/\var]}
271
\\
272
\infer[$\exists$I]
273
  {\vctx\mid\prop \proves \propB[\term/\var] \\
274
   \vctx \proves \wtt\term\type}
275
  {\vctx\mid\prop \proves \exists \var: \type. \propB}
276
277
\and
\infer[$\exists$E]
278
279
  {\vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\Exists \var: \type. \prop \proves \propB}
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
% \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 \\
296
297
  \prop * \propB &\proves& \propB * \prop \\
  (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)
298
299
300
301
302
303
304
305
306
307
308
309
\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's avatar
Ralf Jung committed
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
\paragraph{Laws for the plainness modality.}
\begin{mathpar}
\infer[$\plainly$-mono]
  {\prop \proves \propB}
  {\plainly{\prop} \proves \plainly{\propB}}
\and
\infer[$\plainly$-E]{}
{\plainly\prop \proves \always\prop}
\and
\begin{array}[c]{rMcMl}
  \TRUE &\proves& \plainly{\TRUE} \\
  (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q)
\end{array}
\and
\begin{array}[c]{rMcMl}
  \plainly{\prop} &\proves& \plainly\plainly\prop \\
  \All x. \plainly{\prop} &\proves& \plainly{\All x. \prop} \\
  \plainly{\Exists x. \prop} &\proves& \Exists x. \plainly{\prop}
\end{array}
\and
\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
\end{mathpar}

\paragraph{Laws for the persistence modality.}
334
\begin{mathpar}
335
336
337
\infer[$\always$-mono]
  {\prop \proves \propB}
  {\always{\prop} \proves \always{\propB}}
338
\and
339
340
341
\infer[$\always$-E]{}
{\always\prop \proves \prop}
\and
342
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
343
344
  \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
345
\end{array}
346
\and
347
348
349
350
\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}
351
352
353
\end{array}
\end{mathpar}

354

355
356
357
\paragraph{Laws for the later modality.}
\begin{mathpar}
\infer[$\later$-mono]
358
359
  {\prop \proves \propB}
  {\later\prop \proves \later{\propB}}
360
361
362
363
364
365
\and
\infer[L{\"o}b]
  {}
  {(\later\prop\Ra\prop) \proves \prop}
\and
\begin{array}[c]{rMcMl}
366
367
  \All x. \later\prop &\proves& \later{\All x.\prop} \\
  \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop}  \\
Ralf Jung's avatar
Ralf Jung committed
368
  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)
369
370
371
\end{array}
\and
\begin{array}[c]{rMcMl}
372
  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
Ralf Jung's avatar
Ralf Jung committed
373
374
  \always{\later\prop} &\provesIff& \later\always{\prop} \\
  \plainly{\later\prop} &\provesIff& \later\plainly{\prop}
375
376
377
\end{array}
\end{mathpar}

378

Ralf Jung's avatar
Ralf Jung committed
379
\paragraph{Laws for resources and validity.}
380
\begin{mathpar}
381
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
382
383
384
385
\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)
386
\end{array}
Ralf Jung's avatar
Ralf Jung committed
387
388
389
390
391
392
393
394
% \and
% \infer[valid-intro]
% {\melt \in \mval}
% {\TRUE \vdash \mval(\melt)}
% \and
% \infer[valid-elim]
% {\melt \notin \mval_0}
% {\mval(\melt) \proves \FALSE}
395
\and
396
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
397
\ownM{\melt} &\proves& \mval(\melt) \\
398
399
400
\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
\mval(\melt) &\proves& \always\mval(\melt)
\end{array}
401
402
\end{mathpar}

403

Ralf Jung's avatar
Ralf Jung committed
404
\paragraph{Laws for the basic update modality.}
405
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
406
\inferH{upd-mono}
407
408
409
{\prop \proves \propB}
{\upd\prop \proves \upd\propB}

Ralf Jung's avatar
Ralf Jung committed
410
\inferH{upd-intro}
411
412
{}{\prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
413
\inferH{upd-trans}
414
415
416
{}
{\upd \upd \prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
417
\inferH{upd-frame}
418
419
420
421
{}{\propB * \upd\prop \proves \upd (\propB * \prop)}

\inferH{upd-update}
{\melt \mupd \meltsB}
Ralf Jung's avatar
Ralf Jung committed
422
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
Ralf Jung's avatar
Ralf Jung committed
423
424
425
426

\inferH{upd-plainly}
{}
{\upd\plainly\prop \proves \prop}
427
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
428
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
Ralf Jung's avatar
Ralf Jung committed
429
%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
430

Ralf Jung's avatar
Ralf Jung committed
431
\subsection{Consistency}
432

Ralf Jung's avatar
Ralf Jung committed
433
The consistency statement of the logic reads as follows: For any $n$, we have
434
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
435
  \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)
436
437
\end{align*}
where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
438

Ralf Jung's avatar
Ralf Jung committed
439
440
441
442
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.

443
444
445
446
447

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