senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

paper: adapt soundness theorems

Browse source
This commit is contained in:
Michael Sippel 2024-09-05 12:46:24 +02:00
parent 6f81686105
commit e62c028126
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 53 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
paper/main.tex
View file

@ -518,17 +518,23 @@ while preserving its semantics.
\end{enumerate} \end{enumerate}
\end{example} \end{example}
\subsubsection{Inference of Expression Types} \subsubsection{Typing Context}
As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) 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}\). 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 \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" %Using the inference rules given in \ref{def:pathrules} \ref{def:typerules}, further typing-judgements
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\). %of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
%can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
\subsubsection{Morphism Graph}
Every typing context \(\Gamma\) implies a \emph{Morphism Graph}, a directed graph whose vertices are types
and the edges represent a type-transformations, as defined by morphisms.
A type \(\metavariable{\tau}\) can be implicitly coerced into a type \(\metavariable{\tau'}\),
provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\),
written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
\begin{definition}[Morphism Paths] \begin{definition}[Morphism Paths]
Given a typing context \(\Gamma\), any type \(\metavariable{\tau}\) can be transformed into \(\metavariable{\tau'}\), provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\), written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
\label{def:pathrules} \label{def:pathrules}
\begin{mathpar} \begin{mathpar}
@ -783,6 +789,20 @@ D_1
\and \and
\Big{\llbracket}
\inferrule[T-MorphAbs]{
D_1 :: \Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
\metavariable{\tau} \precsim \metavariable{\tau'}
}{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_\text{morph}}\metavariable{\tau'}
}
\Big{\rrbracket} =
\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau}
\exprterminal{\mapsto_\text{morph}} \Big{\llbracket}D_1\Big{\rrbracket}
\and
\Big{\llbracket} \Big{\llbracket}
\inferrule[T-App]{ \inferrule[T-App]{
D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
@ -905,16 +925,17 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\rightarrow_\beta \rightarrow_\beta
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e} \{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
} }
\inferrule[E-AppLamAscribe]{ \inferrule[E-AppLamAscribe]{
}{ }{
\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )} \exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\exprterminal{\text{ as }} \exprterminal{\text{ as }}
\typeterminal{\metavariable{\tau}} \typeterminal{\metavariable{\tau}}
\metavariable{e} \exprterminal{)}
\metavariable{a}
\rightarrow_\beta \rightarrow_\beta
\metavariable{v} \exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\metavariable{e} \metavariable{a}
} }
\end{mathpar} \end{mathpar}
\end{definition} \end{definition}
@ -924,10 +945,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\begin{lemma}[Preservation] \begin{lemma}[Preservation]
\label{lemma:preservation} \label{lemma:preservation}
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) Assume the expression \(\metavariable{e}\) is well typed,
for some type \(\metavariable{\tau}\). i.e. there is a type-derivation tree
Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) \(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well. for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then forall \(\metavariable{e'}\) with \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof} \begin{proof}
\todo{} \todo{}
@ -936,38 +960,31 @@ it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as we
\begin{lemma}[Progress] \begin{lemma}[Progress]
\label{lemma:progress} \label{lemma:progress}
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), Assume the expression \(\metavariable{e}\) is well typed,
then either \(\metavariable{e}\) is a value i.e. there is a type-derivation tree
or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) \(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then either \(\metavariable{e}\) is a value
or there exists some \(\metavariable{e'}\) such that \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
\begin{proof} \begin{proof}
\todo{} \todo{}
\end{proof} \end{proof}
\end{lemma} \end{lemma}
\begin{theorem}[Syntactic Type Soundness] \begin{theorem}[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}
Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
\end{proof}
\end{theorem}
\begin{theorem}[Semantic Type Soundness]
\label{theorem:semantic-soundness} \label{theorem:semantic-soundness}
No semantically well-typed expression is stuck. No well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\). Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\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. 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} \begin{proof}
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\). \todo{}
By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\) %Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\).
and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck. %By \ref{lemma:translation}, \(\Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
%and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
\end{proof} \end{proof}
\end{theorem} \end{theorem}