model.tex 6.85 KB
 Ralf Jung committed Jan 31, 2016 1 \section{Model and semantics} Ralf Jung committed Mar 15, 2016 2 \label{sec:model} Ralf Jung committed Jan 31, 2016 3 4 5 The semantics closely follows the ideas laid out in~\cite{catlogic}. Ralf Jung committed Oct 04, 2016 6 \paragraph{Semantic domains.} Ralf Jung committed Jan 31, 2016 7 Ralf Jung committed Oct 04, 2016 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)} Ralf Jung committed Jan 31, 2016 28 Ralf Jung committed Mar 12, 2016 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. Ralf Jung committed Jan 31, 2016 31 32 \begin{align*} Ralf Jung committed Mar 12, 2016 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 committed Aug 11, 2016 44 & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\ Ralf Jung committed Mar 12, 2016 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 committed Oct 04, 2016 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} Aleš Bizjak committed Oct 09, 2016 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 committed Oct 04, 2016 62 63 \end{aligned} } Ralf Jung committed Jan 31, 2016 64 65 \end{align*} Ralf Jung committed Mar 12, 2016 66 For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone. Ralf Jung committed Mar 12, 2016 67 Ralf Jung committed Mar 12, 2016 68 69 Ralf Jung committed Oct 04, 2016 70 \judgment[Interpretation of non-propositional terms]{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}} Ralf Jung committed Mar 12, 2016 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 committed Aug 11, 2016 98 \typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : \mProp} Ralf Jung committed Mar 12, 2016 99 100 Ralf Jung committed Oct 06, 2016 101 \Sem{\vctx \mid \prop \proves \propB} \eqdef Ralf Jung committed Mar 12, 2016 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 committed Oct 06, 2016 108 109 n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs) \Ra n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs) Ralf Jung committed Mar 12, 2016 110 111 112 \end{aligned} Ralf Jung committed Oct 07, 2016 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 committed Oct 06, 2016 115 116 $\vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB}$ Ralf Jung committed Oct 07, 2016 117 It now becomes straight-forward to show consistency of the logic. Ralf Jung committed Jan 31, 2016 118 119 120 121 122 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: