base-logic.tex

\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}
\inferhref{$\always$-mono}{pers-mono}
  {\prop \proves \propB}
  {\always{\prop} \proves \always{\propB}}
\and
\inferhref{$\always$-E}{pers-elim}
{}
{\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}
\inferhref{$\later$-mono}{later-mono}
  {\prop \proves \propB}
  {\later\prop \proves \later{\propB}}
\and
\inferhref{$\later$-I}{later-intro}
  {}
  {\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& \plainly\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}

\inferhref{upd-I}{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: