\section{Base Logic} \label{sec:base-logic} The base logic is parameterized by an arbitrary camera $\monoid$ having a unit $\munit$. By \lemref{lem:camera-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following. 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.} Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$). Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \begin{align*} \type \bnfdef{}& \sigtype \mid 0 \mid 1 \mid \type + \type \mid \type \times \type \mid \type \to \type \\[0.4em] \term, \prop, \pred \bnfdef{}& \var \mid \sigfn(\term_1, \dots, \term_n) \mid \textlog{abort}\; \term \mid () \mid (\term, \term) \mid \pi_i\; \term \mid \Lam \var:\type.\term \mid \term(\term) \mid \\& \textlog{inj}_i\; \term \mid \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term \mid \Ret\textlog{inj}_2\; \var. \term \;\textlog{end} \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 %\\& \ownM{\term} \mid \mval(\term) \mid \always\prop \mid \plainly\prop \mid {\later\prop} \mid \upd \prop \end{align*} Well-typedness forces recursive definitions to be \emph{guarded}: In $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. Furthermore, the type of the definition must be \emph{complete}. The type $\Prop$ is complete, and if $\type$ is complete, then so is $\type' \to \type$. Note that the modalities $\upd$, $\always$, $\plainly$ 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}} } %%% empty, unit, products, sums \and \infer{\vctx \proves \wtt\term{0}} {\vctx \proves \wtt{\textlog{abort}\; \term}\type} \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}} \and \infer{\vctx \proves \wtt\term{\type_i} \and i \in \{1, 2\}} {\vctx \proves \wtt{\textlog{inj}_i\;\term}{\type_1 + \type_2}} \and \infer{\vctx \proves \wtt\term{\type_1 + \type_2} \and \vctx, \var:\type_1 \proves \wtt{\term_1}\type \and \vctx, \varB:\type_2 \proves \wtt{\term_2}\type} {\vctx \proves \wtt{\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term_1 \mid \Ret\textlog{inj}_2\; \varB. \term_2 \;\textlog{end}}{\type}} %%% 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\melt{\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$} \and \text{$\type$ is complete and inhabited} }{ \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}}} {\vctx \proves \wtt{\ownM{\melt}}{\Prop}} \and \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a camera}} {\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{\plainly\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} 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} proposition 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. \judgment{\vctx \mid \prop \proves \propB} \paragraph{Laws of intuitionistic higher-order logic with equality.} This is entirely standard. \begin{mathparpagebreakable} \infer[Asm] {} {\prop \proves \prop} \and \infer[Cut] {\prop \proves \propB \and \propB \proves \propC} {\prop \proves \propC} \and \infer[Eq] {\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]} \and \infer[Refl] {} {\TRUE \proves \term =_\type \term} \and \infer[$\bot$E] {} {\FALSE \proves \prop} \and \infer[$\top$I] {} {\prop \proves \TRUE} \and \infer[$\wedge$I] {\prop \proves \propB \\ \prop \proves \propC} {\prop \proves \propB \land \propC} \and \infer[$\wedge$EL] {\prop \proves \propB \land \propC} {\prop \proves \propB} \and \infer[$\wedge$ER] {\prop \proves \propB \land \propC} {\prop \proves \propC} \and \infer[$\vee$IL] {\prop \proves \propB } {\prop \proves \propB \lor \propC} \and \infer[$\vee$IR] {\prop \proves \propC} {\prop \proves \propB \lor \propC} \and \infer[$\vee$E] {\prop \proves \propC \\ \propB \proves \propC} {\prop \lor \propB \proves \propC} \and \infer[$\Ra$I] {\prop \land \propB \proves \propC} {\prop \proves \propB \Ra \propC} \and \infer[$\Ra$E] {\prop \proves \propB \Ra \propC \\ \prop \proves \propB} {\prop \proves \propC} \and \infer[$\forall$I] { \vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\prop \proves \All \var: \type. \propB} \and \infer[$\forall$E] {\vctx\mid\prop \proves \All \var :\type. \propB \\ \vctx \proves \wtt\term\type} {\vctx\mid\prop \proves \propB[\term/\var]} \\ \infer[$\exists$I] {\vctx\mid\prop \proves \propB[\term/\var] \\ \vctx \proves \wtt\term\type} {\vctx\mid\prop \proves \exists \var: \type. \propB} \and \infer[$\exists$E] {\vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\Exists \var: \type. \prop \proves \propB} % \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, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$. \paragraph{Laws of (affine) bunched implications.} \begin{mathpar} \begin{array}{rMcMl} \TRUE * \prop &\provesIff& \prop \\ \prop * \propB &\proves& \propB * \prop \\ (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC) \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} \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} (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q) \\ \plainly ( ( P \Ra Q) \land (Q \Ra P ) ) &\proves& P =_{\Prop} 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.} \begin{mathpar} \infer[$\always$-mono] {\prop \proves \propB} {\always{\prop} \proves \always{\propB}} \and \infer[$\always$-E]{} {\always\prop \proves \prop} \and \begin{array}[c]{rMcMl} (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB \end{array} \and \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} \end{array} \end{mathpar} \paragraph{Laws for the later modality.} \begin{mathpar} \infer[$\later$-mono] {\prop \proves \propB} {\later\prop \proves \later{\propB}} \and \infer[$\later$-I] {} {\prop \proves \later\prop} \and \begin{array}[c]{rMcMl} \All x. \later\prop &\proves& \later{\All x.\prop} \\ \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\ \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \end{array} \and \begin{array}[c]{rMcMl} \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\ \always{\later\prop} &\provesIff& \later\always{\prop} \\ \plainly{\later\prop} &\provesIff& \later\plainly{\prop} \end{array} \end{mathpar} \paragraph{Laws for resources and validity.} \begin{mathpar} \begin{array}{rMcMl} \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) \end{array} % \and % \infer[valid-intro] % {\melt \in \mval} % {\TRUE \vdash \mval(\melt)} % \and % \infer[valid-elim] % {\melt \notin \mval_0} % {\mval(\melt) \proves \FALSE} \and \begin{array}{rMcMl} \ownM{\melt} &\proves& \mval(\melt) \\ \mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\ \mval(\melt) &\proves& \always\mval(\melt) \end{array} \end{mathpar} \paragraph{Laws for the basic update modality.} \begin{mathpar} \inferH{upd-mono} {\prop \proves \propB} {\upd\prop \proves \upd\propB} \inferH{upd-intro} {}{\prop \proves \upd \prop} \inferH{upd-trans} {} {\upd \upd \prop \proves \upd \prop} \inferH{upd-frame} {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update} {\melt \mupd \meltsB} {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB} \inferH{upd-plainly} {} {\upd\plainly\prop \proves \prop} \end{mathpar} The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$. %\ralf{Trouble is, we do not actually have $\in$ inside the logic...} \subsection{Consistency} The consistency statement of the logic reads as follows: For any $n$, we have \begin{align*} \lnot(\TRUE \proves (\later)^n\spac\FALSE) \end{align*} where $(\later)^n$ is short for $\later$ being nested $n$ times. 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$ and $\plainly$, this follows from the elimination rules. For updates, we use the fact that $\upd\FALSE \proves \upd\plainly\FALSE \proves \FALSE$. However, there is no elimination rule for $\later$, so we declare that it is impossible to derive a contradiction below any number of laters. %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: