Move Slides to a separate Repo

aspUnify.tex

@@ -2,8 +2,9 @@
 % LLNCS macro package for Springer Computer Science proceedings;
 % Version 2.21 of 2022/01/12
 %
-\documentclass[runningheads]{llncs}
-%
+\documentclass[submission]{eptcs}
+\providecommand{\event}{Symposium in honor of Peter Thiemann's 60th birthday} % Name of the event you are submitting to
+\usepackage{underscore}
 \usepackage[T1]{fontenc}
 % T1 fonts will be used to generate the final print and online PDFs,
 % so please use T1 fonts in your manuscript whenever possible.
@@ -23,77 +24,232 @@
 \usepackage{mathpartir}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{amsthm}
 \usepackage{enumitem}
+\usepackage{xcolor}
 %\usepackage{amsthm}
 
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}[theorem]{Lemma}
+
+\title{Global Type Inference for Java using Answer Set Programming}
+\author{Andreas Stadelmeier
+    \institute{DHBW\\ Stuttgart}
+    \email{a.stadelmeier@hb.dhbw-stuttgart.de}
+}
+\newcommand{\authorrunning}{Andreas Stadelmeier}
+\newcommand{\titlerunning}{Type Unification with ASP}
+\hypersetup{
+  bookmarksnumbered,
+  pdftitle    = {\titlerunning},
+  pdfauthor   = {\authorrunning},
+  pdfsubject  = {Global Type Inference for Java},               % Consider adding a more appropriate subject or description
+  pdfkeywords = {typeinference, java, sat solving, answer set programming} % Uncomment and enter keywords specific to your paper
+}
+
 \begin{document}
 %
-\title{Global Type Inference for Java using SAT Solvers}
-%
-%\titlerunning{Abbreviated paper title}
-% If the paper title is too long for the running head, you can set
-% an abbreviated paper title here
-%
-\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
-Second Author\inst{2,3}\orcidID{1111-2222-3333-4444} \and
-Third Author\inst{3}\orcidID{2222--3333-4444-5555}}
-%
-\authorrunning{F. Author et al.}
 % First names are abbreviated in the running head.
 % If there are more than two authors, 'et al.' is used.
 %
-\institute{Princeton University, Princeton NJ 08544, USA \and
-Springer Heidelberg, Tiergartenstr. 17, 69121 Heidelberg, Germany
-\email{lncs@springer.com}\\
-\url{http://www.springer.com/gp/computer-science/lncs} \and
-ABC Institute, Rupert-Karls-University Heidelberg, Heidelberg, Germany\\
-\email{\{abc,lncs\}@uni-heidelberg.de}}
 %
 \maketitle              % typeset the header of the contribution
 %
 \begin{abstract}
-The abstract should briefly summarize the contents of the paper in
-150--250 words.
-
-\keywords{First keyword  \and Second keyword \and Another keyword.}
+Global type inference for Java is able to compute correct types for an input program
+which has no type annotations at all, but turns out to be NP-hard.
+Former implementations of the algorithm therefore struggled with bad runtime performance.
+In this paper we translate the type inference algorithm for Featherweight Generic Java to an
+Answer Set Program.
+Answer Set Programming (ASP) promises to solve complex computational search problems
+as long as they are finite domain.
+This paper shows that it is possible to implement global type inference for Featherweight Generic Java (FGJ) as an ASP program.
+Afterwards we compared the ASP implementation with our own implementation in Java
+exposing promising results.
+% We also show soundness, completeness and termination for our ASP implementation.
+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.
+Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types.
 \end{abstract}
 %
 %
 %
-\section{Type Inference}
-Every major typed programming language uses some form of type inference.
-Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
-Type inference adds alot of value to a programming language.
-\begin{itemize}
-\item Code is more readable.
-\item Type inference usually does a better job at finding types than a programmer.
-\item Type inference can use types that are not denotable by the programmer.
-\item Better reusability.
-\item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
-\end{itemize}
+\section{Global Type Inference}
+% Every major typed programming language uses some form of type inference.
+% Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
+% Type inference adds alot of value to a programming language.
+% \begin{itemize}
+% \item Code is more readable.
+% \item Type inference usually does a better job at finding types than a programmer.
+% \item Type inference can use types that are not denotable by the programmer.
+% \item Better reusability.
+% \item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
+% \end{itemize}
 
-Java has adopted more and more type inference features over time.
-%TODO: list type inference additions
-Currently Java only has local type inference.
-We want to bring type inference for Java to the next level.
+% Java has adopted more and more type inference features over time.
+% %TODO: list type inference additions
+% Currently Java only has local type inference.
+% We want to bring type inference for Java to the next level.
 
-\section{Subtyping}
+Java is a strictly typed programming language.
+The current versions come with a local type inference feature that allows the programmer to omit
+type annotations in some places like argument types of lambda expressions for example.
+But methods still have to be fully typed including argument and return types.
+We work at a global type inference algorithm for Java which is able to compute correct types
+for a Java program with no type annotations at all.
+
+\begin{figure}[h]
+\begin{lstlisting}
+class C1 {
+    C1 self(){
+        return this;
+    }
+}
+class C2 {
+    C2 self(){
+        return this;
+    }
+}
+class Example {
+    untypedMethod(var){
+        return var.self();   //  (*@$\implies \set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$@*)
+    }
+}
+\end{lstlisting}
+\caption{Java program missing type annotations}\label{fig:introExample}
+\end{figure}
+
+A possible input for our algorithm is shonw in figure \ref{fig:introExample}.
+Here the method \texttt{untypedMethod} is missing its argument type for \texttt{var} and its return type.
+Global type inference works in two steps.
+First we generate a set of subtype constraints, which are later unified resulting in a type solution consisting of type unifiers $\sigma$.
+Every missing type is replaced by a type placeholder.
+In this example the type placeholder $\tv{var}$ is a placeholder for the type of the \texttt{var} variable.
+The $\tv{ret}$ placeholder represents the return type of the \texttt{untypedMethod} method.
+Also shown as a comment behind the respective method call.
+There are two types of type constraints.
+A subtype constraint like $\tv{var} \lessdot \type{C1}$ meaning that the unification algorithm has to find
+a type replacement for $\tv{var}$ which is a subtype of $\type{C1}$.
+Due to the Java type system being reflexive one possible solution would be $\sigma(\tv{var}) = \type{C1}$.
+A constraint $\tv{var} \doteq \type{C1}$ directly results in $\sigma(\tv{ret}) = \type{C1}$.
+
+Our type inference algorithms for Java are described in a formal manner in
+\cite{MartinUnify}, \cite{TIforGFJ}.
+The first prototype implementation put the focus on a correct implementation rather than
+fast execution times.
+Depending on the input it currently takes upto several minutes or even days to compute all or even one possible type solution.
+To make them usable in practice we now focus on decreasing the runtime to a feasible level.
+
+\section{Motivation}
+The nature of the global type inference algorithm causes the search space of the unification algorithm to
+increase exponentially with every ambiguous method call.
+Java allows overloaded methods causing our type inference algorithm to create so called Or-Constraints.
+This happens if multiple classes implement a method with the same name and the same amount of parameters.
+Given the input program in figure \ref{fig:introExample} we do not know, which method \texttt{self} is meant for the method call
+\texttt{var.self()}, because there is no type annotation for \texttt{var}.
+
+
+%\begin{figure}[h]
+%\begin{minipage}{0.49\textwidth}
+%     \end{minipage}%
+%     \hfill
+%     \begin{minipage}{0.49\textwidth}
+% \begin{lstlisting}[style=constraints]
+% (*@$\tv{var} \lessdot \type{C1} | $@*),
+% (*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
+% \end{lstlisting}
+% \end{minipage}
+%\end{figure}
+
+An Or-Constraint like $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$
+means that either the the constraint set $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }$
+or $\set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$ has to be satisfied.
+If we set the type of \texttt{var} to \texttt{C1}, then the return type of the method will be \texttt{C1} aswell.
+If we set it to \texttt{C2} then also the return type will be \texttt{C2}.
+There are two possibilities therefore the Or-Constraint.
+
+If we chain multiple overloaded method calls together we end up with multiple Or-Constraints.
+The type unification algorithm \unify{} only sees the supplied constraints and has to potentially try all combinations of them.
+This is proven in \cite{TIforGFJ} and is the reason why type inference for Featherweight Generic Java is NP-hard.
+Let's have a look at the following alternation of our example:
+
+\begin{figure}[h]
+\begin{lstlisting}
+    untypedMethod(var){
+        return var.self().self().self().self();
+    }
+\end{lstlisting}
+\caption{Stacked ambiguous method calls}\label{fig:benchmark}
+\end{figure}
+
+Now there are four chained method calls leading to four Or-Constraints:
+\begin{align*}
+    \set{\tv{var} \lessdot \type{C1}, \tv{r1} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{r1} \doteq \type{C2}} \\
+    \set{\tv{r1} \lessdot \type{C1}, \tv{r2} \doteq \type{C1} }\ ||\ \set{\tv{r1} \lessdot \type{C2}, \tv{r2} \doteq \type{C2}} \\
+    \set{\tv{r2} \lessdot \type{C1}, \tv{r3} \doteq \type{C1} }\ ||\ \set{\tv{r2} \lessdot \type{C2}, \tv{r3} \doteq \type{C2}} \\
+    \set{\tv{r3} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{r3} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}} \\
+\end{align*}
+
+The placeholder $\tv{r1}$ stands for the return type of the first call to \texttt{self} and 
+$\tv{r2}$ for the return type of the second call and so on.
+It is obvious that this constraint set only has two solutions.
+The variable \texttt{var} and the return type of the method aswell as all intermediate placeholders $\tv{r1}-\tv{r3}$
+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,
+16 possibilities in this example, and iteratively tried all of them.
+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}
+there are still runtime issues when dealing with many Or-Constraints.
+
+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.
+Another use case scenario is as an editor plugin which helps a Java programmer by enabling him to write untyped Java code
+and letting our tool insert the missing type statements.
+For both applications a short execution time is vital.
+
+Answer Set programming promises to solve complex search problems in a highly optimized way.
+The idea in this paper is to implement the algorithm presented in \cite{TIforGFJ}
+as an ASP program and see how well it handles our type unification problem.
+
+\section{ASP Implementation}
+
+Our ASP implementation replaces the unification step of the type inference algorithm.
+So the input is a set of constraints $c$ and the output is a set of unifiers $\sigma$.
+An ASP program consists of implication rules and facts.
+Here the facts are the input constraints and the rules are the ones depicted in chapter \ref{sec:implicationRules}.
+After running the resulting program through an interpreter the output
+holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
+
+\begin{figure}[h]
+  \center
+\begin{tabular}{lcll}
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
+    $\type{T} $ & $::=$ & $\tv{a} \mid \type{N}$ & Type placeholder or Type \\
+    $\ntype{N}$ & $::=$ & $\exptype{C}{\ol{T}}$ & Class Type containing type placeholders\\
+    $\gtype{G}$ & $::=$ & $\exptype{C}{\ol{G}}$ & Class Type not containing type placeholders \\
+\end{tabular}
+  \caption{Syntax of types and constraints}
+  \label{fig:syntax-constraints}
+\end{figure}
+
+%\subsection{Subtyping}
+\begin{figure}[h]
 \begin{mathpar}
-\inferrule[Refl]{}{
+\inferrule[S-Refl]{}{
 \type{T} <: \type{T}
 }
 \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
 }
 \and
-\inferrule[Var]{}{\type{A} <: \Delta(\type{A})}
+\inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
 \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}
 }
 \end{mathpar}
-
 \begin{mathpar}
 \inferrule[N-Refl]{}{
 \type{C} << \type{C}
@@ -107,39 +263,39 @@ We want to bring type inference for Java to the next level.
 \type{C} << \type{D}
 }
 \end{mathpar}
+\caption{Subtyping}\label{fig:subtyping}
+\end{figure}
 
-\section{Unify}
-Input: Every type placeholder must have an upper bound.
-Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a 
 
-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.
+%Subtyping has no bounds for generic type parameters.
+% but this is propably not needed
 
-We have to formulate the unification algorithm with implication rules.
-Those can be directly translated to ASP.
+\subsection{Unification Algorithm}\label{sec:implicationRules}
+
+%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.
+
+All the implication rules depicted in this chapter can be translated to ASP statements
+described in chapter \ref{sec:translation}.
+
+\label{sec:implicationRules}
 \begin{mathpar}
-\inferrule[Subst]{
-    \tv{a} \doteq \type{N}
-}{
-    \tv{a} \mapsto \type{N}
-}
-\and
 \inferrule[Subst-L]{
-    \tv{a} \mapsto \type{T}_1 \\
+    \tv{a} \doteq \type{T}_1 \\
     \tv{a} \lessdot \type{T}_2
 }{
     \type{T}_1 \lessdot \type{T}_2
 }
 \and
 \inferrule[Subst-R]{
-    \tv{a} \mapsto \type{T}_1 \\
+    \tv{a} \doteq \type{T}_1 \\
     \type{T}_2 \lessdot \tv{a} 
 }{
     \type{T}_2 \lessdot \type{T}_1
 }
 \and
 \inferrule[Subst-Equal]{
-    \tv{a} \mapsto \type{T}_1 \\
+    \tv{a} \doteq \type{T}_1 \\
     \tv{a} \doteq \type{T}_2 
 }{
     \type{T}_1 \doteq \type{T}_2
@@ -157,13 +313,26 @@ Those can be directly translated to ASP.
     \type{T}_i \doteq \type{T}_i 
 }
 \and
+\inferrule[Unfold']{
+    \tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n}
+}{
+    \type{T}_i \doteq \type{T}_i
+}
+\and
 \inferrule[Subst-Param]{
-    \tv{a} \mapsto \type{S} \\
-    \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
+    \type{T}' \doteq \type{S} \\
+    \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\
 }{
     \type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
 }
 \and
+\inferrule[Subst-Param']{
+    \type{T}' \doteq \type{S} \\
+    \tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\
+}{
+    \tv{b} \lessdot \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
+}
+\and
 \inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
 \and
 \inferrule[Match]{
@@ -171,7 +340,7 @@ Those can be directly translated to ASP.
     \tv{a} \lessdot \type{N}_2 \\
     \type{N}_1 << \type{N}_2
 }{
-    \type{T}_1 \lessdot \type{T}_2
+    \type{N}_1 \lessdot \type{N}_2
 }
 \and
 \inferrule[Adopt]{
@@ -206,10 +375,10 @@ Those can be directly translated to ASP.
 \begin{mathpar}
     \text{Apply only once per constraint:}\quad 
     \inferrule[Super]{
-        \type{T} \lessdot \tv{a}\\
-        \type{T} <: \type{N} 
+        \type{N} \lessdot \tv{a}\\
+        \type{N} <: \type{N}' 
     }{
-        \tv{a} \doteq \type{N}
+        \tv{a} \doteq \type{N}'
     } 
 \end{mathpar}
 
@@ -236,40 +405,11 @@ 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{G}
 }{
     \sigma(\tv{a}) = \type{G}
 }
-% \and
-% \inferrule[Generic]{
-%     \tv{a} \lessdot \type{N} %, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
-%     \\
-%     \text{not}\ \tv{a} \doteq \type{N}'
-% }{
-% \tv{a} \mapsto \type{A}
-% }
-% \and
-% \inferrule[Solution-Sub]{
-%     \tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
-%     \forall i: \type{C_m} << \type{C_i} \\
-%     \text{not}\ \tv{a} \doteq \type{N}
-% }{
-%     \Delta(\type{A}) = \exptype{C_m}{\ol{T_m}} \\ \sigma(\tv{a}) = \type{A}
-% }
-% \and
-% \inferrule[Solution-Gen]{
-%     \tv{a} \lessdot \type{G}_1, \ldots, \tv{a} \lessdot \type{G}_n \\
-%     \forall i: \type{G} <: \type{G}_i \\
-% }{
-%     \Delta(\type{A}) = \type{G} \\ \sigma(\tv{a}) = \type{A}
-% }
 \and
 \inferrule[Solution-Gen]{
     \tv{a} \lessdot \type{C}_1, \ldots, \tv{a} \lessdot \type{C}_n \\
@@ -277,6 +417,22 @@ Result:
 }{
     \tv{a} \doteq \type{C}_m
 }
+% \and
+% \inferrule[Solution-Gen]{
+%     \tv{a} \lessdot \type{C}\\
+%     \sigma(\tv{a}) = \emptyset 
+% }{
+%     \tv{a} \doteq \type{A} \\ \sigma'(\tv{a}) = \type{A}
+% }
+% \and
+% \inferrule[Solution-Gen]{
+%     \tv{a} \lessdot \type{G} \\
+%     \tv{a} \lessdot \type{G}_1, \ldots, \tv{a} \lessdot \type{G}_n \\
+%     \forall i: \type{G} << \type{G}_i \\
+%     \sigma'(\tv{a}) = \type{A}
+% }{
+%     \Delta(\type{A}) = \type{G}
+% }
 \end{mathpar}
 
 Fail:
@@ -296,6 +452,13 @@ Fail:
     \emptyset
 }
 \and
+\inferrule[Fail-Generic]{
+    \type{X} \doteq \type{T}\\
+    \type{X} \neq \type{T}
+}{
+    \emptyset
+}
+\and
 \inferrule[Fail-Sigma]{
     \tv{a} \doteq \type{N} \\
     \tv{a} \in \type{N}
@@ -325,130 +488,248 @@ Fail:
 
 The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
 
-\section{ASP Encoding}
-\begin{tabular}{l | r}
-$\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
-\end{tabular}
+\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}
+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}).
 
-\section{Completeness}
-To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
+% \begin{tabular}{l | r}
+%     $\tv{a}$ & \texttt{tph("a")}\\
+%     $\exptype{C}{}$ & \texttt{type("C", null)}\\
+%     $\exptype{C}{\ol{X}}$ & \texttt{type("C", params(\ldots))}\\
+% \end{tabular}
 
-Completeness -> we never exclude a solution
-Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
-Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
-Proof:
-%Induction over every possible constraint variation:
-a =. T -> induction start
-a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
-in latter case: a <. T, a <. T'
+\begin{figure}[h]
+\begin{align*}
+   \aspify(\tv{a}) =& \texttt{tph("a")}\\
+   \exptype{C}{} =& \texttt{type("C", null)}\\
+   \exptype{C}{\type{T}_1, \type{T}_2, \ldots} =& \texttt{type("C", params(}\aspify(\type{T}_1), \aspify(\type{T}_1), \ldots\texttt{))}\\
+   \aspify(\type{T} \doteq \type{T}') =& \texttt{equalcons}(\aspify(\type{T}), \aspify(\type{T}')) \\
+   \aspify(\type{T} \lessdot \type{T}') =& \texttt{subcons}(\aspify(\type{T}), \aspify(\type{T}')) \\
+   \aspify{} \left(\inferrule{
+    c_1, c_2
+}{
+    c
+}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2) \\
+c_1 \ || \ c_2 =& \texttt{orcons}(\aspify(c_1), \aspify(c_2))
+\end{align*}
+\caption{Transformation to ASP code}\label{fig:aspTransformationRules}
+\end{figure}
 
-Proof that every type can be replaced by a Type Placeholder.
-% Whats with a =. T, can T be replaced by a Type Placeholder?
-% What is our finish condition? a <. T constraints stay, a =. b constraints stay.
-% Algorithm does not fail -> \emptyset if a solution exists
-% Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
-% by: a <. T -> a =.T
-%     a =. b, b =. T -> use the solution generation from other paper
-% TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
+%The $\aspify{}$ function converts our formal specification of the algorithm to ASP code.
 
-Soundness -> we never make a wrong implication
-%$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
-If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
-constraints in the original constraint set and
-there exists a typing for the remaining type placeholders 
-so that the constraint set is satisfied.
+This also has to be done for the subtype rules in figure \ref{fig:subtyping}.
+There the S-Class rule needs special handling because it contains a substitution.
+It has to be encoded using variables.
+Given a extends relation $\texttt{class}\ \exptype{C}{\type{X}} \triangleleft \exptype{D}{\type{X}}$
+we generate the ASP code:\\
+{\small{\texttt{subtype(type("C", params(X)), type("D", params(X))) :- subtype(type("C", params(X))).}}}
 
-\begin{theorem}{Soundness}\label{lemma:soundness}
-if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
-then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
-\end{theorem}
+Capital letters like \texttt{X} are variables in ASP and the former statement causes any
+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"))))}.
 
-\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
-\newcommand*\ncasesmakelabel[1]{Case #1}
+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.
 
-\newenvironment{subproof}
-  {\def\proofname{Subproof}%
-   \def\qedsymbol{$\triangleleft$}%
-   \proof}
-  {\endproof}
-Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
-\begin{proof}
-  \begin{enumerate}[ncases]
-    \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
-        Solution-Sub
-    Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
-    \item $\tv{a} \doteq \type{N}$.
-    Solution
-    \item $\tv{a} \lessdot \tv{b}$.
-    There must be a $\tv{a} \lessdot \type{N}$
-    \begin{subproof}
-    $\sigma(\tv{a}) = \type{Object}$, 
-    $\sigma(\tv{b}) = \type{Object}$.
-    \end{subproof}
-    \item $\type{N} \lessdot \tv{a}$.
-    \begin{subproof}
-    $2$
-    \end{subproof}
-  \end{enumerate}
-  And more text.
-\end{proof}
+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}
+% \begin{lemma}{Substitution:}
+% For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
+% there also exists a constraint $[\type{T}/\tv{a}]c$.
 
-\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
+% \noindent
+% \normalfont
+% This lemma proofs that equal constraints lead to a substitution in every other constraint.
+% For exmaple $\tv{b} \doteq \type{String}$ and $\tv{b} \lessdot \exptype{Comparable}{\tv{b}}$
+% lead to a constraint $\type{String} \lessdot \exptype{Comparable}{\type{String}}$
+% \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.
-\end{lemma}
-Proof:
-Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
-Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
+% \section{Termination}
 
