Add Intro and Termination

aspUnify.tex

@@ -87,6 +87,13 @@ Java has adopted more and more type inference features over time.
 Currently Java only has local type inference.
 We want to bring type inference for Java to the next level.
 
+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.
+These programs tend to be in exponential time upper bounded by the amount of ambiguous method calls and subtype relations.
+%TODO: Example with multiple calls to m.toString(). All possibilities are checked in a naive implementation!
+
 \section{Subtyping}
 \begin{mathpar}
 \inferrule[Refl]{}{
@@ -343,7 +350,14 @@ The implication rules defined in chapter \ref{sec:implicationRules} can be trans
 $\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
 \end{tabular}
 
+\section{Proofs}
+\begin{lemma}{Substitution}
+
+
+\end{lemma}
+
 \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
@@ -352,6 +366,9 @@ 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.
+
 
 \section{Completeness}
 To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.