Start with cctv and soundness proof

This commit is contained in:
JanUlrich 2024-07-23 10:47:20 +02:00
parent 2b57b092be
commit 0c260eef12
3 changed files with 76 additions and 22 deletions

View File

@ -38,6 +38,8 @@
\usepackage{arydshln}
\usepackage{dashbox}
\usepackage{mathpartir}
\input{prolog}
\begin{document}

View File

@ -718,3 +718,40 @@ Same as Subst
% \caption{T-Call and T-Field} \label{fig:tletexpr}
% \end{figure}
\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} \doteq \type{S'} })$
\item[Then] there exists a $\sigma'$ with:
\begin{itemize}
\item $\sigma''(\overline{\cctv{x}}) = \overline{\wctype{\Delta''}{C}{\ol{T}}}$
\item $\sigma' = \set{ \overline{\cctv{x}} \mapsto \overline{\exptype{C}{\ol{T}}} } \cup \sigma$
\item $\Delta, \Delta', \overline{\Delta''} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
\end{itemize}
\end{description}
\end{lemma}
\textit{Proof:}
For every step in the \unify{} algorithm:
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
constraint set $C$ before the transformation.
\unify{} terminates with $C = \emptyset$ for which the preposition holds:
$\Delta \vdash \sigma(\emptyset)$
We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
the preposition holds for $C$ using the assumption that it holds for $C'$ :
$\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
\begin{description}
\item[Reduce] Given $\wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
\begin{itemize}
\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
\end{itemize}
\end{description}

View File

@ -225,27 +225,6 @@ We define two types as equal if they are mutual subtypes of each other.
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
%It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\type{N'}) \subseteq \Delta_{in} \\
\text{wtv}(\type{N'}) = \emptyset
\end{array}
\end{array}
$
\\\\
\rulename{Trim}
&
$
@ -421,6 +400,42 @@ After \rulename{Subst} and \rulename{Same} the remaining constraints are $\tv{b}
$\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rwildcard{A}}$
%which is equal to $\tv{a} \lessdot \exptype{List}{\type{Integer}}$ and additionally we have $\tv{b} \doteq \type{Integer}$.
\begin{figure}
\begin{mathpar}
\inferrule[Reduce]{
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
}{
\wildcardEnv
\vdash C \cup \, \set{
\ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
\ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
}
\quad \text{wtv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
\and
\inferrule[Reduce-Empty]{
\wildcardEnv \vdash
C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
}{
\wildcardEnv
\vdash C \cup \, \set{
\ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
\ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
}
\and
\inferrule[Exclude]{
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} }
}{
\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash
[\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
}\quad \Delta \neq \emptyset,
\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
\end{mathpar}
\end{figure}
\begin{figure}
\begin{center}
\leavevmode
@ -458,7 +473,7 @@ $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rw
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\