Add Abstract and Termination

aspUnify.tex

@@ -56,9 +56,16 @@
 \maketitle              % typeset the header of the contribution
 %
 \begin{abstract}
-The abstract should briefly summarize the contents of the paper in
-150--250 words.
+Global type inference for Java is able to compute correct types for an input program
+which has no type annotations at all.
+Global type inference for Featherweigt Generic Java is NP-hard.
+Former implementations of the algorithm struggled with bad runtime performance.
+In this paper we translated 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.
 
+%TODO: Is this correct?
 \end{abstract}
 %
 %
@@ -120,6 +127,7 @@ The need to have an upper bound to every type placeholder.
 
 We have to formulate the unification algorithm with implication rules.
 Those can be directly translated to ASP.
+\label{sec:implicationRules}
 \begin{mathpar}
 \inferrule[Subst]{
     \tv{a} \doteq \type{N}
@@ -300,7 +308,7 @@ Fail:
 }
 \and
 \inferrule[Fail-Sigma]{
-    \tv{a} \doteq \type{N} \\
+    \tv{a} \mapsto \type{N} \\
     \tv{a} \in \type{N}
 }{
     \emptyset
@@ -329,10 +337,22 @@ Fail:
 The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
 
 \section{ASP Encoding}
+The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program.
+
 \begin{tabular}{l | r}
 $\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
 \end{tabular}
 
+\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.
+
+
 \section{Completeness}
 To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.