Cleanup. Define mutual subtyping as equality

constraints.tex

@@ -26,6 +26,12 @@ $
 The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
 Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
 
+
+The parameter types given to a generic method also affect their return type.
+During constraint generation the algorithm does not know the parameter types yet.
+We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
+$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
+
 At points where a well-formed type is needed we use a normal type placeholder.
 Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
 Here captured variables can flow freely.
@@ -144,11 +150,11 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
     \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
-                    & \tv{e} \ \text{fresh} \\
+                    & \tv{e}, \tv{x} \ \text{fresh} \\
                     & \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\
                     & \constraint =
                       \set{
-                      \tv{e} \lessdotCC \tv{x} 
+                      \tv{e} \lessdot \tv{x} 
                       }\\
                     {\mathbf{in}} & {
                     \consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}})
@@ -190,7 +196,7 @@ The ones to already typed methods and calls to untyped methods.
       \textbf{let}
       & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
       & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
-                    \ol{S} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
+                    \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
                     \ol{Y} \lessdot \ol{N} }\\
       \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
       & \mathbf{where}\ \begin{array}[t]{l}

introduction.tex

@@ -513,6 +513,17 @@ $
 \end{figure}
 % TODO: make Unify to resolve C<X> <. a as a =. X.C<X>
 
+% A method has infinte possibilities of being called and there is no most general type.
+% P<X,Y> m(C<X> c, C<Y> c2)
+% depending on 
+% A.P<A,A> <. A,B.P<A,B>
+
+% % During the method call it is not sure what kind of return type is needed from the method.
+% % The method P<A,B> make(A a, B b) 
+% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
+% % But if A^X_X and B^X_X
+% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
+
 
 \end{itemize}
 

soundness.tex

@@ -329,18 +329,17 @@ If there is a solution for a constraint set $C$, then there is also a solution f
 % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
 % maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
 
-\begin{lemma}\label{lemma:unifySoundness}
-The \unify{} algorithm only produces correct output.
+\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
 \begin{description}
 \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
-%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
-\item[Then] there exists a $\sigma'$ with:
-$\sigma \subseteq \sigma'$ and
-$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
-and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
-otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
-% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
-
+\item[Then] there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
+\begin{itemize}
+\item $\sigma \subseteq \sigma'$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
+\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
+\end{itemize}
 \end{description}
 \end{lemma}
 
@@ -433,7 +432,8 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
 \item[Circle] S-Refl
 \item[Swap] by definition
 \item[Erase] S-Refl
-\item[Equals] %by definition
+\item[Equals] by definition \ref{def:equal}
+%by definition
 %TODO
 % Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
 

unify.tex

@@ -1,80 +1,11 @@
 % TODO: unify changes
-% a? <. T can be deleted in the last step
 % delete wildcard tphs a? when needed
 % aswell ass free variables:
 % a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
-% also in T <. T constraints no free variables are allowed on both sides
+% also in T <. T constraints no free variables are allowed on both sides (why? this is wrong i think)
 % the algorithm only removes wildcards, never adds them
 
-% lessdotCC constraint cannot be removed. we do not know what to capture
-% example <X> add(List<X> l, X v)
-% here we need to generate constraints p1 <c List<x>, p2 <c x
-% because x can become List<a?>:
-
-% class Box<X>{}
-
-% class Test{
-
-%     static <X> Box<X> add(Box<X> b, X x){return null;}
-%     static <X> Box<X> empty(){return null;}
-%     static <X> Box<Box<X>> empty2(){return null;}
-%     public static void main(String args[]){
-%         Box<?> b = null;
-%         Box<? extends Box<?>> b2 = add(empty2(), b);
-%     }
-% }
-
 \section{Unify}\label{sec:unify}
-
-%TODO: Remove lessdotC constraints. those have to be handeld during constraint generation
-% is capture conversion for methods in the same class unsovable? Can it be reduced to polymorphic recursion?
-% the other problem is, that there are infinite subtypes.
-% For example for a type X^Infinite<X>.Infinite<X>
-% here a correct subtype would be an instantiation of the class Omega extends Infinite<Omega> 
-
-The parameter types given to a generic method also affect their return type.
-During constraint generation the algorithm does not know the parameter types yet.
-We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
-$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
-
-% A method has infinte possibilities of being called and there is no most general type.
-% P<X,Y> m(C<X> c, C<Y> c2)
-% depending on 
-% A.P<A,A> <. A,B.P<A,B>
-
-% % During the method call it is not sure what kind of return type is needed from the method.
-% % The method P<A,B> make(A a, B b) 
-% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
-% % But if A^X_X and B^X_X
-% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
-
-% Why is there no most general type?
-% - the return type depends on the parameter types
-The most general type denotable in Java of a class $\exptype{C}{\ol{X}}$
-is $\wctype{\ol{X}}{C}{\ol{X}}$
-
-%Is there a direct subtype of a type N including generics? e.g. a <c C<C<x>> 
-% AND if yes! why is there not a most generic expression of a method head without the need of Capture Conversion?
-% Pair<X,Y> m(List<X> l, List<Y> l2) => X,Y.Pair<X,Y> m()
-% X.List<X> <. List<x>
-% because we want the most specfic return type and the least specific parameter types!
-
-
-A method is only equiped with generic parameters if they only appear in a <. T constraints
-Polymorphic recursion makes it impossible to infer a generic type who is called in a more specific way.
-Is it? Not ours for sure!
-
-The problem is, that we don't know which type is the parameter of the method call.
-And a method with a parameter \texttt{List<? extends A>} can have an infinite number of subtypes. %Does it?
-% Y.List<Y> <c Z^List<x>.List<Z>
-% Y <. List<x>
-
-% X,Y^List<X>.List<Y> <c Z^List<x>.List<Z>
-
-% The idea is to hold out until the left side of a $\lessdotCC$ constraint is known to be a named type
-% and then check if the typing is still correct.
-
-
 The wildcard placeholders are used for intermediat types.
 It is not possible to create all super types of a type.
 The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
@@ -93,46 +24,71 @@ $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \
 Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
 which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
 
-The algorithm works in a recursive fashion.
-The input constraints are transformed until they reach a irreducible state,
-which the last step of the algorithm eventually transforms into a solution.
-A constraint set is convertable to a correct type solution if it only contains constraints of the form
-$\tv{a} \doteq \type{T}$ (where $\tv{a} \notin \text{tph}(\type{T})$) and $\tv{a} \lessdot \type{T}$.
-We call this \textit{Solved Form}.
+The input constraints are transformed until they reach a solved form which is then converted to a type solution.
+A constraint set is in solved form if it only consists of constraints of the form 
+$\tv{a} \doteq \type{T}$ and $\tv{a} \lessdot \type{T}$.
+\unify{} is described as a nondeterministic algorithm.
+Some constraints allow for multiple transformations from which
+the algorithm has to pick the right one.
+There are also cases where there is more than on correct transformation and
+therefore more than one correct solution to the given input constraints.
+For that case still only one correct solution is returned by this specification of the algorithm.
+Our implementation of the algorithm considers this and tries every possible transformation option
+and gathers all possible type solutions.
+We skip the definition of this practice, because it is already described in \cite{TIforFGJ}
+and only needed for a proof of completeness.
 
 The \unify{} algorithm applies conversions according to the subtyping rules (depicted in figure \ref{fig:subtyping}).
 At every step we try to find a reduction, which brings us closer to solved form without excluding any possible solution.
-
-A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
+\textit{Examples:}
+\begin{itemize}
+\item A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
 For the type placeholder $\tv{a}$ in the constraint $\tv{a} \lessdot \bot$ only the $\bot$ type is a possible substitution,
 which is set by the \rulename{Pit} rule.
-
-The \rulename{Reduce} rule represents the S-Exists type rule.
+\item The \rulename{Reduce} rule represents the S-Exists type rule.
 This rule uses wildcard placeholders ($\ol{\wtv{a}}$) to find a possible substitution for the wildcards on the right side.
 The constraint $\type{N} \lessdot \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N'}$ is satisfied if
 there is a substitution $[\ol{T}/\ol{X}]\type{N} = \type{N'}$ with $\ol{T}$ inside the bounds $\ol{U}$ and $\ol{L}$.
 
-\textbf{Example:}
+For example the constraint
 $\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ 
-The \rulename{Reduce} rule converts this to 
+is converted to 
 $\set{\tv{a} \doteq \wtv{x}, \wtv{x} \lessdot \type{Object}, \bot \lessdot \wtv{x} }$.
 After applying \rulename{Swap} and \rulename{Subst-WC} on $\tv{a} \doteq \wtv{x}$ we get
 $\set{\tv{a} \lessdot \type{Object}, \bot \lessdot \tv{a}}$ and can now apply the \rulename{Bot} rule.
+This leaves us with $\set{\tv{a} \lessdot \type{Object}}$.
+\item The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints
+\item \rulename{Equals} ensures equality of two types by ensuring they are mutual subtypes.
+Constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
+are transformed to
+$\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \lessdot \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
+and $\wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}} \lessdot \wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}}$.
+% The types $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and $\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$
+% are equal.
+\end{itemize}
 
-The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints.
-But what about constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
-The \rulename{Equals} rule converts this to 
-
-% The equals rule is complicated, because 
-% X.List<X> =. Y.List<Y> -> is the same
-% X^String.List<X> =. X.List<X> -> is not!
-
-% T =. T => T <. T
+We define two types as equal if they are mutual subtypes of each other.
+%This relation is symmetric, reflexive and transitive by the definition of subtyping.
+%This definition is sufficient for proofing soundness.
+\begin{definition}{Type Equality:}\label{def:equal}
+  $\Delta \vdash \type{S} = \type{T}$ if $\Delta \vdash \type{T} <: \type{S}$ and $\Delta \vdash \type{T} <: \type{S}$
+\end{definition}
+%This definition makes sense
+% The symmetric subtyping allows this type to be substit
+% We define types to be equal if they are symmetric subtypes.
+% This allows the substitution of these types with eachother.
+% If $\Delta \vdash \type{S} = \type{S'}$ and $\Delta \vdash \type{T} <: \type{T'}$,
+% then $\Delta \vdash [\type{S}/\type{S'}]\type{T} <: \type{T'}$.
 
 
-% Special cases: lessdotCC, Normalize/Tame rule, 
-The $\lessdotCC$ constraints and the wildcard placeholders $\wtv{a}$ are kept as long as possible.
-%TODO: Example where lessdotCC constraints get spared until they can be captured
+The equality relation on Capture constraints is not reflexive.
+$(\type{T} \lessdotCC \type{S}) \neq (\type{T} \lessdotCC \type{S})$ eventhough it's the same constraint.
+
+Capture conversion is done during the \unify{} algorithm.
+\unify{} has to make two promises to ensure soundness of our type inference algorithm.
+Capture conversion can only be applied at capture constraints.
+Free variables are not allowed to leave their scope.
+This is ensured by type variables which are not allowed to be assigned type holding free variables.
 
 \subsection{Algorithm}
 
@@ -155,15 +111,7 @@ The input constraints must be of the following format:
 \noindent
 Additional requirements:
 \begin{itemize}
-\item Every wildcard $\rwildcard{X} \in \Delta'$ has to have an unique name which is not defined anywhere in the constraint set $C$.
-  \item The input only consists of $\lessdot$ constraints
-%   \item No free variables in type parameters.
-% A constraint like $\tv{a} \lessdot \exptype{List}{\rwildcard{X}}$ is prohibited.
-% $\tv{a} \lessdot \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is valid.
-  \item the input is a list of constraints. It cannot be a set.
-  A constraint set containing the constraint $\tv{a} \lessdot \type{T}$ twice
-  is a different to one that contains it only once.
-  %\item every wildcard is bound to its enclosing type.
+
   \item All types have to be well-formed: $\wcNtype{\Delta}{N} \in C \implies \Delta_{in} \vdash \wcNtype{\Delta}{N} \ \ok$
 \item Naming scheme of every wildcard environment has to be the same.
 %TODO: We need this so that wildcard substitutions get the correct name. also the Equals rule needs this condition
@@ -259,11 +207,8 @@ $
 \end{figure}
 
 
-The capture constraints are preserved when applying the \rulename{Upper} rule.
-%because \texttt{let} statements like
-%let x : X = v in
-%can be transformed to 
-%let x : U = v in 
+%The capture constraints are preserved when applying the \rulename{Upper} rule.
+% This is legal: a T <c S constraint indicates a let-statement can be inserted. Therefore there must exist a type T' with T <. T' <c S
 
 \begin{figure}
   \begin{center}
@@ -372,37 +317,38 @@ The capture constraints are preserved when applying the \rulename{Upper} rule.
       \quad \type{T} \ \text{is no wildcard placeholder}
     $
     \\\\
-% \rulename{Equals} %TODO
-%     & $
-%     \begin{array}[c]{l}
-%         \wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\ 
-%         \hline
-%         \vspace*{-0.4cm}\\
-%         \wildcardEnv \vdash C \cup \, 
-%         \set{
-%            \type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N}
-%         }
-%     \end{array} % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset 
-%     $
-%      \\\\
- \rulename{Equals} %TODO
-& $
-\begin{array}[c]{l}
-    \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ 
-    \hline
-    \vspace*{-0.4cm}\\
-    \wildcardEnv \vdash C \cup \, 
-    \set{
-      \pi(\ol{T}) \doteq  \pi(\ol{T'} )
-      %\ol{T} \doteq \ol{T'}
-    }
-\end{array}
-\quad \begin{array}{l}
-\text{given a permutation}\ \pi\ \text{with:}\\
-\pi(\Delta) = \pi(\Delta')
-\end{array}
-   $
-   \\\\
+\rulename{Equals} %TODO
+    & $
+    \begin{array}[c]{l}
+        \wildcardEnv \vdash C \cup \, \set{ \wcNtype{\Delta}{N} \doteq \wcNtype{\Delta'}{N'} } \\ 
+        \hline
+        \vspace*{-0.4cm}\\
+        \wildcardEnv \vdash C \cup \, 
+        \set{
+          \wcNtype{\Delta}{N} \lessdot \wcNtype{\Delta'}{N'}, \wcNtype{\Delta'}{N'} \lessdot \wcNtype{\Delta}{N}
+        }
+    \end{array} %\quad |\Delta| = |\Delta'|
+    % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset 
+    $
+     \\\\
+%  \rulename{Equals} %TODO
+% & $
+% \begin{array}[c]{l}
+%     \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ 
+%     \hline
+%     \vspace*{-0.4cm}\\
+%     \wildcardEnv \vdash C \cup \, 
+%     \set{
+%       \pi(\ol{T}) \doteq  \pi(\ol{T'} )
+%       %\ol{T} \doteq \ol{T'}
+%     }
+% \end{array}
+% \quad \begin{array}{l}
+% \text{given a permutation}\ \pi\ \text{with:}\\
+% \pi(\Delta) = \pi(\Delta')
+% \end{array}
+%    $
+%    \\\\
     \rulename{Erase}
     & $
     \begin{array}[c]{l}
@@ -439,6 +385,11 @@ The capture constraints are preserved when applying the \rulename{Upper} rule.
         \wildcardEnv \vdash C \cup \set{\type{N} \doteq \rwildcard{A}}\\
         \hline
         \wildcardEnv \vdash C \cup \set{\rwildcard{A} \doteq \type{N}}
+        \end{array} \quad
+        \begin{array}[c]{l}
+        \wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \rwildcard{A}}\\
+        \hline
+        \wildcardEnv \vdash C \cup \set{\rwildcard{A} \doteq \ntv{a}}
         \end{array}$
 \end{tabular}}
 \end{center}
@@ -583,6 +534,46 @@ Their upper and lower bounds are fresh type variables.
     \end{array}
     $
   \\\\
+  \rulename{Clear}
+  & 
+  $
+  \begin{array}[c]{@{}ll}
+  \begin{array}[c]{l}
+      \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash 
+      C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\ 
+    \hline
+    \vspace*{-0.4cm}\\
+    \subst{\type{U}}{\rwildcard{A}}\wildcardEnv \vdash 
+      [\type{U}/\rwildcard{A}]C \cup \, [\type{U}/\rwildcard{A}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\  
+  \end{array}
+   %\quad \ol{Y} = \textit{fresh}(\ol{X})
+   \quad \begin{array}[c]{l}
+    \Delta \neq \emptyset\\
+    \rwildcard{A} \in \text{fv}(\type{T})
+    \end{array}
+  \end{array}
+  $
+\\\\
+\rulename{Exclude}
+& 
+$
+\begin{array}[c]{@{}ll}
+\begin{array}[c]{l}
+    \wildcardEnv \vdash 
+    C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\ 
+  \hline
+  \vspace*{-0.4cm}\\
+  \subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash 
+    [\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\  
+\end{array}
+ %\quad \ol{Y} = \textit{fresh}(\ol{X})
+ \quad \begin{array}[c]{l}
+  \Delta \neq \emptyset\\
+  \wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
+  \end{array}
+\end{array}
+$
+\\\\
         \rulename{Adopt}
         & $
         \begin{array}[c]{@{}ll}
@@ -1002,137 +993,6 @@ This builds a search tree over multiple possible solutions.
   \label{fig:step2-rules}
   \end{figure}
 
-% \begin{figure}
-% \begin{center}
-%         \fbox{
-%         \begin{tabular}[t]{l@{~}l}
-%         \rulename{Same}
-%         & $
-%         \begin{array}[c]{l}
-%           \wildcardEnv \vdash
-%           C \cup \type{G} \lessdot \tv{a}\\
-%           \hline
-%           \wildcardEnv \vdash
-%           C \cup \set{
-%             \tv{a} \doteq \type{G}
-%         }
-%         \end{array} \quad \begin{array}[c]{l}
-%           \text{fv}(\type{G}) \in \Delta_{in}
-%         \end{array}
-%           $
-%       \\\\ 
-%           \rulename{\generalizeRule}
-%           & $
-%           \begin{array}[c]{l}
-%             \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
-%             \hline
-%             \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a},
-%           \tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
-%           %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
-%           \overline{\tv{u} \lessdot \type{S}}
-%           }
-%           \end{array} \quad \begin{array}[c]{l}
-%             \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
-%             \text{fresh}\ \overline{\wildcard{X}{\tv{u}}{\tv{l}}}
-%           \end{array}
-%             $
-%         \\\\ 
-%         \rulename{Subst-X}
-%         & $
-%         \begin{array}[c]{l}
-%           \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
-%           C \cup \rwildcard{X} \lessdot \tv{a}\\
-%           \hline
-%           \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
-%           C \cup \set{
-%             \tv{a} \doteq \rwildcard{X}
-%         }
-%         \end{array} \quad \begin{array}[c]{l}
-%           \rwildcard{X} \in \Delta_{in}
-%         \end{array}
-%           $
-%       \\\\ 
-%       \rulename{Gen-X}
-%       & $
-%       \begin{array}[c]{l}
-%         \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
-%         C \cup \rwildcard{X} \lessdot \tv{a}\\
-%         \hline
-%         \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
-%         C \cup \set{
-%           \type{U} \lessdot \tv{a}
-%       }
-%       \end{array}
-%         $
-%     \\\\ 
-%         \rulename{Super}
-%         & $
-%         \begin{array}[c]{l}
-%           \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
-%           \hline
-%           \wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a}   }
-%         %\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
-%         \end{array} \quad
-%         \begin{array}{l}
-%           \texttt{class} \ \exptype{C}{\ol{X}} \triangleleft \exptype{D}{\ol{N}} \\
-%           \ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
-%         \end{array}
-%         $
-%       \\\\ 
-%       \rulename{Settle}
-%       & $
-%       \begin{array}[c]{l}
-%         \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-%         \tv{a} \lessdot \tv{b}}
-%         \\
-%         \hline
-%         \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot \tv{b}, \tv{b} \lessdot \type{N}  }
-%       \end{array}
-%       $
-%     \\\\ 
-%     \rulename{Raise}
-%     & $
-%     \begin{array}[c]{l}
-%       \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-%       \tv{a} \lessdot \tv{b}}
-%       \\
-%       \hline
-%       \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
-%     \end{array}
-%     $
-%   \\\\ 
-%     \end{tabular}}
-%   \end{center}
-% \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
-% \label{fig:step2-rules}
-% \end{figure}
-
-
-%For every $\type{T} \lessdot \tv{a}$ constraint, the unify algorithm has to consider every possible supertype of $\type{T}$.
-%For every $\type{N}$ with $\type{T} \leq \type{N}$: ($\texttt{class} \ \exptype{T}{\ol{Y} \triangleleft \ol{N}} \triangleleft \type{N}$) 
-%There are two different ways of handling a $\type{T} \lessdot \tv{a}$ constraint:
-%TODO: why the \generalizeRule is basically the Same rule for regular type placeholders
-
-%where is the mistake in the old unify algorithm? 
-%when working with equality the problems arise! Free variables should not escape their scope
-% Replacing regular type placeholders causes problems related to method calls and capture conversion.
-
-% <X> List<X> same(List<X> a, List<X> b){}
-
-% This program has no correct type. the same method requires 
-% \begin{lstlisting}
-% List<?> f;
-% List<?> problem(){
-%   return same(problem(), problem()) ?: f;
-% }
-% \end{lstlisting}
-% \begin{constraints}
-% r <. List<x?>
-% r <. List<x?>
-% X.List<X> <. r
-% \end{constraints}
-% %TODO
-
 \unify{} generates wildcard types for constraints of the form $\type{N} \lessdot \tv{a}$ with the \rulename{\generalizeRule} rule.
 Otherwise only the wildcards already defined in the input constraints will be included in the result.
 \rulename{\generalizeRule} attempts to give $\tv{a}$ a more general type by replacing only the type parameters with fresh wildcards.
@@ -1145,15 +1005,6 @@ need to be handled in a similiar fashion.
 The type variable $\tv{b}$ could either be a sub or a supertype of the type $\type{N}$.
 We have to consider both possibilities.
 \\[1em]
-% The specification of the \unify{} algorithm has only two rules generating $\doteq$-Constraints
-% , \rulename{Reduce} and \rulename{Ground}.
-% $\doteq$-Constraints and the accompaning substitutions are dangerous respective to the soundness of the algorithm.
-% For the soundness proof of the \unify{} algorithm we have to show every generation of equals constraints
-% and the subsequent application of the \rulename{subst} rule is correct.
-% We try to use them as sparsely as possible to simplify the soundness proof.
-% You can notice this at \rulename{Equals} or \rulename{Force}:
-% Instead of setting $\type{U} \doteq \type{L}$, we say
-% $\type{U} \lessdot \type{L}, \type{L} \lessdot \type{U}$.
 
 \noindent
 \textbf{Step 3} 
@@ -1164,23 +1015,6 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
 \begin{center}
   \fbox{
   \begin{tabular}[t]{l@{~}l}
-%     \rulename{Remove} % kann beim Subst step gemacht werden und ist nur nötig wenn ein a =. T constraint mit wtv(T) > 1 entsteht
-%     & $
-%     \begin{array}[c]{@{}ll}
-%     \begin{array}[c]{l}
-%        \wildcardEnv \vdash C \\
-%         % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\ 
-%       \hline
-%       \vspace*{-0.4cm}\\
-%       \subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash [\tv{a}/\wtv{a}]C 
-%     \end{array}
-%     &\begin{array}[c]{l}
-%       \wtv{a} \in C \\
-%       \tv{a} \ \text{fresh}
-%    \end{array}
-%     \end{array}
-% $
-% \\\\
 \rulename{Remove-Cons} & $
     \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{\type{S} \lessdotCC \type{T} } \\
@@ -1192,23 +1026,6 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
 \end{tabular}}
 \end{center}
 
-% \textbf{Step 4:}
-% If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
-% apply the \rulename{Sub-Elim} rule and start over with step 1.
-% Otherwise continue to step 5.
-% \begin{center}
-%   \fbox{
-%   \begin{tabular}[t]{l@{~}l}
-%     \rulename{SubElim} 
-%     & $\begin{array}[c]{l}
-%       \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
-%       \hline
-%       [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
-%     \end{array}
-%     $
-% \end{tabular}}
-% \end{center}
-
 \noindent
 \textbf{Step 4:}
 We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6.
@@ -1242,43 +1059,6 @@ C \cup \set{ \tv{a} \doteq \bot }
 %\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
 \end{array}
 \end{array}$
-% \\\\  % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards
-% \rulename{Force} &$
-%   \begin{array}[c]{@{}ll}
-%   \begin{array}[c]{l}
-%      \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
-% \vdash C \cup \, \set{
-%         \tv{a} \lessdot \type{N} } \\ 
-%     \hline
-%     \vspace*{-0.4cm}\\
-%     \wildcardEnv 
-% \vdash
-%     C \cup \, \set{ \tv{a} \lessdot [\type{U}/\rwildcard{X}]\type{N}, 
-%      \type{U} \doteq \type{L} }
-%   \end{array}
-%   &\begin{array}[c]{l}
-%     \type{X} \in \text{fv}(\type{N}) \\
-%     %\Delta' = \Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
-%  \end{array}
-%   \end{array}$
-% \\\\
-% \rulename{FlatOut} &$
-%   \begin{array}[c]{@{}ll}
-%   \begin{array}[c]{l}
-%      \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
-% \vdash C \cup \, \set{
-%         \tv{a} \lessdot \wcNtype{\Delta}{N} } \\ 
-%     \hline
-%     \vspace*{-0.4cm}\\
-%     \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
-% \vdash
-%     C
-%   \end{array}
-%   &\begin{array}[c]{l}
-%     \type{X} \in \text{fv}(\wcNtype{\Delta}{N}) \\
-%     \tv{a} \notin C , \, \tv{a} \notin \wildcardEnv, \tv{a} \notin \sigma
-%  \end{array}
-%   \end{array}$
   \end{tabular}}
 \end{center}
 \caption{Cleanup rules}\label{fig:cleanup-rules}