model.tex 6.85 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
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
The semantic  domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\textlog{\Prop}} &\eqdef& \UPred(\monoid)  \\
\Sem{\textlog{M}} &\eqdef& \monoid
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{1} &\eqdef& \Delta \{ () \} \\
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
\[
\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)}
28

29
30
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.
31
32

\begin{align*}
33
34
35
36
37
38
39
40
41
42
43
	\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 \\
	\Sem{\vctx \proves \TRUE : \Prop}_\gamma &\eqdef \Lam \any. \mathbb{N} \\
	\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}
            \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
Ralf Jung's avatar
Ralf Jung committed
44
            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
45
46
47
48
49
50
51
52
53
54
55
	\Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
	\Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef
        \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
  ~\\
	\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}
            \All m, \meltB.& m \leq n \land  \melt\mtimes\meltB \in \mval_m \Ra {} \\
            & 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
56
57
58
59
60
	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
	\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)}\\
        \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mincl[n] \meltB}  \\
        \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \melt : \type}_\gamma \in \mval_n} \\
        \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
61
            \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
Ralf Jung's avatar
Ralf Jung committed
62
63
          \end{aligned}
}
64
65
\end{align*}

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

Ralf Jung's avatar
Ralf Jung committed
68
69


Ralf Jung's avatar
Ralf Jung committed
70
\judgment[Interpretation of non-propositional terms]{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}}
Ralf Jung's avatar
Ralf Jung committed
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
\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
	\Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\
	\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
	\mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\
  ~\\
	\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) \\
	\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 \mcore\melt : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma} \\
	\Sem{\vctx \proves \melt \mtimes \meltB : \textlog{M}}_\gamma &\eqdef
	\Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textlog{M}}_\gamma
\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)}$.

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

Ralf Jung's avatar
Ralf Jung committed
98
\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : \mProp}
Ralf Jung's avatar
Ralf Jung committed
99
100

\[
Ralf Jung's avatar
Ralf Jung committed
101
\Sem{\vctx \mid \prop \proves \propB} \eqdef
Ralf Jung's avatar
Ralf Jung committed
102
103
104
105
106
107
\begin{aligned}[t]
\MoveEqLeft
\forall n \in \mathbb{N}.\;
\forall \rs \in \textdom{Res}.\; 
\forall \gamma \in \Sem{\vctx},\;
\\&
Ralf Jung's avatar
Ralf Jung committed
108
109
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
110
111
112
\end{aligned}
\]

Ralf Jung's avatar
Ralf Jung committed
113
114
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
115
116
\[ \vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB} \]

Ralf Jung's avatar
Ralf Jung committed
117
It now becomes straight-forward to show consistency of the logic.
118
119
120
121
122

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