Start Implication Rules

This commit is contained in:
Andreas Stadelmeier 2024-06-10 09:03:46 +02:00
parent 4a2f3078e6
commit 2702bf6cab

View File

@ -19,6 +19,11 @@
%\renewcommand\UrlFont{\color{blue}\rmfamily} %\renewcommand\UrlFont{\color{blue}\rmfamily}
%\urlstyle{rm} %\urlstyle{rm}
% %
\include{prolog}
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{amssymb}
\begin{document} \begin{document}
% %
\title{Global Type Inference for Java using SAT Solvers} \title{Global Type Inference for Java using SAT Solvers}
@ -70,4 +75,78 @@ Java has adopted more and more type inference features over time.
Currently Java only has local type inference. Currently Java only has local type inference.
We want to bring type inference for Java to the next level. We want to bring type inference for Java to the next level.
\section{Unify}
We have to formulate the unification algorithm with implication rules.
Those can be directly translated to ASP.
\begin{mathpar}
\inferrule[Subst-L]{
\tv{a} \doteq \type{N} \\
\tv{a} \lessdot \type{T}
}{
\type{N} \lessdot \type{T}
}
\and
\inferrule[Subst-R]{
\tv{a} \doteq \type{N} \\
\type{T} \lessdot \tv{a}
}{
\type{T} \lessdot \type{N}
}
\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}
}{
\emptyset
}
\and
\inferrule[Fail]{
\tv{a} \lessdot \type{T}_1 \\
\tv{a} \lessdot \type{T}_2 \\
\type{T}_1 \nless : \type{T}_2 \\
\type{T}_2 \nless : \type{T}_1
}{
\emptyset
}
\and
\inferrule[Swap]{
\type{T}_1 \doteq \type{T}_2
}{
\type{T}_2 \doteq \type{T}_1
}
\and
\inferrule[Adopt]{
\tv{a} \lessdot \type{T}_1 \\
\tv{a} \lessdot \type{T}_2 \\
\type{T}_1 <: \type{T}_2
}{
\type{T}_1 \lessdot \type{T}_2
}
\and
\inferrule[Subst-Param]{
\tv{a} \doteq \type{N} \\
\tv{a} = \type{T}_i \\
\exptype{C}{\type{T}_1 \ldots \type{T}_n} <: \type{T} \\
}{
\type{T}_i \doteq \type{N} \\
}
\end{mathpar}
% Subst
% a =. N, a <. T, N <: T
% --------------
% N <. T
% how to proof completeness and termination?
% TODO: how to proof termination?
\section{Completeness}
To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
\end{document} \end{document}