coercion semantics
This commit is contained in:
parent
b8e8543813
commit
8da65e4d38
GPG key ID:
F96CF119C34B64A6
1 changed files with 158 additions and 100 deletions
258
paper/main.tex
258
paper/main.tex
|
|
@ -508,40 +508,42 @@ while preserving its semantics.
|
|||
|
||||
\subsubsection{Inference of Expression Types}
|
||||
|
||||
The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).
|
||||
As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
|
||||
is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
|
||||
Using the inference rules given in \ref{def:typerules}, further typing-judgements
|
||||
of the form
|
||||
\begin{itemize}
|
||||
\item \(\metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
|
||||
\item \(\metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
|
||||
\item \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
|
||||
\item \(\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
|
||||
\end{itemize}
|
||||
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
|
||||
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
|
||||
|
||||
|
||||
|
||||
\begin{definition}[Syntactic Well-Typedness]
|
||||
An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
|
||||
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
|
||||
such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Semantic Well-Typedness]
|
||||
An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
|
||||
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules}.
|
||||
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
|
||||
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Inference Rules for the Typing Relation.]
|
||||
\label{def:typerules}
|
||||
|
||||
As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
|
||||
\begin{definition}[Syntactic Typing Relation]
|
||||
|
||||
\label{def:typerules}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[T-Variable]{
|
||||
\metavariable{x} \in \exprvars\\
|
||||
\metavariable{\tau} \in \nonterm{T}\\
|
||||
% \metavariable{x} \in \exprvars\\
|
||||
% \metavariable{\tau} \in \nonterm{T}\\
|
||||
\metavariable{x}:\metavariable{\tau} \in \Gamma\\
|
||||
}{
|
||||
\Gamma \vdash \metavariable{x}:\metavariable{\tau}
|
||||
}\and
|
||||
|
||||
|
||||
\inferrule[T-LetBinding]{
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
|
||||
\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau}
|
||||
|
|
@ -549,17 +551,16 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
|
|||
\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau}
|
||||
}
|
||||
|
||||
|
||||
\inferrule[T-TypeAbs]{
|
||||
\metavariable{\tau} \in \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
% \metavariable{\tau} \in \nonterm{T} \\
|
||||
% \metavariable{e} \in \nonterm{E} \\
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
|
||||
}{
|
||||
\Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
|
||||
}
|
||||
|
||||
\inferrule[T-TypeApp]{
|
||||
\metavariable{\tau} \in \nonterm{T} \\
|
||||
% \metavariable{\tau} \in \nonterm{T} \\
|
||||
\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
|
||||
\metavariable{\sigma} \in \nonterm{T}
|
||||
}{
|
||||
|
|
@ -567,42 +568,34 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
|
|||
}
|
||||
|
||||
|
||||
\inferrule[T-ValueAbs]{
|
||||
\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
|
||||
\inferrule[T-Abs]{
|
||||
% \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
|
||||
% \metavariable{e} \in \nonterm{E} \\
|
||||
\Gamma,\metavariable{x}:\metavariable{\sigma} \vdash \metavariable{e} : \metavariable{\tau} \\
|
||||
}{
|
||||
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
|
||||
}
|
||||
|
||||
\inferrule[T-ValueApp]{
|
||||
\inferrule[T-App]{
|
||||
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
|
||||
\Gamma \vdash \metavariable{a} : \metavariable{\sigma} \\
|
||||
}{
|
||||
\Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau}
|
||||
}\and
|
||||
|
||||
|
||||
\inferrule[T-Compatible]{
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}
|
||||
}\and
|
||||
|
||||
\inferrule[T-MorphAbs]{
|
||||
\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
|
||||
}{
|
||||
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
|
||||
}\and
|
||||
|
||||
\inferrule[T-MorphApp]{
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
|
||||
\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
|
||||
% \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
|
||||
% \metavariable{e} \in \nonterm{E} \\
|
||||
\Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
|
||||
\metavariable{\tau} \precsim \metavariable{\tau'}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
|
||||
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\metavariable{\tau'}
|
||||
}\and
|
||||
|
||||
\inferrule[T-MorphFun]{
|
||||
\Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
|
||||
}\and
|
||||
|
||||
\inferrule[T-Ascension]{
|
||||
|
|
@ -617,16 +610,98 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
|
|||
\metavariable{\tau} \leq \metavariable{\tau'}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{e} : \metavariable{\tau'}
|
||||
}\and
|
||||
}
|
||||
|
||||
\end{mathpar}
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Semantic Typing Relation]
|
||||
\label{def:semtyperules}
|
||||
\begin{mathpar}
|
||||
\inferrule[T-NativeRepr]{
|
||||
\Gamma\vdash \metavariable{e} : \metavariable{\tau}
|
||||
}{
|
||||
\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
|
||||
}
|
||||
|
||||
\inferrule[T-CoercedRepr]{
|
||||
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
|
||||
% \metavariable{\tau} \precsim \metavariable{\tau'}\\
|
||||
%\exists \metavariable{h} \text{ s.t. }
|
||||
\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
|
||||
}
|
||||
|
||||
|
||||
\inferrule[T-CompatibleApp]{
|
||||
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
|
||||
\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
|
||||
}{
|
||||
\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
|
||||
}
|
||||
\end{mathpar}
|
||||
\end{definition}
|
||||
|
||||
\subsection{Coercion Semantics}
|
||||
|
||||
We define the translation function \(\llbracket . \rrbracket\) which completes a \emph{semantically well-typed} expression
|
||||
by inserting all required coercions based on the typing derivation of the expression.
|
||||
The result shall be a \emph{syntactically well-typed} expression.
|
||||
|
||||
We write \(C :: \sigma \precsim \tau\) to mean "C is a subtyping derivation tree whose conclusion is \(\sigma \precsim \tau\)".
|
||||
Similarly, we write \(D :: \Gamma \vdash e : \tau\) to mean "D is a typing derivation whose conclusion is \(\Gamma \vdash e : \tau\)"
|
||||
|
||||
\begin{definition}[Translation]
|
||||
\begin{mathpar}
|
||||
|
||||
\Big{\llbracket} \inferrule[T-SemanticSubtype]{
|
||||
D_1 :: \Gamma \vdash \metavariable{h}:\metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}\\
|
||||
D_2 :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\\
|
||||
% C :: \metavariable{\tau} \precsim \metavariable{\tau'}
|
||||
}{
|
||||
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
|
||||
}\Big{\rrbracket} = \exprterminal{(}
|
||||
\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
|
||||
%\metavariable{h} \llbracket D_2 \rrbracket
|
||||
\exprterminal{)}
|
||||
|
||||
\Big{\llbracket} \inferrule[T-CoercedApp]{
|
||||
D_1 :: \Gamma \vdash \metavariable{f}:\metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
|
||||
D_2 :: \Gamma \vdash \metavariable{a}:\approx\metavariable{\sigma}
|
||||
}{
|
||||
\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
|
||||
}\Big{\rrbracket} = \exprterminal{(}
|
||||
%\exprterminal{(}\metavariable{f} \llbracket D_2 \rrbracket \exprterminal{)}
|
||||
\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
|
||||
\exprterminal{)}
|
||||
|
||||
\Big{\llbracket}
|
||||
\inferrule[\emph{Otherwise}]{}{
|
||||
D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}
|
||||
}
|
||||
\Big{\rrbracket} = \metavariable{e}
|
||||
|
||||
\end{mathpar}
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[Elimination of \(:\approx\)]
|
||||
\label{lemma:translation}
|
||||
|
||||
For all \emph{semantically well-typed} expressions \metavariable{e} with the typing derivation \(D :: \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\),
|
||||
the translation \(\llbracket D \rrbracket = \metavariable{e'}\), yields a \emph{syntactically well-typed} expression \metavariable{e'} with
|
||||
\(\emptyset \vdash \metavariable{e'} : \metavariable{\tau} \)
|
||||
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
\end{proof}
|
||||
|
||||
\end{lemma}
|
||||
|
||||
|
||||
\subsection{Evaluation}
|
||||
|
||||
Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
|
||||
which are given in \ref{def:evalrules}.
|
||||
Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by exhaustive application of the rewrite rule \(\rightarrow_\beta\) as in \ref{def:evalrules}.
|
||||
|
||||
\begin{definition}[Inference Rules for Evaluation]
|
||||
\label{def:evalrules}
|
||||
|
|
@ -644,13 +719,13 @@ which are given in \ref{def:evalrules}.
|
|||
\inferrule[E-App2]{
|
||||
\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
|
||||
}{
|
||||
\metavariable{e_1} \metavariable{e_2}
|
||||
\metavariable{v_1} \metavariable{e_2}
|
||||
\rightarrow_\beta
|
||||
\metavariable{e_1} \metavariable{e_2'}
|
||||
}
|
||||
\metavariable{v_1} \metavariable{e_2'}
|
||||
}\and
|
||||
|
||||
\inferrule[E-TypApp]{
|
||||
\metavariable{\tau} \in \typenonterm{\emptyset}\\
|
||||
% \metavariable{\tau} \in \typenonterm{\emptyset}\\
|
||||
\metavariable{e} \rightarrow_\beta \metavariable{e'}
|
||||
}{
|
||||
\metavariable{e}
|
||||
|
|
@ -671,7 +746,6 @@ which are given in \ref{def:evalrules}.
|
|||
\rightarrow_\beta
|
||||
\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
|
||||
}\and
|
||||
|
||||
\inferrule[E-AppLam]{
|
||||
}{
|
||||
\exprterminal{(\lambda} \metavariable{x}
|
||||
|
|
@ -690,64 +764,27 @@ which are given in \ref{def:evalrules}.
|
|||
\exprterminal{\text{ in }}\metavariable{e}
|
||||
\rightarrow_\beta
|
||||
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
|
||||
}
|
||||
|
||||
|
||||
\inferrule[E-ImplicitCast]{
|
||||
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
|
||||
\Gamma \vdash \metavariable{h} : \metavariable{\sigma'} \typeterminal{\rightarrow_{morph}} \metavariable{\sigma} \\
|
||||
\Gamma \vdash \metavariable{a} : \metavariable{\sigma'}
|
||||
}\and
|
||||
\inferrule[E-Ascribe]{
|
||||
}{
|
||||
\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
|
||||
\rightarrow_\delta
|
||||
\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
|
||||
\metavariable{e}
|
||||
\exprterminal{\text{ as }}
|
||||
\metavariable{\tau}
|
||||
\rightarrow_\beta
|
||||
\metavariable{e}
|
||||
}
|
||||
|
||||
\end{mathpar}
|
||||
\end{definition}
|
||||
|
||||
|
||||
\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
|
||||
\label{lemma:preserve-delta-normalform}
|
||||
Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow_\beta \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
\end{proof}
|
||||
\end{lemma}
|
||||
|
||||
\begin{lemma}[\(\delta\)-normalform eliminates compatibility]
|
||||
\label{lemma:eliminate-compat}
|
||||
Assume \(\emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\) and \(\metavariable{e} \rightarrow_{\delta}^* \metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
|
||||
Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\)
|
||||
|
||||
\begin{proof}
|
||||
\end{proof}
|
||||
|
||||
\end{lemma}
|
||||
|
||||
\subsection{Soundness}
|
||||
|
||||
\begin{lemma}[\(\beta\)-Preservation]
|
||||
\label{lemma:beta-preservation}
|
||||
Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
|
||||
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
\end{proof}
|
||||
|
||||
\end{lemma}
|
||||
|
||||
\begin{lemma}[\(\delta\)-Preservation]
|
||||
\label{lemma:delta-preservation}
|
||||
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
\end{proof}
|
||||
\end{lemma}
|
||||
|
||||
\begin{lemma}[Preservation]
|
||||
\label{lemma:preservation}
|
||||
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
|
||||
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
|
||||
for some type \(\metavariable{\tau}\).
|
||||
Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
|
||||
it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
|
||||
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
|
|
@ -756,23 +793,44 @@ Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdas
|
|||
|
||||
\begin{lemma}[Progress]
|
||||
\label{lemma:progress}
|
||||
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
|
||||
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
|
||||
then either \(\metavariable{e}\) is a value
|
||||
or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
|
||||
|
||||
\begin{proof}
|
||||
\todo{}
|
||||
\end{proof}
|
||||
\end{lemma}
|
||||
|
||||
\begin{theorem}[Soundness]
|
||||
If \(\emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
|
||||
\begin{theorem}[Syntactic Type Soundness]
|
||||
\label{theorem:syntactic-soundness}
|
||||
No syntactically well-typed expression is stuck.
|
||||
|
||||
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
|
||||
Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
|
||||
|
||||
\begin{proof}
|
||||
By \ref{lemma:}
|
||||
Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
|
||||
\end{proof}
|
||||
\end{theorem}
|
||||
|
||||
\begin{theorem}[Semantic Type Soundness]
|
||||
\label{theorem:semantic-soundness}
|
||||
No semantically well-typed expression is stuck.
|
||||
|
||||
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
|
||||
Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
|
||||
|
||||
\begin{proof}
|
||||
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
|
||||
By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
|
||||
and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
|
||||
\end{proof}
|
||||
\end{theorem}
|
||||
|
||||
|
||||
|
||||
\newpage
|
||||
\section{Boehm-Berarducci Encoding}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue