Var Rule Subtyping. Add Termination Theorem

This commit is contained in:
Andreas Stadelmeier 2024-06-13 17:07:08 +02:00
parent 05260c286d
commit 71ffb2c766

View File

@ -87,6 +87,8 @@ We want to bring type inference for Java to the next level.
\type{T}_1 <: \type{T}_3
}
\and
\inferrule[Var]{}{\type{A} <: \Delta(\type{A})}
\and
\inferrule[Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
}
@ -126,6 +128,19 @@ Those can be directly translated to ASP.
\type{T}_2 \doteq \type{T}_1
}
\and
\inferrule[Unfold]{
\tv{b} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n}
}{
\type{T}_i \doteq \type{T}_i
}
\and
\inferrule[Subst-Param]{
\tv{a} \doteq \type{G} \\
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
}{
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{G}, \ldots \type{T}_n}
}
\and
\inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
\and
\inferrule[Match]{
@ -166,6 +181,7 @@ Those can be directly translated to ASP.
\end{mathpar}
\begin{mathpar}
\text{Apply only once per constraint:}\quad
\inferrule[Super]{
\type{T} \lessdot \tv{a}\\
\type{T} <: \type{N}
@ -174,6 +190,9 @@ Those can be directly translated to ASP.
}
\end{mathpar}
\begin{center}
Apply one or the other:
\end{center}
\begin{mathpar}
\inferrule[Split-L]{
\tv{a} \lessdot \tv{b}\\
@ -181,9 +200,9 @@ Those can be directly translated to ASP.
}{
\tv{b} \lessdot \type{N}
}
\and
\quad \quad
\vline
\and
\quad \quad
\inferrule[Split-R]{
\tv{a} \lessdot \tv{b}\\
\tv{a} \lessdot \type{N}\\
@ -194,9 +213,14 @@ Those can be directly translated to ASP.
Result:
\begin{mathpar}
% \inferrule[Solution]{
% \tv{a} \doteq \type{N} \\
% \tv{a} \notin \type{N}
% }{
% \sigma(\tv{a}) = \type{N}
% }
\inferrule[Solution]{
\tv{a} \doteq \type{N} \\
\tv{a} \notin \type{N}
\tv{a} \doteq \type{G}
}{
\sigma(\tv{a}) = \type{N}
}
@ -206,39 +230,20 @@ Result:
\forall i: \type{C_m} << \type{C_i} \\
\text{not}\ \tv{a} \doteq \type{N}
}{
\sigma(\tv{a}) = \exptype{C_m}{\ol{T_m}}
}
\and
\inferrule[Solution]{
\tv{a} \doteq \type{G}
}{
\sigma(\tv{a}) = \type{N}
}
\and
\inferrule[Unfold]{
\tv{b} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n}
}{
\type{T}_i \doteq \type{T}_i
}
\and
\inferrule[Subst-Param]{
\tv{a} \doteq \type{G} \\
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
}{
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{G}, \ldots \type{T}_n}
\Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \sigma(\tv{a}) = \type{A}
}
\end{mathpar}
Fail:
\begin{mathpar}
\inferrule[Fail]{
\type{T} \lessdot \type{N}\\
\type{T} \nless : \type{N}
}{
\emptyset
}
\and
% \inferrule[Fail]{
% \type{T} \lessdot \type{N}\\
% \type{T} \nless : \type{N}
% }{
% \emptyset
% }
% \and
\inferrule[Fail]{
\exptype{C}{\ldots} \doteq \exptype{D}{\ldots}\\
\type{C} \neq \type{D}
@ -338,6 +343,15 @@ Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type
And more text.
\end{proof}
\begin{lemma}{Substitution}
\begin{description}
\item[If] $\tv{a} \doteq \type{N}$ with $\tv{a} \neq \type{N}$
\item[Then] for every $\type{T} \doteq \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \doteq [\type{N}/\tv{a}]\type{T}$
\item[Then] for every $\type{T} \lessdot \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \lessdot [\type{N}/\tv{a}]\type{T}$
\end{description}
\end{lemma}
\textit{Proof:}
TODO
\begin{lemma} \label{lemma:subtypeOnly}
If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
@ -350,6 +364,18 @@ The Solution-Sub rule is always correct.
Proof:
\begin{theorem}{Termination}
%jede nichtendliche Menge von Constraints bleibt endlich. Die Regeln können nicht unendlich oft angewendet werden
%Trivial. The only possibility would be if we allow a =. C<a> constraints!
\end{theorem}
TODO: For completeness we have to proof that not $\tv{a} \doteq \type{N}$ only is the case if $\tv{a}$ only appears on the left side of $\tv{a} \lessdot \type{T}$ constraints.
Problem: a <. List<a>
a <. List<b>
then a =. b
Solution: Keep the a <. N constraints and apply the Step 6 from the GTFGJ paper.
Then we have to proof that only a <. N constraints remain with sigma(a) = empty. Or Fail
\begin{theorem}{Completeness}
$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.