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

Finished version for symposium submission

Browse Source
This commit is contained in:
JanUlrich 2024-07-22 15:34:00 +02:00
parent ac3e5651e3
commit c9c531741e
1 changed files with 18 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
aspUnify.tex
View File

@ -71,7 +71,6 @@ exposing promising results.
Another advantage is that the specification of the algorithm can be translated one on one to ASP code Another advantage is that the specification of the algorithm can be translated one on one to ASP code
leading to less errors in the respective implementation. leading to less errors in the respective implementation.
Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types. Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types.
%TODO: Is this correct?
\end{abstract} \end{abstract}
% %
% %
@ -200,8 +199,8 @@ get either the type \texttt{C1} or \texttt{C2}.
A first prototype implementation of the \unify{} algorithm simply created the cartesian product of all Or-Constraints, A first prototype implementation of the \unify{} algorithm simply created the cartesian product of all Or-Constraints,
16 possibilities in this example, and iteratively tried all of them. 16 possibilities in this example, and iteratively tried all of them.
This leads to a exponential runtime increase with every added overloaded method call. This leads to a exponential runtime increase with every added overloaded method call.
Eventhough the current algorithm is equipped with various optimizations as presented in \cite{plue181} and \cite{plue231}, Eventhough the current algorithm is equipped with various optimizations as presented in \cite{plue181} and \cite{plue231}
there is still a runtime increas sensible when dealing with many Or-Constraints. there are still runtime issues when dealing with many Or-Constraints.
Our global type inference algorithm should construct type solutions in real time. Our global type inference algorithm should construct type solutions in real time.
Then it can effectively used as a Java compiler which can deal with large inputs of untyped Java code. Then it can effectively used as a Java compiler which can deal with large inputs of untyped Java code.
@ -273,8 +272,8 @@ holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
\subsection{Unification Algorithm}\label{sec:implicationRules} \subsection{Unification Algorithm}\label{sec:implicationRules}
The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints. %The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
The need to have an upper bound to every type placeholder. %The need to have an upper bound to every type placeholder.
All the implication rules depicted in this chapter can be translated to ASP statements All the implication rules depicted in this chapter can be translated to ASP statements
described in chapter \ref{sec:translation}. described in chapter \ref{sec:translation}.
@ -484,8 +483,13 @@ Fail:
The algorithm terminates if every type placeholder in the input constraint set has an assigned type. The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
\section{ASP Encoding}\label{sec:translation} \section{ASP Encoding}\label{sec:translation}
Answer Set Programming is a declarative way of formulating search problems.
ASP statements consist of a head and a body separated by a implication operator \textquotedbl{}\texttt{:-}\textquotedbl{}:
\texttt{head :- body}.
This statement is interpreted as an implication rule.
If the premises in the body are satisfied the facts stated in the head are deducted.
\newcommand{\aspify}{\nabla} \newcommand{\aspify}{\nabla}
The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program The implication rules defined in chapter \ref{sec:implicationRules} are formulated in a way that can be translated to an ASP program
(see figure \ref{fig:aspTransformationRules}). (see figure \ref{fig:aspTransformationRules}).
% \begin{tabular}{l | r} % \begin{tabular}{l | r}
@ -505,7 +509,8 @@ The implication rules defined in chapter \ref{sec:implicationRules} can be trans
c_1, c_2 c_1, c_2
}{ }{
c c
}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2) }\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2) \\
c_1 \ || \ c_2 =& \texttt{orcons}(\aspify(c_1), \aspify(c_2))
\end{align*} \end{align*}
\caption{Transformation to ASP code}\label{fig:aspTransformationRules} \caption{Transformation to ASP code}\label{fig:aspTransformationRules}
\end{figure} \end{figure}
@ -523,7 +528,13 @@ Capital letters like \texttt{X} are variables in ASP and the former statement ca
literal like \texttt{subtype(type("C", params(tph("a"))))} to imply the literal literal like \texttt{subtype(type("C", params(tph("a"))))} to imply the literal
\texttt{subtype(type("C", params(tph("a"))), type("D", params(tph("a"))))}. \texttt{subtype(type("C", params(tph("a"))), type("D", params(tph("a"))))}.
The vital part is the generation of the cartesian product of the Or-Constraints.\\
{{\texttt{subcons(A,B); orCons(C,D) :- orCons(subcons(A,B), subcons(C,D)).}}}\\
The operator \textquotedbl{}\texttt{;}\textquotedbl{} tells ASP to consider either the left or the right side.
By supplying multiple Or-Constraints this way the ASP interpreter will consider all combinations, the cartesian product of the or constraints.
The rules implying a failure $\emptyset$ are translated by leaving the head of the asp statement empty.
If the body of such rules is satisfied the algorithm considers the deduction as incorrect.
% \section{Proofs} % \section{Proofs}
% \begin{lemma}{Substitution:} % \begin{lemma}{Substitution:}
% For every $\tv{a} \doteq \type{T}$ and every constraint $c$, % For every $\tv{a} \doteq \type{T}$ and every constraint $c$,