Submission to the Workshop on Answer Set Programming and Other Computing Paradigms 2025

aspUnify.tex

@@ -2,8 +2,13 @@
 % LLNCS macro package for Springer Computer Science proceedings;
 % Version 2.21 of 2022/01/12
 %
-\documentclass[submission]{eptcs}
-\providecommand{\event}{Symposium in honor of Peter Thiemann's 60th birthday} % Name of the event you are submitting to
+
+\documentclass[]{ceurart}
+
+%% This command is for the conference information
+%% CHOOSE the one corresponding to your conference
+\conference{ASPOCP 2024: 17$^{th}$ Workshop on Answer Set Programming and Other Computing Paradigms, October, 2024, Dallas, USA.}
+
 \usepackage{underscore}
 \usepackage[T1]{fontenc}
 % T1 fonts will be used to generate the final print and online PDFs,
@@ -29,33 +34,34 @@
 \usepackage{xcolor}
 %\usepackage{amsthm}
 
+\newcommand{\aspAlgo}[0]{\ensuremath{\Omega}}
 
-\newtheorem{theorem}{Theorem}
-\newtheorem{lemma}[theorem]{Lemma}
+\title{Global Type Inference for Java using ASP}
 
-\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
-}
+\author[1]{Andreas Stadelmeier}[%
+orcid=0009-0007-8414-5977,
+email=andi@paulus.haus,
+%url=http://www. ,
+]
+\address[1]{Duale Hochschule Baden-Württemberg, Stuttgart, Germany}
+%
+
+%% Rights management information.
+%% CC-BY is default license.
+\copyrightyear{2024}
+\copyrightclause{Copyright for this paper by its authors.
+  Use permitted under Creative Commons License Attribution 4.0
+  International (CC BY 4.0).}
+
+
+
+
+
+\sloppy
 
 \begin{document}
-%
-% First names are abbreviated in the running head.
-% If there are more than two authors, 'et al.' is used.
-%
-%
-\maketitle              % typeset the header of the contribution
-%
+
+
 \begin{abstract}
 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.
@@ -73,6 +79,13 @@ 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}
 %
+
+\begin{keywords}
+  typeinference, java, programming languages, answer set programming
+\end{keywords}
+
+\maketitle              % typeset the header of the contribution
+%
 %
 %
 \section{Global Type Inference}
@@ -217,7 +230,7 @@ as an ASP program and see how well it handles our type unification problem.
 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}.
+Here the facts are the input constraints and the rules are the ones depicted in figure \ref{fig:aspUnifyAlgorithm}.
 After running the resulting program through an interpreter the output
 holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
 
@@ -225,16 +238,19 @@ holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
   \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\\
+    $\type{T}, \type{S} $ & $::=$ & $\tv{a} \mid \type{N}$ & Type placeholder or Type \\
+    $\ntype{N}$ & $::=$ & $\exptype{C}{\ol{P}}$ & Class Type containing type placeholders\\
     $\gtype{G}$ & $::=$ & $\exptype{C}{\ol{G}}$ & Class Type not containing type placeholders \\
+    $\type{P}$ & $::=$ & $\tv{a} \mid \gtype{G}$ & Well-Formed Parameter \\
 \end{tabular}
   \caption{Syntax of types and constraints}
   \label{fig:syntax-constraints}
 \end{figure}
 
-%\subsection{Subtyping}
-\begin{figure}[h]
+\begin{figure}
+\fbox{
+\begin{minipage}{\textwidth}
+\textbf{Subtyping:}
 \begin{mathpar}
 \inferrule[S-Refl]{}{
 \type{T} <: \type{T}
@@ -244,39 +260,26 @@ holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
 \type{T}_1 <: \type{T}_3
 }
 \and
-\inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
-\and
+% \inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
+% \and
 \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}
-}
-\and
-\inferrule[N-Trans]{\type{C}_1 << \type{C}_2 \\ \type{C}_2 << \type{C}_3}{
-\type{C}_1 << \type{C}_3
-}
-\and
-\inferrule[N-Class]{\texttt{class}\ \exptype{C}{\ldots} \triangleleft \exptype{D}{\ldots}}{
-\type{C} << \type{D}
-}
-\end{mathpar}
-\caption{Subtyping}\label{fig:subtyping}
-\end{figure}
-
-
-%Subtyping has no bounds for generic type parameters.
-% but this is propably not needed
-
-\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}.
+% \begin{mathpar}
+% \inferrule[N-Refl]{}{
+% \type{C} << \type{C}
+% }
+% \and
+% \inferrule[N-Trans]{\type{C}_1 << \type{C}_2 \\ \type{C}_2 << \type{C}_3}{
+% \type{C}_1 << \type{C}_3
+% }
+% \and
+% \inferrule[N-Class]{\texttt{class}\ \exptype{C}{\ldots} \triangleleft \exptype{D}{\ldots}}{
+% \type{C} << \type{D}
+% }
+% \end{mathpar}
+\textbf{Unify:}
 
 \label{sec:implicationRules}
 \begin{mathpar}
