model.tex 7.93 KB
Newer Older
1
\section{Model and semantics}
Ralf Jung's avatar
Ralf Jung committed
2
\label{sec:model}
3 4 5

The semantics closely follows the ideas laid out in~\cite{catlogic}.

Ralf Jung's avatar
Ralf Jung committed
6
\paragraph{Semantic domains.}
7

Ralf Jung's avatar
Ralf Jung committed
8 9 10
The semantic  domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
Ralf Jung's avatar
Ralf Jung committed
11
\Sem{\Prop} &\eqdef& \UPred(\monoid)  \\
Ralf Jung's avatar
Ralf Jung committed
12 13 14
\Sem{\textlog{M}} &\eqdef& \monoid \\
\Sem{0} &\eqdef& \Delta \emptyset \\
\Sem{1} &\eqdef& \Delta \{ () \}
Ralf Jung's avatar
Ralf Jung committed
15 16 17
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
Ralf Jung's avatar
Ralf Jung committed
18
\Sem{\type + \type'} &\eqdef& \Sem{\type} + \Sem{\type} \\
Ralf Jung's avatar
Ralf Jung committed
19 20 21 22
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
23
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\OFEs$ and define
Ralf Jung's avatar
Ralf Jung committed
24 25 26 27 28 29
\[
\Sem{\type} \eqdef X_\type
\]
For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick a function $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \nfn \Sem{\type_{n+1}}$.

\judgment[Interpretation of assertions.]{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}
30

31 32
Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$.
We are thus going to define the assertions as mapping CMRA elements to sets of step-indices.
33 34

\begin{align*}
35 36 37
	\Sem{\vctx \proves t =_\type u : \Prop}_\gamma &\eqdef
	\Lam \any. \setComp{n}{\Sem{\vctx \proves t : \type}_\gamma \nequiv{n} \Sem{\vctx \proves u : \type}_\gamma} \\
	\Sem{\vctx \proves \FALSE : \Prop}_\gamma &\eqdef \Lam \any. \emptyset \\
Robbert Krebbers's avatar
Robbert Krebbers committed
38
	\Sem{\vctx \proves \TRUE : \Prop}_\gamma &\eqdef \Lam \any. \nat \\
39 40 41 42 43 44
	\Sem{\vctx \proves \prop \land \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cap \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
	\Sem{\vctx \proves \prop \lor \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
	\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{\begin{aligned}
45
            \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land m \in \mval(\meltB) \Ra {} \\
Ralf Jung's avatar
Ralf Jung committed
46
            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
47 48 49
	\Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
	\Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\gamma &\eqdef
50 51 52
        \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) }
\end{align*}
\begin{align*}
53 54 55 56
	\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
\\
	\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{\begin{aligned}
57
            \All m, \meltB.& m \leq n \land  m \in \mval(\melt\mtimes\meltB) \Ra {} \\
58
            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
Ralf Jung's avatar
Ralf Jung committed
59
        \Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB}  \\
60
        \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \mval(\Sem{\vctx \proves \term : \textlog{M}}_\gamma) \\
Ralf Jung's avatar
Ralf Jung committed
61 62 63
	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
	\Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
	\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
Ralf Jung's avatar
Ralf Jung committed
64
        \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
65
            \All m, \melt'. & m \leq n \land m \in \mval(\melt \mtimes \melt') \Ra {}\\& \Exists \meltB. m \in \mval(\meltB \mtimes \melt') \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
Ralf Jung's avatar
Ralf Jung committed
66 67
          \end{aligned}
}
68 69
\end{align*}

Ralf Jung's avatar
Ralf Jung committed
70
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
71

Ralf Jung's avatar
Ralf Jung committed
72 73


Ralf Jung's avatar
Ralf Jung committed
74
\judgment[Interpretation of non-propositional terms]{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}}
Ralf Jung's avatar
Ralf Jung committed
75 76 77 78
\begin{align*}
	\Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\
	\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\
	\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef
Ralf Jung's avatar
Ralf Jung committed
79
	\Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \gamma} \\
Ralf Jung's avatar
Ralf Jung committed
80 81 82
	\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
	\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
	\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
83
	\fixp_{\Sem{\type}}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
Ralf Jung's avatar
Ralf Jung committed
84
  ~\\
Ralf Jung's avatar
Ralf Jung committed
85
	\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
Ralf Jung's avatar
Ralf Jung committed
86 87
	\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
	\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
Ralf Jung's avatar
Ralf Jung committed
88 89 90 91 92 93
	\Sem{\vctx \proves \pi_i\; \term : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
        \Sem{\vctx \proves \textlog{inj}_i\;\term : \type_1 + \type_2}_\gamma &\eqdef \mathit{inj}_i(\Sem{\vctx \proves \term : \type_i}_\gamma) \\
        \Sem{\vctx \proves \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var_1. \term_1 \mid \Ret\textlog{inj}_2\; \var_2. \term_2 \;\textlog{end} : \type }_\gamma &\eqdef 
    \Sem{\vctx, \var_i:\type_i \proves \term_i : \type}_{\mapinsert{\var_i}\termB \gamma} \\
    &\qquad \text{where $\Sem{\vctx \proves \term : \type_1 + \type_2}_\gamma = \mathit{inj}_i(\termB)$}
    \\
Ralf Jung's avatar
Ralf Jung committed
94
  ~\\
Ralf Jung's avatar
Ralf Jung committed
95 96 97 98
        \Sem{ \melt : \textlog{M} }_\gamma &\eqdef \melt \\
	\Sem{\vctx \proves \mcore\term : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\gamma} \\
	\Sem{\vctx \proves \term \mtimes \termB : \textlog{M}}_\gamma &\eqdef
	\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \termB : \textlog{M}}_\gamma
Ralf Jung's avatar
Ralf Jung committed
99 100 101 102 103 104
\end{align*}
%

An environment $\vctx$ is interpreted as the set of
finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and
$\rho(x)\in\Sem{\vctx(x)}$.
105
Above, $\fixp$ is Banach's fixed-point (see \thmref{thm:banach}), and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
Ralf Jung's avatar
Ralf Jung committed
106 107 108 109

\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.

Ralf Jung's avatar
Ralf Jung committed
110
\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : \mProp}
Ralf Jung's avatar
Ralf Jung committed
111 112

\[
Ralf Jung's avatar
Ralf Jung committed
113
\Sem{\vctx \mid \prop \proves \propB} \eqdef
Ralf Jung's avatar
Ralf Jung committed
114 115
\begin{aligned}[t]
\MoveEqLeft
Robbert Krebbers's avatar
Robbert Krebbers committed
116
\forall n \in \nat.\;
117
\forall \rs \in \monoid.\; 
Ralf Jung's avatar
Ralf Jung committed
118 119
\forall \gamma \in \Sem{\vctx},\;
\\&
Ralf Jung's avatar
Ralf Jung committed
120 121
n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
\Ra n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)
Ralf Jung's avatar
Ralf Jung committed
122 123 124
\end{aligned}
\]

Ralf Jung's avatar
Ralf Jung committed
125 126
The following soundness theorem connects syntactic and semantic entailment.
It is proven by showing that all the syntactic proof rules of \Sref{sec:base-logic} can be validated in the model.
Ralf Jung's avatar
Ralf Jung committed
127 128
\[ \vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB} \]

Ralf Jung's avatar
Ralf Jung committed
129
It now becomes straight-forward to show consistency of the logic.
130 131 132 133 134

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