Cleanup soundness. Add Delta environment to Unify input

This commit is contained in:
Andreas Stadelmeier 2024-01-23 16:30:24 +01:00
parent 881eecef8a
commit 05b6b84e1e
2 changed files with 32 additions and 79 deletions

View File

@ -13,6 +13,10 @@ Type inference produces a correctly typed program.
\end{description}
\end{theorem}
\begin{lemma}{Well-formedness:}
TODO:
\end{lemma}
\begin{lemma}{Soundness:}
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description}
@ -44,7 +48,7 @@ By structural induction over the expression $\texttt{e}$.
then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
$\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
%Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
%Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
@ -62,7 +66,9 @@ By structural induction over the expression $\texttt{e}$.
$\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
%Easy, because unify only generates substitutions for normal type placeholders which are OK
\item[$\texttt{e}.\texttt{m}(\ol{e})$]
\item[$\texttt{e}.\texttt{m}(\ol{e})$]
Lets have a look at the case where the receiver and parameter types are all named types.
So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:
\begin{gather}
\label{sp:1}
\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
@ -70,7 +76,7 @@ By structural induction over the expression $\texttt{e}$.
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
\label{sp:4}
\Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} \\
\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} \\
\end{gather}
\ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
$\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with
@ -78,6 +84,12 @@ By structural induction over the expression $\texttt{e}$.
If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
\ref{sp:4} is not using $\ol{\Delta}$.
$\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$
Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
%TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)
% X.List<X> <. List<a?>
% set \sigma(r) = X.N
% If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
@ -100,73 +112,32 @@ By structural induction over the expression $\texttt{e}$.
% If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
\end{description}
\begin{lemma}
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( C )$
\item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
\end{description}
\end{lemma}
\textit{Proof:} by induction over the \unify{} algorithm.
A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
$\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
%UNIFY fails when there are free variables on the right side of a a =. T constraint
\begin{lemma}
\unify{} only produces well-formed type substitutions.
% Could this be done via the GenSigma rule? just check if substitutions are well-formed?
% L <. U
% not possible because well-formedness depends on the input, which is not checked (should we check it? is that possible?)
%only type variables have to be OK
% TODO: Problem: how to proof \ol{S} ok for T-Call.
% a <. List<x?> --> here the type substituted for x? must be ok. Proof that by changing Unify to not return type insertions for this type and assume there is a correct substitution for x
\end{lemma}
% %This lemma can be used to proof Normalize rule!
% \begin{lemma}\label{lemma:wildcardReplacement}
% Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations.
% \begin{description}
% \item[If] $\Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash \type{T} <: \type{S}$
% \item[and] $\type{U} = \type{L}$ and $\text{fv}(\type{U}) = \emptyset$
% \item[Then] $\Delta \vdash [\type{U}/\type{X}]\type{T} <: [\type{U}/\type{X}]\type{S}$
% \end{description}
% \end{lemma}
% \textit{Proof:} %TODO
% %By structural induction over the subtype relation
% %S-Refl: by assumption L <: L implies [\type{U}/\type{X}]L
% \begin{lemma}\label{lemma:noAdditionalFV}
% Type solution $\sigma$ does not add additional free variables.
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup C)$
% \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
% \item[Then] $fv(\sigma(\overline{ \type{S} })) = \emptyset, fv(\sigma(\overline{ \type{T} })) = \emptyset$
% \end{description}
% \end{lemma}
% \begin{lemma}
% % https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Book%3A_Mathematical_Reasoning__Writing_and_Proof_(Sundstrom)/07%3A_Equivalence_Relations/7.03%3A_Equivalence_Classes
% $\doteq$ is an equivalence relation on a constraint set $C$.
% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
% \begin{description}
% \item[If] $\Delta \vdash \overline{\type{T} <: \type{S}}$ and $\type{T} \doteq \type{S}$
% \item[Then] $\Delta \vdash [\type{T}/\type{S}](\overline{\type{T} <: \type{S}})$
% \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
% \item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
% \end{description}
% \end{lemma}
% \textit{Proof:} by induction over the \unify{} algorithm.
% A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
% $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
% %UNIFY fails when there are free variables on the right side of a a =. T constraint
\begin{lemma} \label{lemma:tvsNoFV}
\unify{} does not add free variables to types not containing free variables.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{} (C)$
\item[If] $(\sigma, \Delta) = \unify{} (\Delta', C)$
\item[and] $\tv{a}$ being a type placeholders used in $C$
\item[then] $\text{fv}(\sigma(\tv{a})) = \emptyset$
\item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
\end{description}
\end{lemma}
\textit{Proof:}
Trivial
Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
\begin{lemma} \label{lemma:unifyCC}
Free variables do not leave their scope. TODO
Wildcard variables are only substituted by wildcards inside the same constraint.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
\item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$,
@ -180,11 +151,6 @@ Free variables do not leave their scope. TODO
Their scope is the set of constraints, which contain the same free variable placeholders.
% Wildcard place holders only use free variables occuring in the same constraint as them.
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( C )$
% \item[Then] $\text{fv}(\sigma(\tv{a})) \subseteq \set{ \text{fv}(\type{T}) \cup \text{fv}(\type{S}) \mid \tv{a} \in \text{tph}(\type{T},\type{S}), (\type{T} \lessdot \type{S}) \in C }$
% \end{description}
\end{lemma}
\textit{Proof:}
%TODO: is it true even?
@ -192,20 +158,6 @@ The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.
%where to get a Box<Box<a?>> ?
% Box<Box<a?>> <. Box<? super Box<?>>
% %What is with wildcards in the lower bounds of type
% Box<Box<a?>> <. X_Y.Box<Y>.Box<X>
% Y.Box<Y> <. Box<a?>
% Y =. a?
% Box<Y.Box<Y>> <. Box<? extends Box<a>>
% Y.Box<Y> <. Box<a>
% Problem: für tvs dürfen keine Wildcards eingesetzt werden, außer für die
\begin{lemma}\label{lemma:unifySoundness}
The \unify{} algorithm only produces correct output.
\begin{description}
@ -213,14 +165,13 @@ The \unify{} algorithm only produces correct output.
%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\sigma'$ with:
$\sigma \subseteq \sigma'$ and
$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
$\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
% The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
% List<b?> <. List<b?>
% b? =. X

View File

@ -5,7 +5,8 @@
The \unify{} algorithm computes the type solution.
\begin{description}
\item[Input:] List of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \doteq \type{T} \ldots}$
\item[Input:] An environment $\Delta'$
and a List of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \doteq \type{T} \ldots}$
The input constraints must be of the following format:
@ -18,6 +19,7 @@ The input constraints must be of the following format:
\noindent
Additional requirements:
\begin{itemize}
\item Every wildcard $\rwildcard{X} \in \Delta'$ has to have an unique name which is not defined anywhere in the constraint set $C$.
\item The input only consists of $\lessdot$ constraints
% \item No free variables in type parameters.
% A constraint like $\tv{a} \lessdot \exptype{List}{\rwildcard{X}}$ is prohibited.
@ -91,7 +93,7 @@ C \cup \set{\tv{a} \doteq \type{T}}
\end{array}
\quad \begin{array}{c}
\tv{a} \notin \type{T} \\
\text{fv}(\type{T}) = \emptyset
\text{fv}(\type{T}) \subseteq \Delta'
\end{array}$\\
\\
\rulename{Subst-WC} &$