@@ -307,49 +310,62 @@ described in chapter \ref{sec:translation}.
     \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[Unfold']{
-    \tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n}
-}{
-    \type{T}_i \doteq \type{T}_i
-}
-\and
+% \inferrule[Unfold]{
+%     \type{T} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} 
+% }{
+%     \type{T}_i \doteq \type{T}_i 
+% }
+% \and
+% \inferrule[Unfold-Right]{
+%     \type{T} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n}
+% }{
+%     \type{T}_i \doteq \type{T}_i
+% }
+% \and
+% \inferrule[Unfold-Left]{
+%     \exptype{C}{\type{T}_1 \ldots \type{T}_n} \lessdot \type{T}
+% }{
+%     \type{T}_i \doteq \type{T}_i
+% }
+% \and
 \inferrule[Subst-Param]{
-    \type{T}' \doteq \type{S} \\
-    \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\
+    \tv{a} \doteq \type{G} \\
+    \type{T} \doteq \exptype{C}{\type{P}_1 \ldots, \tv{a}, \ldots \type{P}_n} \\
 }{
-    \type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
+    \type{T} \doteq \exptype{C}{\type{P}_1, \ldots \type{G}, \ldots \type{P}_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} \\
+\inferrule[Subst-Param-Right]{
+    \tv{a} \doteq \type{G} \\
+    \tv{b} \lessdot \exptype{C}{\type{P}_1 \ldots, \tv{a}, \ldots \type{P}_n} \\
 }{
-    \tv{b} \lessdot \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
+    \tv{b} \lessdot \exptype{C}{\type{P}_1, \ldots \type{G}, \ldots \type{P}_n}
+}
+\and
+\inferrule[Subst-Param-Left]{
+    \tv{a} \doteq \type{G} \\
+    \exptype{C}{\type{P}_1 \ldots, \tv{a}, \ldots \type{P}_n} \lessdot \tv{b} \\
+}{
+    \exptype{C}{\type{P}_1, \ldots \type{G}, \ldots \type{P}_n} \lessdot \tv{b}
 }
 \and
 \inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
-\and
-\inferrule[Match]{
-    \tv{a} \lessdot \type{N}_1 \\
-    \tv{a} \lessdot \type{N}_2 \\
-    \type{N}_1 << \type{N}_2
-}{
-    \type{N}_1 \lessdot \type{N}_2
-}
-\and
-\inferrule[Adopt]{
-    \tv{a} \lessdot \tv{b} \\
-    \tv{b} \lessdot \type{T}
-}{
-    \tv{a} \lessdot \type{T}
-}
-\and
+% \and
+% \inferrule[Match]{
+%     \tv{a} \lessdot \type{N}_1 \\
+%     \tv{a} \lessdot \type{N}_2 \\
+%     \type{N}_1 << \type{N}_2
+% }{
+%     \type{N}_1 \lessdot \type{N}_2
+% }
+% \and
+% \inferrule[Adopt]{
+%     \tv{a} \lessdot \tv{b} \\
+%     \tv{b} \lessdot \type{T}
+% }{
+%     \tv{a} \lessdot \type{T}
+% }
+% \and
 % \inferrule[Subst-Param]{
 %     \tv{a} \doteq \type{N} \\
 %     \tv{a} = \type{T}_i \\
@@ -359,51 +375,27 @@ described in chapter \ref{sec:translation}.
 % }
 \and
 \inferrule[Adapt]{
-    \type{N}_1 \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
-    \type{N}_1 <: \exptype{C}{\type{S}_1 \ldots \type{S}_n} \\
+    \type{N} \lessdot \exptype{C}{\type{P}_1 \ldots \type{P}_n} \\
+    \type{N} <: \exptype{C}{\type{P'}_1 \ldots \type{P'}_n}
 }{
-    \exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
+    \type{P}_1 \doteq \type{P'}_1 \ \ldots \ \type{P}_n \doteq \type{P'}_n \\
 }
 \and
 \inferrule[Reduce]{
-    \exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
+    \exptype{C}{\type{P}_1 \ldots \type{P}_n} \doteq \exptype{C}{\type{P'}_1 \ldots \type{P'}_n} \\
 }{
-    \type{S}_i \doteq \type{T}_i \\
+    \type{P}_i \doteq \type{P'}_i \\
 }
+\and
+\inferrule[Super]{
+    \type{N} \lessdot \tv{a}\\
+    \type{N} <: \type{N}_1, \ldots, \type{N} <: \type{N}_n \\
+    \type{N}_1, \ldots, \type{N}_n \ \ok
+}{
+    \text{for one}\ m \in \set{1, \ldots, n}: \quad  \tv{a} \doteq \type{N}_m
+} 
 \end{mathpar}
-
-\begin{mathpar}
-    \text{Apply only once per constraint:}\quad 
-    \inferrule[Super]{
-        \type{N} \lessdot \tv{a}\\
-        \type{N} <: \type{N}' 
-    }{
-        \tv{a} \doteq \type{N}'
-    } 
-\end{mathpar}
-
-\begin{center}
-    Apply one or the other:
-\end{center}
-\begin{mathpar}
-    \inferrule[Split-L]{
-        \tv{a} \lessdot \tv{b}\\
-        \tv{a} \lessdot \type{N}\\
-    }{
-        \tv{b} \lessdot \type{N}
-    }
-    \quad \quad
-    \vline
-    \quad \quad
-    \inferrule[Split-R]{
-        \tv{a} \lessdot \tv{b}\\
-        \tv{a} \lessdot \type{N}\\
-    }{
-        \type{N} \lessdot \tv{b}
-    }
-\end{mathpar}
-
-Result:
+\textbf{Solution:}
 \begin{mathpar}
 \inferrule[Solution]{
     \tv{a} \doteq \type{G}
@@ -412,10 +404,17 @@ Result:
 }
 \and
 \inferrule[Solution-Gen]{
-    \tv{a} \lessdot \type{C}_1, \ldots, \tv{a} \lessdot \type{C}_n \\
-    \forall i: \type{C}_m << \type{C}_i \\
+    \tv{a} \lessdot \type{N}
 }{
-    \tv{a} \doteq \type{C}_m
+    \tv{a} \doteq \type{N} \ \text{or}\ \tv{a} \lessdot \type{N}
+}
+\and
+\inferrule[Solution-Requirement]{
+\tv{a} \lessdot \type{N}_1
+%, \tv{a} \doteq \type{N}_2
+, \ldots, \tv{a} \lessdot \type{N}_n \\
+}{
+    \text{there must exist atleast one}: \quad  \tv{a} \doteq \type{N}
 }
 % \and
 % \inferrule[Solution-Gen]{
@@ -434,30 +433,28 @@ Result:
 %     \Delta(\type{A}) = \type{G}
 % }
 \end{mathpar}
-
-Fail:
-            
+\textbf{Fail Conditions:}
 \begin{mathpar}
-% \inferrule[Fail]{
-%     \type{T} \lessdot \type{N}\\
-%     \type{T} \nless : \type{N} 
-% }{
-%     \emptyset
-% }
-% \and
-\inferrule[Fail]{
+\inferrule[Fail-Subtype]{
+    \exptype{C}{\ldots} \lessdot \exptype{D}{\ldots}\\
+    \type{C}\ \kw{not extends}\ \type{D}
+}{
+    \emptyset
+}
+\and
+\inferrule[Fail-Equals]{
     \exptype{C}{\ldots} \doteq \exptype{D}{\ldots}\\
     \type{C} \neq \type{D}
 }{
     \emptyset
 }
-\and
-\inferrule[Fail-Generic]{
-    \type{X} \doteq \type{T}\\
-    \type{X} \neq \type{T}
-}{
-    \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} \\
@@ -465,242 +462,21 @@ Fail:
 }{
     \emptyset
 }
-\and
-\inferrule[Fail]{
-\tv{a} \lessdot \type{N}_1 \\
-\tv{a} \lessdot \type{N}_2 \\
-\text{not}\ \type{N}_1 << \type{N}_2 \\
-\text{not}\ \type{N}_2 << \type{N}_1
-}{
-    \emptyset
-}
+% \and
+% \inferrule[Fail]{
+% \tv{a} \lessdot \type{N}_1 \\
+% \tv{a} \lessdot \type{N}_2 \\
+% \text{not}\ \type{N}_1 << \type{N}_2 \\
+% \text{not}\ \type{N}_2 << \type{N}_1
+% }{
+%     \emptyset
+% }
 \end{mathpar}
-
-% Subst
-% a =. N, a <. T, N <: T
-% --------------
-% N <. T
-
-% a <. List<b>, b <. List<a>
-
-% how to proof completeness and termination?
-% TODO: how to proof termination?
-
-The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
-
-\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}).
-
-% \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}
-
-\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{minipage}
+}
+\caption{Unify Algorithm}\label{fig:aspUnifyAlgorithm}
 \end{figure}
 
-%The $\aspify{}$ function converts our formal specification of the algorithm to ASP code.
-
-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))).}}}
-
-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"))))}.
-
-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}
-% \begin{lemma}{Substitution:}
-% For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
-% there also exists a constraint $[\type{T}/\tv{a}]c$.
-
-% \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
-
-% \section{Termination}
-
-% 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.
-
-% 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.
-
-% 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.
-
-% 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}$.
-
-% \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.
@@ -718,9 +494,9 @@ The Java implementation also supports Java wildcard types whereas the ASP implem
 %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,
+While 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.
 
 

prolog.tex

@@ -1,27 +1,102 @@
+\usepackage{csquotes}
+\usepackage{amsmath}
+\usepackage{amssymb}
 \usepackage{xspace}
 \usepackage{color,ulem}
+\usepackage{mathpartir}
+
+\usepackage{qtree}
+
+\usepackage{enumitem}
+\usepackage{tabularx}
+
+\usepackage{amssymb,amsmath,amsthm}
+
+\newtheorem{theorem}{Theorem}
+
 \usepackage{listings}
+
 \lstset{language=Java,
   showspaces=false,
   showtabs=false,
   %breaklines=true,
   showstringspaces=false,
   %breakatwhitespace=true,
-  basicstyle=\ttfamily, %\footnotesize
+  basicstyle=\small\ttfamily, %\footnotesize
   escapeinside={(*@}{@*)},
-  captionpos=t,float,abovecaptionskip=-\medskipamount
+  captionpos=t,float,%abovecaptionskip=\medskipamount,
+  %backgroundcolor=\color{lipicsLightGray},%
+  frame=single,framerule=0pt,xleftmargin=\fboxsep,xrightmargin=\fboxsep
 }
 
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
+\lstdefinestyle{javatx}{backgroundcolor=\color{yellow!20}}
 \lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{constraints}{
   basicstyle=\normalfont,
   backgroundcolor=\color{red!20}
 }
 
+\newcommand{\code}[1]{\texttt{#1}}
+\newcommand{\todo}[0]{\texttt{TODO}}
+\newtheorem{lemma}[theorem]{Lemma}
+
+\newcommand{\tokenOne}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenOne}%
+  \endgroup%
+}
+\newcommand{\tokenTwo}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenTwo}%
+  \endgroup%
+}
+\newcommand{\tokenThree}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenThree}%
+  \endgroup%
+}
+\newcommand{\tokenFour}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenFour}%
+  \endgroup%
+}
+\newcommand{\tokenFive}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenFive}%
+  \endgroup%
+}
+\newcommand{\tokenSix}{%
+  \begingroup\normalfont%
+  \includegraphics[height=\fontcharht\font`\B]{images/tokenSix}%
+  \endgroup%
+}
+
+\newenvironment{note}{\begin{figure}[h]\begin{minipage}[t]{0.08\textwidth}
+  \colorbox{black}{\textcolor{white}{\textbf{\texttt{Note}}}}
+  \end{minipage}
+  \begin{minipage}[t]{0.92\textwidth}
+    \itshape}
+    {\end{minipage}\end{figure}}
+
+\newcommand{\kw}[1]{\texttt{#1}}
+\newcommand{\tlist}[1]{\ol{\mv{#1}}}
+\newcommand{\elist}[1]{\ol{\mv{#1}}}
+
+\newtheorem{definition}{Definition}
+
+% TODO: make example environment better (needs spacing)
+\newenvironment{example}{ 
+  \noindent
+  \textbf{Example} 
+}
+{}
+
+\newcommand{\subcons}{\ensuremath{\ \mathtt{<:}\ }}
+
 \newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
 
 \newcommand{\tifj}{\texttt{TamedFJ}}
@@ -207,10 +282,10 @@
 
 \newenvironment{constraintset}
     {
-\begin{tcolorbox}
+      %nothing
     }
     { 
-\end{tcolorbox}
+      % nothing
     }
 
 \newcommand{\wcNtype}[2]{\exists #1 .\ntype{#2}}