base-logic.tex 13.3 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
63
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
64
    \ownM{\term} \mid \mval(\term) \mid
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's avatar
Ralf Jung committed
171
		{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
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}

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

198
\judgment{\vctx \mid \prop \proves \propB}
199
200
201
202
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
203
204
205
  {}
  {\prop \proves \prop}
\and
206
\infer[Cut]
207
208
  {\prop \proves \propB \and \propB \proves \propC}
  {\prop \proves \propC}
209
210
\and
\infer[Eq]
211
212
  {\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]}
213
214
215
\and
\infer[Refl]
  {}
216
  {\TRUE \proves \term =_\type \term}
217
218
\and
\infer[$\bot$E]
219
220
  {}
  {\FALSE \proves \prop}
221
222
223
\and
\infer[$\top$I]
  {}
224
  {\prop \proves \TRUE}
225
226
\and
\infer[$\wedge$I]
227
228
  {\prop \proves \propB \\ \prop \proves \propC}
  {\prop \proves \propB \land \propC}
229
230
\and
\infer[$\wedge$EL]
231
232
  {\prop \proves \propB \land \propC}
  {\prop \proves \propB}
233
234
\and
\infer[$\wedge$ER]
235
236
  {\prop \proves \propB \land \propC}
  {\prop \proves \propC}
237
238
\and
\infer[$\vee$IL]
239
240
  {\prop \proves \propB }
  {\prop \proves \propB \lor \propC}
241
242
\and
\infer[$\vee$IR]
243
244
  {\prop \proves \propC}
  {\prop \proves \propB \lor \propC}
245
246
\and
\infer[$\vee$E]
247
248
249
  {\prop \proves \propC \\
   \propB \proves \propC}
  {\prop \lor \propB \proves \propC}
250
251
\and
\infer[$\Ra$I]
252
253
  {\prop \land \propB \proves \propC}
  {\prop \proves \propB \Ra \propC}
254
255
\and
\infer[$\Ra$E]
256
257
  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB}
  {\prop \proves \propC}
258
259
\and
\infer[$\forall$I]
260
261
  { \vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\prop \proves \All \var: \type. \propB}
262
263
\and
\infer[$\forall$E]
264
  {\vctx\mid\prop \proves \All \var :\type. \propB \\
265
   \vctx \proves \wtt\term\type}
266
  {\vctx\mid\prop \proves \propB[\term/\var]}
267
\\
268
\infer[$\exists$I]
269
  {\vctx\mid\prop \proves \propB[\term/\var] \\
270
   \vctx \proves \wtt\term\type}
271
  {\vctx\mid\prop \proves \exists \var: \type. \propB}
272
273
\and
\infer[$\exists$E]
274
275
  {\vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\Exists \var: \type. \prop \proves \propB}
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
% \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 \\
292
293
  \prop * \propB &\proves& \propB * \prop \\
  (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)
294
295
296
297
298
299
300
301
302
303
304
305
\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}

306
\paragraph{Laws for the always modality.}
307
\begin{mathpar}
308
309
310
\infer[$\always$-mono]
  {\prop \proves \propB}
  {\always{\prop} \proves \always{\propB}}
311
\and
312
313
314
\infer[$\always$-E]{}
{\always\prop \proves \prop}
\and
315
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
316
  \TRUE &\proves& \always{\TRUE} \\
317
318
319
  \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
  \always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
320
\and
321
322
323
324
\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}
325
326
327
\end{array}
\end{mathpar}

328

329
330
331
\paragraph{Laws for the later modality.}
\begin{mathpar}
\infer[$\later$-mono]
332
333
  {\prop \proves \propB}
  {\later\prop \proves \later{\propB}}
334
335
336
337
338
339
\and
\infer[L{\"o}b]
  {}
  {(\later\prop\Ra\prop) \proves \prop}
\and
\begin{array}[c]{rMcMl}
340
341
  \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
342
  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)
343
344
345
\end{array}
\and
\begin{array}[c]{rMcMl}
346
  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
Ralf Jung's avatar
Ralf Jung committed
347
  \always{\later\prop} &\provesIff& \later\always{\prop}
348
349
350
\end{array}
\end{mathpar}

351

Ralf Jung's avatar
Ralf Jung committed
352
\paragraph{Laws for resources and validity.}
353
\begin{mathpar}
354
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
355
356
357
358
\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)
359
\end{array}
Ralf Jung's avatar
Ralf Jung committed
360
361
362
363
364
365
366
367
% \and
% \infer[valid-intro]
% {\melt \in \mval}
% {\TRUE \vdash \mval(\melt)}
% \and
% \infer[valid-elim]
% {\melt \notin \mval_0}
% {\mval(\melt) \proves \FALSE}
368
\and
369
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
370
\ownM{\melt} &\proves& \mval(\melt) \\
371
372
373
\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
\mval(\melt) &\proves& \always\mval(\melt)
\end{array}
374
375
\end{mathpar}

376

Ralf Jung's avatar
Ralf Jung committed
377
\paragraph{Laws for the basic update modality.}
378
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
379
\inferH{upd-mono}
380
381
382
{\prop \proves \propB}
{\upd\prop \proves \upd\propB}

Ralf Jung's avatar
Ralf Jung committed
383
\inferH{upd-intro}
384
385
{}{\prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
386
\inferH{upd-trans}
387
388
389
{}
{\upd \upd \prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
390
\inferH{upd-frame}
391
392
393
394
{}{\propB * \upd\prop \proves \upd (\propB * \prop)}

\inferH{upd-update}
{\melt \mupd \meltsB}
Ralf Jung's avatar
Ralf Jung committed
395
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
396
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
397
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
398
%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
399

Ralf Jung's avatar
Ralf Jung committed
400
\subsection{Consistency}
401

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

Ralf Jung's avatar
Ralf Jung committed
408
409
410
411
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.

412
413
414
415
416

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