-The Solution-Sub rule is always correct.
+% The amount of different constraints is limited by the maximum amount of encapsulated generics.
+% The only part that is able to add an additional nesting is the Subst-Param rule.
+% Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
+% another layer of nesting but it also removes one type placeholder.
 
-Proof:
+% There must be one substitution that does not add another type placeholder.
+% Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
 
-\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}
+% The Subst-Param rule can only be applied a finite number of times.
+% Due to the substitution lemma and the Sigma-Fail rule the Subst-Param rule can only be applied once per type placeholder.
 
-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
+% The Subst-Param rule can only be applied once per type placeholder.
+% If $\type{T} \doteq \exptype{C}{\tv{a}}$ is substituted to $\type{T} \doteq \exptype{C}{\type{N}}$
+% then there is no $\tv{a} \in \type{N}$.
 
-\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}$.
-\end{theorem}
-%Problem: We do not support multiple inheritance
-\begin{proof}
-  \begin{enumerate}[ncases]
-    \item $\tv{a} \lessdot \type{N}$.
-        Solution-Sub
-    \item $\tv{a} \doteq \type{N}$.
-    Solution
-    \item $\tv{a} \lessdot \tv{b}$.
-    There must be a $\tv{a} \lessdot \type{N}$
-    \begin{subproof}
-    $\sigma(\tv{a}) = \type{Object}$, 
-    $\sigma(\tv{b}) = \type{Object}$.
-    \end{subproof}
-    \item $\type{N} \lessdot \tv{a}$.
-    \begin{subproof}
-    $2$
-    \end{subproof}
-  \end{enumerate}
-  And more text.
-\end{proof}
+% \section{Completeness}
+% To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
+
+% Completeness -> we never exclude a solution
+% Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
+% Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
+% Proof:
+% %Induction over every possible constraint variation:
+% a =. T -> induction start
+% a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
+% in latter case: a <. T, a <. T'
+
+% Proof that every type can be replaced by a Type Placeholder.
+% % Whats with a =. T, can T be replaced by a Type Placeholder?
+% % What is our finish condition? a <. T constraints stay, a =. b constraints stay.
+% % Algorithm does not fail -> \emptyset if a solution exists
+% % Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
+% % by: a <. T -> a =.T
+% %     a =. b, b =. T -> use the solution generation from other paper
+% % TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
+
+% Soundness -> we never make a wrong implication
+% %$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
+% If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
+% constraints in the original constraint set and
+% there exists a typing for the remaining type placeholders 
+% so that the constraint set is satisfied.
+
+% \begin{theorem}{Soundness}\label{lemma:soundness}
+% if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
+% then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
+% \end{theorem}
+
+% \SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
+% \newcommand*\ncasesmakelabel[1]{Case #1}
+
+% \newenvironment{subproof}
+%   {\def\proofname{Subproof}%
+%    \def\qedsymbol{$\triangleleft$}%
+%    \proof}
+%   {\endproof}
+% Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
+% \begin{proof}
+%   \begin{enumerate}[ncases]
+%     \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
+%         Solution-Sub
+%     Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
+%     \item $\tv{a} \doteq \type{N}$.
+%     Solution
+%     \item $\tv{a} \lessdot \tv{b}$.
+%     There must be a $\tv{a} \lessdot \type{N}$
+%     \begin{subproof}
+%     $\sigma(\tv{a}) = \type{Object}$, 
+%     $\sigma(\tv{b}) = \type{Object}$.
+%     \end{subproof}
+%     \item $\type{N} \lessdot \tv{a}$.
+%     \begin{subproof}
+%     $2$
+%     \end{subproof}
+%   \end{enumerate}
+%   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.
+% \end{lemma}
+% Proof:
+% Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
+% Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
+
+% 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}$.
+% \end{theorem}
+% %Problem: We do not support multiple inheritance
+% \begin{proof}
+%   \begin{enumerate}[ncases]
+%     \item $\tv{a} \lessdot \type{N}$.
+%         Solution-Sub
+%     \item $\tv{a} \doteq \type{N}$.
+%     Solution
+%     \item $\tv{a} \lessdot \tv{b}$.
+%     There must be a $\tv{a} \lessdot \type{N}$
+%     \begin{subproof}
+%     $\sigma(\tv{a}) = \type{Object}$, 
+%     $\sigma(\tv{b}) = \type{Object}$.
+%     \end{subproof}
+%     \item $\type{N} \lessdot \tv{a}$.
+%     \begin{subproof}
+%     $2$
+%     \end{subproof}
+%   \end{enumerate}
+%   And more text.
+% \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
+
+
+\section{Outcome and Conclusion}
+ASP handles Or-Constraints surprisingly well.
+We tested our ASP implementation of the unification algorithm with the constraints originating from the program in
+figure \ref{fig:benchmark}.
+We compared it with the current implementation of the Unification algorithm in Java
+\footnote{\url{https://gitea.hb.dhbw-stuttgart.de/JavaTX/JavaCompilerCore}}.
+We increased the complexity by adding more stacked method calls up to ten stacked calls and the interpreter clingo \footnote{\url{https://potassco.org/clingo/}}
+was still able to handle it easily and finish computation in under 50 milliseconds.
+By contrast our Java implementation already takes multiple seconds processing time for the same input.
+
+We are using this example for a fair comparision between the two implementations because it does not include generic type parameters causing the unification algorithm
+not to consider wildcard types.
+The Java implementation also supports Java wildcard types whereas the ASP implementation does not.
+%It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
+It is unfortunately not possible to implement the unification algorithm including wildcard support with Answer Set Programming.
+The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
+The grounding process of the ASP interpreter clingo would not terminate if the problem is turing complete
+\cite{kaufmann2016grounding}.
+The Java implementation is still able to spawn atleast one solution in most cases and only never terminates for specific inputs,
+whereas the ASP program never terminates as soon as wildcards are involved.
+
+
+%\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}
+\bibliography{martin}
 
 \end{document}

eptcs.cls

@@ -0,0 +1,263 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{eptcs}[2022/05/20 v1.7]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%                             options                            %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newif\ifadraft
+\newif\ifsubmission
+\newif\ifpreliminary
+\newif\ifcopyright
+\newif\ifpublicdomain
+\newif\ifcreativecommons
+\newif\ifnoderivs
+\newif\ifsharealike
+\newif\ifnoncommercial
+\adraftfalse
+\submissionfalse
+\preliminaryfalse
+\copyrightfalse
+\publicdomainfalse
+\creativecommonsfalse
+\noderivsfalse
+\sharealikefalse
+\noncommercialfalse
+\DeclareOption{adraft}{\adrafttrue}
+\DeclareOption{submission}{\submissiontrue}
+\DeclareOption{preliminary}{\preliminarytrue}
+\DeclareOption{copyright}{\copyrighttrue}
+\DeclareOption{publicdomain}{\publicdomaintrue}
+\DeclareOption{creativecommons}{\creativecommonstrue}
+\DeclareOption{noderivs}{\noderivstrue}
+\DeclareOption{noncommercial}{\noncommercialtrue}
+\DeclareOption{sharealike}{\sharealiketrue}
+\ProcessOptions\relax
+
+\LoadClass[letterpaper,11pt,twoside]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%   On US letter paper the margins (left-top-right-bottom) are       %%
+%%              2.795cm - 1.23cm - 2.795cm - 3.46cm                   %%
+%%   Note: When \topmargin would be 0, the real top margin would be   %%
+%%   (72-25-12=35pt) + 1pt (unused portion of head) = .5in = 1.27cm.  %%
+%%   The bottom margin is   11in - 1in + 0.04cm - 623/72in = 3.46cm.  %%
+%%   On the first page the bottom margin contains various footers.    %%
+%%   When translating from US letter to A4 paper, without scaling, by %%
+%%   leaving the centre of the paper invariant (as is possible when   %%
+%%   printing the paper with acroread), the resulting A4 margins are  %%
+%%                2.5cm - 2.11cm - 2.5cm - 4.34cm                     %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\textwidth              16cm             % A4 width is 21cm            %
+\textheight             623.01pt         % 46 lines exactly = 21.98cm  %
+\oddsidemargin          -0.04cm          % +1 inch = 2.5cm             %
+\evensidemargin         -0.04cm          % +1 inch = 2.5cm             %
+\topmargin              -0.04cm          % +1 inch = 2.5cm             %
+\advance\topmargin-\headheight           % 12pt                        %
+\advance\topmargin-\headsep              % 25pt                        %
+\marginparwidth          45pt            % leaves 15pt from A4 edge    %
+\advance\evensidemargin  .295cm          % centre w.r.t. letter paper  %
+\advance\oddsidemargin   .295cm          % centre w.r.t. letter paper  %
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%                  load eptcsdata when available                 %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\IfFileExists{eptcsdata.tex}{\input{eptcsdata}}{}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Pagestyle and titlepage      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\pagestyle{myheadings}
+\renewcommand\pagestyle[1]{}             % ignore further \pagestyles
+
+\renewcommand\maketitle{\par
+  \begingroup
+    \providecommand{\event}{}
+    \ifadraft
+      \providecommand{\publicationstatus}{\Large DRAFT\quad\today}
+    \else\ifsubmission
+      \providecommand{\publicationstatus}{Submitted to:\\
+      \event}
+    \else\ifpreliminary
+      \providecommand{\publicationstatus}{Preliminary Report. Final version to appear in:\\
+      \event}
+    \else
+      \providecommand{\publicationstatus}{To appear in EPTCS.}
+    \fi\fi\fi
+    \providecommand{\titlerunning}{Please define {\ttfamily $\backslash$titlerunning}}
+    \providecommand{\authorrunning}{Please define {\ttfamily $\backslash$authorrunning}}
+    \providecommand{\copyrightholders}{\authorrunning}
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \def\@makefnmark{\rlap{\@textsuperscript{\normalfont\@thefnmark}}}%
+    \long\def\@makefntext##1{\parindent 1em\noindent
+            \hb@xt@1.8em{%
+                \hss\@textsuperscript{\normalfont\@thefnmark}}##1}%
+    \newpage
+    \global\@topnum\z@   % Prevents figures from going at top of page.
+    \@maketitle
+    \thispagestyle{empty}\@thanks
+  \endgroup
+  \setcounter{footnote}{0}%
+  \label{FirstPage}
+  \global\let\thanks\relax
+  \global\let\maketitle\relax
+  \global\let\@maketitle\relax
+  \global\let\@thanks\@empty
+  \global\let\@author\@empty
+  \global\let\@date\@empty
+  \global\let\@title\@empty
+  \global\let\title\relax
+  \global\let\author\relax
+  \global\let\date\relax
+  \global\let\and\relax
+}
+\def\@maketitle{%                       adapted from article.cls
+  \newpage
+\noindent
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\begin{tabular}{@{}l}
+\publicationstatus
+\end{tabular}}
+\hfill\vspace{-1em}
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\makebox[0pt][r]{
+\begin{tabular}{l@{}}
+\ifpublicdomain
+  This work is \href{https://creativecommons.org/publicdomain/zero/1.0/}
+  {dedicated to the public domain}.
+\else
+  \ifcopyright
+    \copyright~\copyrightholders\\
+  \fi
+  \ifcreativecommons
+    This work is licensed under the
+    \ifnoncommercial
+      \href{https://creativecommons.org}{Creative Commons}\\
+      \ifnoderivs
+	\href{https://creativecommons.org/licenses/by-nc-nd/4.0/}
+	{Attribution-Noncommercial-No Derivative Works} License.
+      \else\ifsharealike
+	\href{https://creativecommons.org/licenses/by-nc-sa/4.0/}
+	{Attribution-Noncommercial-Share Alike} License.
+      \else
+	\href{https://creativecommons.org/licenses/by-nc/4.0/}
+	{Attribution-Noncommercial} License.
+      \fi\fi
+    \else
+      \ifnoderivs
+        \href{https://creativecommons.org}{Creative Commons}\\
+	\href{https://creativecommons.org/licenses/by-nd/4.0/}
+	{Attribution-No Derivative Works} License.
+      \else\ifsharealike
+        \href{https://creativecommons.org}{Creative Commons}\\
+	\href{https://creativecommons.org/licenses/by-sa/4.0/}
+	{Attribution-Share Alike} License.
+      \else
+        \\\href{https://creativecommons.org}{Creative Commons}
+	\href{https://creativecommons.org/licenses/by/4.0/}
+	{Attribution} License.
+      \fi\fi
+    \fi
+  \fi
+\fi
+\end{tabular}}}
+  \null
+  %\vskip 2em%				a bit of space removed (< 2em)
+  \begin{center}%
+  \let \footnote \thanks
+    {\LARGE\bfseries \@title \par}%		\bf added
+    \vskip 2em%				was: 1.5em
+    {\large
+      \lineskip .5em%
+      \begin{tabular}[t]{c}%
+        \@author
+      \end{tabular}\par}%
+    \vskip 1em%			       \date and extra space removed
+  \end{center}%
+  \par
+  \markboth{\hfill\titlerunning}{\authorrunning\hfill}
+  \vskip .5em}
+
+\AtBeginDocument{
+  \providecommand{\firstpage}{1}
+  \setcounter{firstpage}{\firstpage}
+  \setcounter{page}{\firstpage}
+  \@ifpackageloaded{array}% Contributed by Wolfgang Jeltsch
+    {\newcommand{\IfArrayPackageLoaded}[2]{#1}}
+    {\newcommand{\IfArrayPackageLoaded}[2]{#2}}}
+\newcommand{\institute}[1]{\IfArrayPackageLoaded
+    {\\{\scriptsize\begin{tabular}[t]{@{}>{\footnotesize}c@{}}#1\end{tabular}}}
+    {\\{\scriptsize\begin{tabular}[t]{@{\footnotesize}c@{}}#1\end{tabular}}}}
+\newcommand{\email}[1]{\\{\footnotesize\ttfamily #1}}
+
+\renewenvironment{abstract}{\begin{list}{}%   header removed and noindent
+			{\rightmargin\leftmargin
+			\listparindent 1.5em
+			\parsep 0pt plus 1pt}
+			\small\item}{\end{list}
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\RequirePackage{hyperref} % add hyperlinks
+\RequirePackage{mathptmx} % Pick Times Roman as a base font
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Remember page numbers      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcounter{firstpage}
+\setcounter{firstpage}{1}
+\AtEndDocument{\clearpage
+   \addtocounter{page}{-1}
+   \immediate\write\@auxout{\string
+   \newlabel{LastPage}{{}{\thepage}{}{page.\thepage}{}}}%
+   \newwrite\pages
+   \immediate\openout\pages=\jobname.pag
+   \immediate\write\pages{\arabic{firstpage}-\arabic{page}}
+   \addtocounter{page}{1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Less space in lists      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\@listi{\leftmargin\leftmargini
+            \parsep 2.5\p@ \@plus1.5\p@ \@minus\p@
+            \topsep 5\p@   \@plus2\p@ \@minus5\p@
+            \itemsep2.5\p@ \@plus1.5\p@ \@minus\p@}
+\let\@listI\@listi
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    1\p@ \@plus\p@ \@minus\p@
+              \parsep    1\p@   \@plus\p@  \@minus\p@
+              \itemsep   \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    \z@
+              \parsep    \z@
+              \itemsep   \topsep}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%       References small and with less space between items       %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}\small%              small added
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \@openbib@code
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \sloppy
+      \clubpenalty4000
+      \@clubpenalty \clubpenalty
+      \widowpenalty4000%
+      \sfcode`\.\@m
+		\setlength{\parskip}{0pt}%
+		\setlength{\itemsep}{3pt plus 2pt}% less space between items
+     }
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}

prolog.tex

@@ -7,7 +7,7 @@
   %breaklines=true,
   showstringspaces=false,
   %breakatwhitespace=true,
-  basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
+  basicstyle=\ttfamily, %\footnotesize
   escapeinside={(*@}{@*)},
   captionpos=t,float,abovecaptionskip=-\medskipamount
 }
@@ -22,8 +22,6 @@
   backgroundcolor=\color{red!20}
 }
 
-\newtheorem{recap}[note]{Recap}
-
 \newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
 
 \newcommand{\tifj}{\texttt{TamedFJ}}

reviews.md

@@ -0,0 +1,163 @@
+----------------------- REVIEW 1 ---------------------
+SUBMISSION: 4
+TITLE: Global Type Inference for Java using Answer Set Programming
+AUTHORS: Andreas Stadelmeier
+
+----------- Overall evaluation -----------
+SCORE: 1 (weak accept)
+----- TEXT:
+The paper provides a good overview and introduction to the research topic but needs more specifics and comes across as a careless abridgment of a more comprehensive document.
+
+Initially, the author briefly outlines the primary problem and presents Answer Set Programming (ASP) as a more promising alternative to overcome the obstacles with existing algorithms. The problem is sufficiently motivated in its brevity, and the author pitches the idea behind ASP and its objective, unfortunately, without introducing ASP in detail or presenting any concrete results. The paper, therefore, reads more as motivation and a superficial introduction to the topic.
+
+Some further points:
+
+* The author should have better explained the evaluation rules on page 4, as well as the syntax and semantic domains used. Without a detailed explanation or a look at the (only incidentally) referenced paper ([3] and [6]), the evaluation rules are not self-explanatory.
+* Just adding evaluation rules without further using them makes no sense. The author could have used this space better.
+* Are the evaluation rules on page 4 inline or floating figures? There is no explanation or caption that one could use to reference the image later. Anyways, without use or explanation, all the evaluation rules appear context-free.
+* Knowledge of ASP is also assumed. More information and a better introduction would be desirable.
+* Overall, I would like to see some more concrete results.
+* "Chapter 3.1": The author can omit this sectioning as just one sub-section exists.
+* "Chapters" should probably be called "Sections".
+
+The paper fails to provide concrete results and reads more like a declaration of intent. The evaluation rules are not further used or discussed and seem unrelated to the paper; therefore, they are not helpful.
+
+To summarise. The paper can be seen as motivation and introduction to a research topic. Omitting the evaluation rules in favor of a better introduction to ASP and more detail on the results already obtained would significantly increase the comprehensibility of the paper.
+----------- Reviewer's confidence -----------
+SCORE: 2 ((low))
+
+
+
+----------------------- REVIEW 2 ---------------------
+SUBMISSION: 4
+TITLE: Global Type Inference for Java using Answer Set Programming
+AUTHORS: Andreas Stadelmeier
+
+----------- Overall evaluation -----------
+SCORE: -1 (weak reject)
+----- TEXT:
+Global Type Inference for Java using Answer Set Programming
+
+
+SUMMARY
+
+This work is about an improved implementation of a previously introduced
+global type inference algorithm for a subset of Java. Instead of using a
+standard type inference algorithm that relies on calls to a unification procedure,
+the whole type inference process is mapped to an ASP program.
+Thanks to some magic of ASP, this leads to a significant speed up to infer
+the types of programs.
+The paper presents an example to motivate the issue of type inference for Java.
+Some parts of the unification algorithm are presented plus its translation to ASP.
+The (performance) benefits of ASP are explained in text.
+No empirical measurements are provided.
+
+EVALUATION
+
+This work reminds me of some earlier work that shows how to map algorithm W to
+a logic program. It seems that ASP has an edge over Prolog when it comes
+to search problems that involve "or constraints". Unfortunately, the paper
+is very sketchy (possible to due to space constraints) and leaves many
+questions unanswered (see below for details).
+
+There are various places where the paper needs to be improved.
+I am also missing insights why ASP is "better" (compared to Prolog).
+
+
+DETAILS
+
+p3
+
+ "...construct type solutions in real time"    reasonable time?
+
+p3
+
+"Another use case ..."
+
+To me the most interesting use would case would be type error diagnosis.
+Just as a pointer for future work.
+
+p3
+
+"Our ASP implementation replaces the unification step of the type inference algorithm."
+
+At this point I'm getting lost.
+
+The rules below Figure 4 cover the "unification steps"?
+
+When/how are these rules applied?
+Motivation behind these rules?
+What about rule (Match)? There are no references to T1 and T1 in the premise.
+
+p3
+
+"The algorithm terminates if every type placeholder in the input constraint set has an assigned type."
+
+I couldn't find the entry point to this algorithm.
+Needs a short example.
+
+
+p5, Figure 5.
+
+This seems to be saying turn the whole type inference algorithm into a logic program.
+It seems that ASP has the best computational model to achieve an efficient implementation.
+Would be interesting to have a comparison with Prolog.
+
+p6
+
+"ASP handles Or-Constraints surprisingly well."
+
+I guess Prolog will perform a "naive" search.
+What's the magic? Stable model semantics of ASP?
+----------- Reviewer's confidence -----------
+SCORE: 4 ((high))
+
+
+
+----------------------- REVIEW 3 ---------------------
+SUBMISSION: 4
+TITLE: Global Type Inference for Java using Answer Set Programming
+AUTHORS: Andreas Stadelmeier
+
+----------- Overall evaluation -----------
+SCORE: -2 (reject)
+----- TEXT:
+Summary
+=======
+
+The paper describes an algorithm for global type
+inference in Java based on ASP (answer set programming).
+Essentially, subtyping rules are translated to ASP
+statements, which are then solved. To paper concludes
+that the implementation based on ASP offers much better
+performance than a "traditional" formulation of the
+inference algorithms.
+
+Evaluation
+==========
+
+The results presented in the paper are promising. But the
+article in its current form feels like a preliminary writeup
+and does a bad job in presenting the results. Hence, I suggest
+to reject the paper.
+
+Here are some of the points that definitely need to be improved:
+
+- The introduction does not mention the contributions of the article
+  (I guess that the first section is meant to be the introduction,
+   it is not called liked that.)
+- The algorithm from [6] should be explained at a high-level.
+- The purpose of section 3 is not clear to me. I was expecting
+  that the section would explain figures 3 and 4, but these figures
+  do not come with any explanation.
+- I am missing some kind of introduction to ASP.
+- Why is ASP so much faster? After all it also has to try it all
+  variants in some ways.
+- A discussion of related work is completely missing.
+
+There is still plenty of space that can be used to address the points
+mentioned. (The paper is only 6 pages long.)
+
+The paper also contains several typos, which I do not list explicitly.
+----------- Reviewer's confidence -----------
+SCORE: 4 ((high))