stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Soundness proof rework WIP

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-24 00:38:29 +02:00
parent 2b57b092be
commit df24f3fd2f
3 changed files with 91 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
prolog.tex
View File

@ -1,5 +1,6 @@
\usepackage{xspace} \usepackage{xspace}
\usepackage{color,ulem} \usepackage{color,ulem}
\usepackage{mathpartir}
\usepackage{listings} \usepackage{listings}
\lstset{language=Java, \lstset{language=Java,
showspaces=false, showspaces=false,

39
soundness.tex
View File

@ -91,6 +91,10 @@
% TODO: % TODO:
% \end{lemma} % \end{lemma}
\unify{} calculates solutions for all normal type placeholders.
Those are used for all untyped method's argument and return type.
A correct typing for method calls can be deducted from those type informations.
\begin{lemma}{Soundness:}\label{lemma:soundness} \begin{lemma}{Soundness:}\label{lemma:soundness}
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct. \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description} \begin{description}
@ -131,7 +135,12 @@ By structural induction over the expression $\texttt{e}$.
and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness} and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
given the constraint $\tv{e}_2 \lessdot \tv{a}$. given the constraint $\tv{e}_2 \lessdot \tv{a}$.
\item[$\expr{v}.\texttt{f}$] \item[$\expr{v}.\texttt{f}$]
We are alowwed to use capture conversion for $\expr{v}$ here. %TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
% but it also works with a subset of the initial constraints.
% the generated constraints do not share wildcard placehodlers with other constraints.
% can they contain free variables from other places? They could, but isolation prevents that.
% TODO: but how to proof?
We are allowed to use capture conversion for $\expr{v}$ here.
$\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption. $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
$\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
$\Delta \vdash \type{U}_i <: \sigma(\tv{a})$, $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
@ -387,13 +396,20 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
\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'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with: with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
\begin{itemize} \item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
\item $\sigma \subseteq \sigma'$ \item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$ or $\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S'}) <: \sigma(\type{T'})}$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ with the capture converted substitution $\sigma' = \set{ \tv{a} \mapsto \type{N} \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma}$
\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ and $\overline{\Delta} = \set{\Delta \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma }$
\end{itemize}
% there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ 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{description}
\end{lemma} \end{lemma}
@ -467,6 +483,13 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}. <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.
\item[Reduce] \item[Reduce]
To proof $\wctype{\Delta}{C}{\ol{S}} <: \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}
%Assumption and S-Exists. %Assumption and S-Exists.
% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$: % Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:

71
unify.tex
View File

@ -576,18 +576,18 @@ gets the same wildcard twice.
\text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset \text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
\end{array}$\\ \end{array}$\\
\\ \\
\rulename{Subst} & % \rulename{Subst} &
$\begin{array}[c]{l} % $\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\ % \wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
\hline % \hline
[\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}] % [\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
C \cup \set{\ntv{a} \doteq \type{T}} % C \cup \set{\ntv{a} \doteq \type{T}}
\end{array} % \end{array}
\quad \begin{array}{c} % \quad \begin{array}{c}
\ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\ % \ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
\text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset % \text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
\end{array}$\\ % \end{array}$\\
\\ % \\
\rulename{Subst-WC} &$ \rulename{Subst-WC} &$
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\ \wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
@ -1019,6 +1019,53 @@ List<? extends Object> someList(){
\caption{Constraint normalize rules}\label{fig:normalizing-rules} \caption{Constraint normalize rules}\label{fig:normalizing-rules}
\end{figure} \end{figure}
\begin{figure}
\begin{mathpar}
\inferrule[Capture]{
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\
}{
\wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
\vdash C \cup \, \set{
[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
}
\quad \ol{\rwildcard{C}} \ \text{fresh}
\and
\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{figure}
\begin{center} \begin{center}
\leavevmode \leavevmode