Adding to Soundness proof: Adding the old Unify-Soundness. Start writing lemmas to proof free variables cannot travel out of the scope of a let statement. They can only travel one hop at a time -> cant go through normal type placeholders

This commit is contained in:
Andreas Stadelmeier 2024-08-09 23:35:36 +02:00
parent a41b298566
commit b50a6a93a2

View File

@ -86,11 +86,17 @@ We have to show T-Let and T-Call which leaves us with:
\begin{itemize} \begin{itemize}
\item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
\item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied.
Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are
solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$.
\begin{itemize} \begin{itemize}
\item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step. \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
\item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness} \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit) there must be some $\ol{S}$ satisfying this premise.
% what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints
%TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
\item
\end{itemize} \end{itemize}
\end{itemize} \end{itemize}
\item[$\texttt{v}.\texttt{m}(\ol{v})$] \item[$\texttt{v}.\texttt{m}(\ol{v})$]
@ -156,12 +162,56 @@ We have to show T-Let and T-Call which leaves us with:
\end{description} \end{description}
During the unification process free variables can only move one hop at a time.
Free variables originate from capture constraints.
By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$
are now free in the constraint $\type{N} \lessdot \type{T}$.
The other way of free variables traveling into a constraint is by substitution.
This is only possible if a constraint contains wildcard placeholders.
And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in.
This effect is transitive. Free variables travel from constraint to constraint.
If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint,
then free variables cannot travel there.
\begin{lemma} \begin{lemma}
Free variables never leave their scope. Free variables travel only
If $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
\tv{r} \lessdot \tv{a}$ % TODO
\end{lemma} \end{lemma}
\begin{lemma}{Free variables}\label{lemma:freeVariableScope}
Free variables never leave their scope.
If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set,
then it will never contain free variables used outside of it.
$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
\end{lemma}
\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.
If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders
used for the method call.
No other free variables can move into that scope.
With this lemma we can further proof that during a method call only the generated free variables are used.
% \begin{lemma}
% Free variables never leave their scope.
% $C' = \set{
% \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}},
% \overline{\tv{r} \lessdot \tv{a}}
% }$
% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him
% \end{lemma}
% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders) % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
% \begin{description} % \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$ % \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
@ -288,11 +338,24 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
%TODO %TODO
% does this really work. We have to show that the algorithm never gets stuck as long as there is a solution % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
% maybe there are substitutions with types containing free variables that make additional solutions possible. Check! % maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness} \begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}. \unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
\begin{description} \begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
\item[Then] there exists a substitution $\sigma'$ with:
\begin{itemize}
\item $\sigma \subseteq \sigma'$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$
\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
\end{itemize}
\end{description}
\end{lemma}
\begin{lemma}{\unify{} Soundness:}%\label{lemma:unifySoundness}
\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$ with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
\item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ \item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
\item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$ \item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$