From e62c028126fccb23aa4fd93c6a7d737dec6f70e0 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 5 Sep 2024 12:46:24 +0200 Subject: [PATCH] paper: adapt soundness theorems --- paper/main.tex | 89 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 53 insertions(+), 36 deletions(-) diff --git a/paper/main.tex b/paper/main.tex index b15f3cc..62d84a0 100644 --- a/paper/main.tex +++ b/paper/main.tex @@ -518,17 +518,23 @@ while preserving its semantics. \end{enumerate} \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 \}\) 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}\)" -can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\). + +%Using the inference rules given in \ref{def:pathrules} \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}\)" +%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] -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} \begin{mathpar} @@ -783,6 +789,20 @@ D_1 \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} \inferrule[T-App]{ 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 \{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e} } - + \inferrule[E-AppLamAscribe]{ }{ - \exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )} + \exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )} \exprterminal{\text{ as }} \typeterminal{\metavariable{\tau}} - \metavariable{e} + \exprterminal{)} + \metavariable{a} \rightarrow_\beta - \metavariable{v} - \metavariable{e} + \exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )} + \metavariable{a} } \end{mathpar} \end{definition} @@ -924,10 +945,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e \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_{\beta} \metavariable{e'}\) -it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well. +Assume the expression \(\metavariable{e}\) is well typed, +i.e. there is a type-derivation tree +\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\) +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} \todo{} @@ -936,38 +960,31 @@ it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as we \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_{\beta} \metavariable{e'}\) +Assume the expression \(\metavariable{e}\) is well typed, +i.e. there is a type-derivation tree +\(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} \todo{} \end{proof} \end{lemma} -\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} -Follows from \ref{lemma:progress} and \ref{lemma:preservation}. -\end{proof} -\end{theorem} - -\begin{theorem}[Semantic Type Soundness] +\begin{theorem}[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. \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. +\todo{} +%Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\). +%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{theorem}