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

Discussion#

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-01 12:32:56 +02:00
parent 0373eb69e8
commit 435b3ed07b
1 changed files with 25 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
aspUnify.tex
View File

@ -187,17 +187,17 @@ as an ASP program and see how well it handles our type unification problem.
\section{Subtyping} \section{Subtyping}
\begin{mathpar} \begin{mathpar}
\inferrule[Refl]{}{ \inferrule[S-Refl]{}{
\type{T} <: \type{T} \type{T} <: \type{T}
} }
\and \and
\inferrule[Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{ \inferrule[S-Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
\type{T}_1 <: \type{T}_3 \type{T}_1 <: \type{T}_3
} }
\and \and
\inferrule[Var]{}{\type{A} <: \Delta(\type{A})} \inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
\and \and
\inferrule[Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{ \inferrule[S-Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N} \exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
} }
\end{mathpar} \end{mathpar}
@ -617,6 +617,27 @@ and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
And more text. And more text.
\end{proof} \end{proof}
\section{Discussion}
% We cannot use Datalog, because it cannot solve NP-Hard problems.
% See: E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov. Complexity and Expressive Power of Logic Programming.
% ACM Computing Surveys, 33(3):374–425, 2001. Available at
% http://www.kr.tuwien.ac.at/staff/eiter/et-archive/
% Source: https://www.cs.ox.ac.uk/files/1018/gglecture7.pdf
It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
It is not possible to implement a type inference algorithm for Java in ASP, because the grounding process will not terminate
\cite{kaufmann2016grounding}.
\section{Outcome and Conclusion}
ASP handles Or-Constraints surprisingly well.
\section{Future Work}
% Benchmarks
% Integrating the ASP Unify implementation into existing Java-TX Compiler
% Checking how many programs are abel to be build without wildcards
\bibliographystyle{eptcs} \bibliographystyle{eptcs}
\bibliography{martin} \bibliography{martin}