Commit 48c7dfca authored by Ralf Jung's avatar Ralf Jung

add model for new terms

parent 06bb6d4d
Pipeline #5623 passed with stages
in 5 minutes and 52 seconds
......@@ -41,7 +41,7 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\term, \prop, \pred \bnfdef{}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
\textlog{abort}(\term) \mid
\textlog{abort}\; \term \mid
() \mid
(\term, \term) \mid
\pi_i\; \term \mid
......@@ -119,7 +119,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
%%% empty, unit, products, sums
\and
\infer{\vctx \proves \wtt\term{0}}
{\vctx \proves \wtt{\textlog{abort}(\term)}\type}
{\vctx \proves \wtt{\textlog{abort}\; \term}\type}
\and
\axiom{\vctx \proves \wtt{()}{1}}
\and
......
......@@ -9,11 +9,13 @@ The semantic domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\Prop} &\eqdef& \UPred(\monoid) \\
\Sem{\textlog{M}} &\eqdef& \monoid
\Sem{\textlog{M}} &\eqdef& \monoid \\
\Sem{0} &\eqdef& \Delta \emptyset \\
\Sem{1} &\eqdef& \Delta \{ () \}
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{1} &\eqdef& \Delta \{ () \} \\
\Sem{\type + \type'} &\eqdef& \Sem{\type} + \Sem{\type} \\
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
......@@ -80,9 +82,15 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
\mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
\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 \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)$}
\\
~\\
\Sem{ \melt : \textlog{M} }_\gamma &\eqdef \melt \\
\Sem{\vctx \proves \mcore\term : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\gamma} \\
......@@ -94,6 +102,7 @@ For every definition, we have to show all the side-conditions: The maps have to
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)}$.
Above, $\mathit{fix}$ is the fixed-point on COFEs, and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment