Start with cctv and soundness proof

Fixes for Soundness Proof. Start with Capture Conversion at Subst-Step and introduce ccTVs
Remove Adopt
2024-07-23 10:47:20 +02:00 · 2024-07-17 16:15:24 +02:00 · 2024-06-04 01:55:48 +02:00 · 2024-05-31 13:52:18 +02:00 · 2024-05-31 11:49:44 +02:00 · 2024-05-31 00:10:22 +02:00
11 changed files with 1417 additions and 1278 deletions
--- a/TIforWildFJ.tex
+++ b/TIforWildFJ.tex
@@ -38,6 +38,8 @@
 \usepackage{arydshln}
 \usepackage{dashbox}

+\usepackage{mathpartir}
+
 \input{prolog}

 \begin{document}
@@ -112,51 +114,26 @@

 \input{tRules}

+\input{typeinference}
+
 %\input{tiRules}

 \input{constraints}

 \input{Unify}

-\section{Limitations}
-
-This example does not work:
-
-\begin{minipage}{0.35\textwidth}
-  \begin{verbatim}
-class Example{
-<A> Pair<A,A> make(List<A> l){...}
-<A> bool compare(Pair<A,A> p){...}
-
-  bool test(List<?> l){
-    return compare(make(l));
-  }
-}
-\end{verbatim}
-  \end{minipage}%
-  \hfill
-  \begin{minipage}{0.55\textwidth}
-\begin{constraintset}
-    \textbf{Constraints:}\\
-    $
-  \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
-  \exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
-  \tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
-  %\tv{y} \lessdot \tv{m}
-    $\\
-\end{constraintset}
-  \end{minipage}
-
+\include{relatedwork}

 \input{conclusion}

-\include{soundness}
 %\include{termination}
-\include{relatedwork}

 \bibliography{martin}

 \appendix
+
+\include{soundness}
+\include{helpers}
 %\include{examples}
 %\input{exampleWildcardParameter}
 %\input{commonPatternsProof}
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,68 +1,62 @@
-\section{Properties of the Algorithm}
-\begin{itemize}
-    \item Our algorithm is designed for extensibility with the final goal of full support for Java.
-    \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
-    Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
-    
-\end{itemize}
-
 %TODO: how are the challenges solved: Describe this in the last chapter with examples!
-\section{Soundness}\label{sec:soundness}
+\section{Discussion}\label{sec:completeness}
+We couldn't verify it with an implementation yet, but we assume atleast the same functionality
+as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}.

-\section{Completeness}\label{sec:completeness}
-The algorithm can find a solution to every program which the Unify by Plümicke finds
-a correct solution aswell.
-It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
-There is propably some loss of completeness when capture constraints get deleted.
-This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible.
-Here the variable $\tv{a}$ maybe could hold a wildcard type,
-but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$.
-This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution.
+When it comes to wildcards there is a limitation we couldn't find a good workaround:
+\begin{example} This example does not work:

-This is our result:
-\begin{verbatim}
-class List<X> {
-    <Y extends X> void addTo(List<Y> l){
-        l.add(this.get());
-    }
+\noindent
+\begin{minipage}{0.51\textwidth}
+  \begin{lstlisting}[style=java]
+class Example{
+<A> Pair<A,A> make(List<A> l){...}
+<A> bool compare(Pair<A,A> p){...}
+
+  bool test(List<?> l){
+    return compare(make(l));
+  }
 }
-\end{verbatim}
-$
-\tv{l} \lessdotCC \exptype{List}{\wtv{y}},
-\type{X} \lessdot \wtv{y}
-$
-But the most general type would be:
-\begin{verbatim}
-class List<X> {
-    void addTo(List<? super X> l){
-        l.add(this.get());
-    }
-}
-\end{verbatim}
-
-\subsection{Discussion Pair Example}
-\begin{verbatim}
-<X> Pair<X,X> make(List<X> l){ ... }
-<X> boolean compare(Pair<X,X> p) { ... }
-
-List<?> l;
-Pair<?,?> p;
-
-compare(make(l)); // Valid
-compare(p); // Error
-\end{verbatim}
-
-Our type inference algorithm is not able to solve this example.
-When we convert this to \TamedFJ{} and generate constraints we end up with:
-\begin{lstlisting}[style=tamedfj]
-let m = let x = l in make(x) in compare(m)
 \end{lstlisting}
-\begin{constraintset}$
-\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
-\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
-\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
-\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
-$\end{constraintset}
+  \end{minipage}%
+  \hfill
+  \begin{minipage}{0.48\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}$@*),
+(*@$\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \ntv{r}$@*),
+(*@$\ntv{r} \lessdot \exptype{Pair}{\wtv{z}, \wtv{z}}$@*)
+\end{lstlisting}
+  \end{minipage}
+\end{example}
+
+%The algorithm can find a solution to every program which the Unify by Plümicke finds
+%a correct solution aswell.
+We will not infer intermediat types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$
+for a normal type placeholder.
+$\ntv{r}$ will get the type $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$
+which renders the constraint set unsolvable.
+
+% This is our result:
+% \begin{verbatim}
+% class List<X> {
+%     <Y extends X> void addTo(List<Y> l){
+%         l.add(this.get());
+%     }
+% }
+% \end{verbatim}
+% $
+% \tv{l} \lessdotCC \exptype{List}{\wtv{y}},
+% \type{X} \lessdot \wtv{y}
+% $
+% But the most general type would be:
+% \begin{verbatim}
+% class List<X> {
+%     void addTo(List<? super X> l){
+%         l.add(this.get());
+%     }
+% }
+% \end{verbatim}
+

 $\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
 from the constraint
@@ -71,63 +65,74 @@ $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.

 Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
-The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
+The correct substition for $\ntv{r}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
 But this leads to additional branching inside the \unify{} algorithm and increases runtime.
 %We refrain from using that type, because it is not denotable with Java syntax.
 %Types used for normal type placeholders should be expressable Java types. % They are not!
+This also just solves this specific issue and not the problem in general.

-The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.

-\begin{lstlisting}[style=letfj]
-let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
-\end{lstlisting}
+% The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.

-We can make it work with a special rule in the \unify{}.
-But this will only help in this specific example and not generally solve the issue.
-A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
-$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
-$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
-Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has 
-% TODO: how many supertypes are there?
-%X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <: 
-%X,Y,Z.Triple<X,Y,Z>
+% \begin{lstlisting}[style=letfj]
+% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
+% \end{lstlisting}

-% TODO example:
-\begin{lstlisting}[style=java]
-<X> Triple<X,X,X> sameL(List<X> l)
-<X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
-<X,Y> void triple(Triple<X,Y,Y> tr){}
+% We can make it work with a special rule in the \unify{}.
+% But this will only help in this specific example and not generally solve the issue.
+% A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
+% $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
+% $\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
+% Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has 
+% % TODO: how many supertypes are there?
+% %X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <: 
+% %X,Y,Z.Triple<X,Y,Z>

-Pair<?,?> p ...
-List<?> l ...
+% % TODO example:
+% \begin{lstlisting}[style=java]
+% <X> Triple<X,X,X> sameL(List<X> l)
+% <X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
+% <X,Y> void triple(Triple<X,Y,Y> tr){}

-make(t) { return t; }
-triple(make(sameP(p)));
-triple(make(sameL(l)));
-\end{lstlisting}
+% Pair<?,?> p ...
+% List<?> l ...

-\begin{constraintset}
-$
-\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
-\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
-(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
-$
-% Triple<X,X,X> <. t
-% ( Triple<X,Y,Y> <. t ) <- this constraint is added later
-% t <. Triple<a?, b?, b?>
+% make(t) { return t; }
+% triple(make(sameP(p)));
+% triple(make(sameL(l)));
+% \end{lstlisting}

-% t =. x.Triple<X,X,X>
-\end{constraintset}
+% \begin{constraintset}
+% $
+% \exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
+% \ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
+% (\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
+% $
+% % Triple<X,X,X> <. t
+% % ( Triple<X,Y,Y> <. t ) <- this constraint is added later
+% % t <. Triple<a?, b?, b?>
+
+% % t =. x.Triple<X,X,X>
+% \end{constraintset}


 \section{Conclusion and Further Work}
 % we solved the problems given in the introduction (see examples TODO give names to examples)
-The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}).
-As you can see by the given examples our type inference algorithm can calculate
-type solutions for programs involving wildcards.
+The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm. %(see examples \ref{example1} and \ref{example2}).
+Additionally we could prove that type solutions generated by our type inference algorithm are correct respective to \TamedFJ{}'s type rules.
+The important parts are lemma \ref{lemma:soundness} and \ref{lemma:unifySoundness}.
+They prove that the \unify{} algorithm solves a constraint set according to our subtyping rules
+and that the generated constraints match \TamedFJ{}'s type system.
+%As you can see by the given examples our type inference algorithm can calculate
+%type solutions for programs involving wildcards.

-Going further we try to prove soundness and completeness for \unify{}.
+The crucial parts introduced in this paper are capture constraints, wildcard placeholders and existential types.
+Those data structures allow us to solve the problems introduced in chapter \ref{challenges}.

+%Going further we try to prove soundness and completeness for \unify{}.
+Our algorithm is designed for extensibility with the final goal of full support for Java.
+\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.

 % The tricks are:
 % \begin{itemize}
--- a/constraints.tex
+++ b/constraints.tex
@@ -1,69 +1,3 @@
-\subsection{Capture Constraints}
-%TODO: General Capture Constraint explanation
-
-Capture Constraints are bound to a variable.
-For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
-$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
-This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
-Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
-creating the constraints \ref{lst:sameConstraints}.
-
-\begin{figure}
-  \begin{minipage}[t]{0.49\textwidth}
-    \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
-  List<?> v = ...;
-  
-  let x = v in 
-      let y = v in
-        concat(x, y) // Error!
-    \end{lstlisting}\end{minipage}
-    \hfill
-    \begin{minipage}[t]{0.49\textwidth}
-  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
-  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
-  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
-    \end{lstlisting}
-    \end{minipage}
-\end{figure}
-
-
-During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
-but they are not the same because they are each linked to a different let introduced variable.
-In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
-resulting in:
-%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
-\begin{displaymath}
-  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
-\end{displaymath}
-Thanks to the original annotations we can still see that those are different constraints.
-After \unify{} uses the \rulename{Capture} rule on those constraints
-it gets obvious that this constraint set is unsolvable:
-\begin{displaymath}
-  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
-\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
-\end{displaymath}
-
-%In this paper we do not annotate capture constraint with their source let statement.
-The rest of this paper will not annotate capture constraints with variable names.
-Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
-because we know that each of them originates from a different let statement.
-\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
-and has to allow doubles in the constraint set.
-
-% %We see the equality relation on Capture constraints is not reflexive.
-% A capture constraint is never equal to another capture constraint even when structurally the same
-% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
-% This is necessary to solve challenge \ref{challenge:1}.
-% A capture constraint is bound to a specific let statement.
-
-\textit{Note:}
-In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
-\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
-and we could actually delete one of them without loosing information.
-But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
-
-

 \section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
@@ -77,11 +11,6 @@ But this case will never occur in our algorithm, because the let statements for
 % But it can be easily adapted to Featherweight Java or Java.
 % We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T

-\begin{description}
-\item[input] \TamedFJ{} program in A-Normal form
-\item[output] Constraints
-\end{description}
-
 The constraint generation works on the \TamedFJ{} language.
 This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
 We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
@@ -145,7 +74,7 @@ $\begin{array}{lrcl}
 & \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2} 
 \end{array}$
 \end{center}
-\caption{ANF Transformation}\label{fig:anfTransformation}
+\caption{ANF Transformation $\tau$}\label{fig:anfTransformation}
 \end{figure}

 \begin{figure}
@@ -215,7 +144,7 @@ Those type variables count as regular types and can be held by normal type place
 \begin{figure}[tp]
  \begin{gather*}
    \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment }, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
              & \begin{array}{ll@{}l}
 \textbf{let} & \ol{\methodAssumption} =
                \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
@@ -237,11 +166,11 @@ Those type variables count as regular types and can be held by normal type place

 \begin{displaymath}
  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{e}.\texttt{f}, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{r} \ \text{fresh} \\
-                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
+                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \Gamma, \texttt{e}, \tv{r})\\
                    & \constraint = \begin{array}[t]{@{}l@{}l}
                      \orCons\set{
                      \set{ &
@@ -260,12 +189,12 @@ Those type variables count as regular types and can be held by normal type place

 \begin{displaymath}
  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
-                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\
-                    & \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, \expr{e}_1, \tv{e}_1)\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment } \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
                    & \constraint =
                      \set{
                      \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
@@ -278,7 +207,7 @@ Those type variables count as regular types and can be held by normal type place

 \begin{displaymath}
  \begin{array}{@{}l@{}l}
-      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
+      \typeExpr{} & ({\mtypeEnvironment}, \Gamma , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
      & \begin{array}{ll}
      \textbf{let}
      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
@@ -288,16 +217,55 @@ Those type variables count as regular types and can be held by normal type place
      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
      & \mathbf{where}\ \begin{array}[t]{l}
        \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
-        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
+        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment }
      \end{array}
                    
      \end{array}
      \end{array}
  \end{displaymath}
+
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , e_1 \elvis{} e_2, \tv{a}) = \\
+                & \begin{array}{ll}
+                    \textbf{let} 
+                    & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, e_1, \tv{r}_2)\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, \Gamma, e_2, \tv{r}_2)\\
+                    {\mathbf{in}} & {
+                    \consSet_1 \cup \consSet_2 \cup
+                        \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
+
+%We could skip wfresh here:
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , x, \tv{a}) = 
+    \mtypeEnvironment(x)
+  \end{array}
+\end{displaymath}
+
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
+                & \begin{array}{ll}
+                    \textbf{let} 
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \Gamma, \overline{e}, \ol{\ntv{r}}) \\
+                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
+                    {\mathbf{in}} & {
+                    \overline{\consSet} \cup
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
 \\[1em]
 \noindent
-\textbf{Example:}
-\begin{verbatim}
+\begin{example}
+Given the following input program missing type annotations for the \texttt{example} method:
+\begin{lstlisting}[style=java]
 class Class1{
  <A> A head(List<X> l){ ... }
  List<? extends String> get() { ... }
@@ -308,7 +276,7 @@ class Class2{
    return c1.head(c1.get());
  }
 }
-\end{verbatim}
+\end{lstlisting}
 %This example comes with predefined type annotations.
 We assume the class \texttt{Class1} has already been processed by our type inference algorithm
 leading to the following type annotations:
@@ -324,7 +292,8 @@ leading to the following type annotations:
 At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
 Afterwards the the \fjtype{} algorithm is able to generate constraints.

-\begin{minipage}{0.45\textwidth}
+\noindent
+\begin{minipage}{0.52\textwidth}
  \begin{lstlisting}[style=tamedfj]
 class Class2 {
  example(c1) = let x = c1 in
@@ -333,42 +302,33 @@ class Class2 {
 \end{lstlisting}
      \end{minipage}%
      \hfill
-      \begin{minipage}{0.5\textwidth}
-\begin{constraintset}
-$
-    \begin{array}{l}
-      \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
-    \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
-    \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\
-    \tv{xp} \lessdotCC \exptype{List}{\wtv{a}}
-    \end{array}
-$
-  \end{constraintset}
+      \begin{minipage}{0.46\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
+(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
+(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}$@*),
+(*@$\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}$@*)
+\end{lstlisting}
 \end{minipage}

 Following is a possible solution for the given constraint set:

+\noindent
 \begin{minipage}{0.55\textwidth}
-  \begin{lstlisting}[style=letfj]
+  \begin{lstlisting}[style=tamedfj]
 class Class2 {
-  example(c1) = let x : Class1 = c1 in
-    let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
-      in x.m(xp);
+ example(c1) = let x :Class1 = c1 in
+  let xp :(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
+   in x.m(xp);
 }
 \end{lstlisting}
      \end{minipage}%
      \hfill
-      \begin{minipage}{0.4\textwidth}
-\begin{constraintset}
-$
-    \begin{array}{l}
-    \sigma(\ntv{x}) = \type{Class1} \\
-    %\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
-    %\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
-    \sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
-    \end{array}
-$
-  \end{constraintset}
+      \begin{minipage}{0.43\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\sigma(\ntv{x}) = \type{Class1}$@*),
+(*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
+  \end{lstlisting}
 \end{minipage}

 For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
@@ -378,6 +338,7 @@ This is possible, because we deal with a capture constraint.
 The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
 which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
 Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
+\end{example}

 The wildcard placeholders are not used as parameter or return types of methods.
 Or as types for variables introduced by let statements.
@@ -387,44 +348,6 @@ This practice hinders free variables to leave their scope.
 The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
 cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.

-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
-                & \begin{array}{ll}
-                    \textbf{let} 
-                    & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
-                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
-                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\
-                    {\mathbf{in}} & {
-                    \consSet_1 \cup \consSet_2 \cup
-                        \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
-                  \end{array} 
-  \end{array}
-\end{displaymath}
-
-%We could skip wfresh here:
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = 
-    \mtypeEnvironment(x)
-  \end{array}
-\end{displaymath}
-
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
-                & \begin{array}{ll}
-                    \textbf{let} 
-                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
-                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
-                    {\mathbf{in}} & {
-                    \overline{\consSet} \cup
-                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
-                  \end{array} 
-  \end{array}
-\end{displaymath}
-
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}

@@ -507,4 +430,8 @@ cannot be used anywhere else then inside the constraints generated by the method
 %  \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
 % \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
 % \end{array}
-% \end{displaymath}
+% \end{displaymath}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:
--- a/helpers.tex
+++ b/helpers.tex
@@ -0,0 +1,34 @@
+
+\section{Additional Functions}
+\begin{description}
+\item[$\tph{}$] returns all type placeholders inside a given type.
+
+\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
+
+%\textbf{Wildcard renaming}\\
+\item[Wildcard renaming:]
+The \rulename{Reduce} rule separates wildcards from their environment.
+At this point each wildcard gets a new and unique name.
+To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
+($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
+\begin{align*}
+  [\type{A}/\type{B}]\type{B} &= \type{A} \\
+  [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
+  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
+  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
+\end{align*}
+\item[Free Variables:]
+The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
+% TODO: describe a function which determines free variables? or do an example?
+\begin{align*}
+\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
+\text{fv}(\tv{a}) &= \emptyset \\
+%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
+\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
+\end{align*}
+
+\item[Fresh Wildcards:]
+$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
+The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
+which are used for the upper and lower bounds.
+\end{description}
--- a/introduction.tex
+++ b/introduction.tex
@@ -59,8 +59,10 @@ is scope for a global type inference algorithm that infers
 method signatures even if no type information (except class headers
 and types of field variables) is given.
 We present such a global type inference algorithm for Featherweight
-Generic Java with wildcards. The same approach can also be used for
-regular Java programs. 
+Generic Java with wildcards, a Java core calculus with generics and
+wildcards in the tradition of Featherweight Java \cite{FJ} and its
+extensions \cite{WildFJ,WildcardsNeedWitnessProtection}. Our approach can also be used for regular Java programs,
+but we limit the formal presentation to this core calculus.

 %The goal is to find a correct typing for a given Java program.
 Our algorithm enables programmers to write Java code with only a
@@ -69,15 +71,17 @@ variables), it can fill in missing type annotations in partially
 type-annotated programs, and it can suggest better (more general)
 types for ordinary, typed Java programs.

+Listing~\ref{lst:intro-example-typeless} shows an example input of a
+method implementation without any type annotation. Our algorithm
+infers the type annotations in Listing~\ref{lst:intro-example-typed}:
+it adds the type arguments to \texttt{List} at object creation and it
+infers the most specific return type \texttt{List<?>}, which is a
+wildcard type. Our algorithm is the first to infer wildcard types that
+comes with a soundness proof.
+Previous work on global type inference for Java either does not
+consider wildcards or it simplifies the problem by not modeling key
+features of Java wildcards.

-\textbf{TO BE CONTINUED}
-
-
-We propose a global type inference algorithm for Java supporting Wildcards and proven sound.
-Global type inference allows input programs without any type annotations.
-A programmer could write Java code without stressing about types and type annotations which
-are infered and inserted by our algorithm.
-%This leads to better types (Poster referenz)

 %The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in listing \ref{lst:intro-example-typeless}.
 %In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst:intro-example-typed}.
@@ -86,7 +90,7 @@ are infered and inserted by our algorithm.
 %The last step to create a type inference algorithm compatible to the Java type system.


-\begin{figure}
+\begin{figure}[tp]
 \begin{minipage}{0.43\textwidth}
 \begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
 genList() {
@@ -113,57 +117,52 @@ List<?> genList() {
 \end{figure}
  

-\subsection{Comparision to similar Type Inference Algorithms}
-To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
-\begin{description}
-    \item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
-The type inference algorithm presented here supports Java Wildcards.
-% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
-% implication rules that follow the subtyping rules directly. Easy to understand soundness proof
-% capture conversion is needed
-\textit{Example:} The type inference algorithm for Generic Featherweight Java produces \texttt{Object} as the return type of the
-\texttt{genBox} method in listing \ref{lst:intro-example-typeless}
-whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}
-involving a wildcard type.
-\item[Type Unification for Java with Wildcards]
-An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
-but exposes some errors when it comes to method invocations.
-Especially the challenges shown in chapter \ref{challenges} are handled incorrectly.
-The main reasons are that Plümickes algorithm only supports types which are expressible in Java syntax
-and its soundness is proven towards a self-defined subtype ordering, but never against a complete type system.
-It appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
-We resolve this by denoting Java wildcards as existential types
-and introducing a second kind of subtype constraint. %, the current state of the art
+
+Global Type Inference for Featherweight Java \cite{TIforFGJ} is a
+sound, but incomplete inference algorithm for Featherweight Generic
+Java. It does not support wildcards, which means that it infers the
+return type \texttt{Object} for the method \texttt{genList} in
+Listing~\ref{lst:intro-example-typeless}. Like our algorithm, their
+algorithm restricts to monomorphic recursion, which leads to
+incompleteness. 
+
+
+A type unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
+but it does not handle capture conversion correctly because it only supports types which are expressible in Java syntax (more details in
+section~\ref{challenges}).  
+Moreover, it appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
+We resolve this problem by modeling Java wildcards as existential
+types \cite{WildFJ,WildcardsNeedWitnessProtection}, which also serve
+as the basis of our soundness proof.
+% forces us to define a new kind of subtype constraint. %, the current state of the art
 %and is able to deal with types that are not directly denotable in Java. 
-Additionally the soundness of our algorithm is proven using a Featherweight Java calculus \cite{WildFJ}.
+

 %The algorithm presented in this paper is able to solve all those challenges correctly
 %and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}.
 %But they are all correctly solved by our new type inference algorithm presented in this paper.

-\item[Java Type Inference]
-Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
-which only works for local environments where the surrounding context has known types.
-But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
-We will show the different capabilities with an example.
-In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
-its type parameters.
-Java is using a matching algorithm \cite{javaTIisBroken} to replace \texttt{T} with \texttt{String} 
-resulting in the correct expected type \texttt{List<String>}.
-%The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
-%because the expected return type is known. \texttt{List<String>} in this case.
-\begin{lstlisting}[caption=Extract of a valid Java program, label=lst:tiExample]
+
+\begin{lstlisting}[caption=Part of a valid Java program, style=tfgj, label=lst:tiExample,float=tp]
 <T> List<T> emptyList() { ... }

 List<String> ls = emptyList();
 \end{lstlisting}
-
-%\textit{Local Type Inference limitations:}
-Note that local type inference depends on the type annotation on the left side of the assignment.
-When calling the \texttt{emptyList} method without this type context its return value will be set to a \texttt{List<Object>}.
-The Java code snippet in \ref{lst:tiLimit} is incorrect, because \texttt{emptyList()} returns
-a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
-\begin{lstlisting}[caption=Limitations of Java's Type Inference, label=lst:tiLimit]
+Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
+which only works for local environments where the surrounding context has known types.
+The example in Listing~\ref{lst:tiExample} exhibits the main differences to our global type inference algorithm.
+The method call \texttt{emptyList} lacks its type parameters.
+Java relies on a matching algorithm \cite{javaTIisBroken} to instantiate \texttt{T} with \texttt{String} 
+resulting in the correct expected type \texttt{List<String>}.
+This local type inference depends on the type annotation on the left side of the assignment.
+When calling the \texttt{emptyList} method without this type context
+its return value will be inferred as \texttt{List<Object>}.
+Therefore, Java rejects the code snippet in Listing~\ref{lst:tiLimit}:
+it infers the type  \texttt{List<Object>} for
+\texttt{emptyList()} instead of the required
+$\exptype{List}{\exptype{List}{String}}$. 
+\begin{lstlisting}[caption=Limitations of Java's Type Inference,
+  label=lst:tiLimit, float=tp]
 emptyList().add(new List<String>())
    .get(0)
    .get(0); //Typing Error
@@ -172,14 +171,12 @@ emptyList().add(new List<String>())
 %List<A> <: List<B>, B <: List<C> 
 % B = A and therefore A on the left and right side of constraints.
 % this makes matching impossible
-The second call to \texttt{get} produces a type error, because Java expects \texttt{emptyList} to return
-a \texttt{List<Object>}.
-The type inference algorithm presented in this paper will correctly replace the type parameter \texttt{T} of the \texttt{emptyList}
-method with \texttt{List<List<String>>} and proof this code snippet correct.
-The local type inference algorithm based on matching cannot produce this solution.
-Here our type inference algorithm based on unification is needed.
+Hence, the second call to \texttt{get} produces a type error.
+
+The type inference algorithm presented in this paper correctly instantiates the type parameter \texttt{T} of the \texttt{emptyList}
+method with \texttt{List<List<String>>} and render this code snippet correct.
+

-\end{description}
 % %motivate constraints: 
 % To solve this example our Type Inference algorithm will create constraints
 % $
@@ -197,20 +194,20 @@ Here our type inference algorithm based on unification is needed.
 % - Easy to implement
 % - Capture Conversion support
 % - Existential Types support
-Our contributions are
+We summarize our contributions:
 \begin{itemize}
 \item
-We introduce the language \tifj{} (chapter \ref{sec:tifj}).
-A Featherweight Java derivative including Generics, Wildcards and Type Inference.
+We introduce the language \tifj{} (section \ref{sec:tifj}), 
+a Featherweight Java derivative including generics, wildcards, and type inference.
 \item
-We support capture conversion and Java style method calls.
-This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
+  Our algorithm handles existential types in a form which is not
+  denotable by Java syntax \cite{aModelForJavaWithWildcards}. Thus, we support capture conversion and Java style method calls.
 \item
-We present a novel approach to deal with existential types and capture conversion during constraint unification.
-\item The algorithm is split in two parts. A constraint generation step and an unification step.
-Input language and constraint generations can be extended without altering the unification part.
+  We present a novel approach to deal with existential types and capture conversion during constraint unification.
+% \item The algorithm is split in two parts. A constraint generation step and an unification step.
+% Input language and constraint generations can be extended without altering the unification part.
 \item
-We prove soundness and aim for a good compromise between completeness and time complexity.
+  We prove soundness and aim for a good compromise between completeness and time complexity.
 \end{itemize}
 % Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
 % \begin{verbatim}
@@ -240,25 +237,25 @@ We prove soundness and aim for a good compromise between completeness and time c
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).

 \section{Java Wildcards}
+\label{sec:java-wildcards}

-Java has invariant subtyping for polymorphic types.
+As Java is an imperative language, subtyping for generic types is invariant.
 %but it incooperates use-site variance via so called wildcard types.
-A \texttt{List<String>} is not a subtype of \texttt{List<Object>}
-even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
-To make the type system more expressive Java incooperates use-site variance by allowing wildcards (\texttt{?}) in type annotations.
-For example a type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type) %with the wildcard \texttt{?} representing a placeholder for any type
+Even though \texttt{String} is subtype of \texttt{Object},
+a \texttt{List<String>} is not a subtype of \texttt{List<Object>}:
+because someone might store an  \texttt{Integer} in the list, which is
+compatible with \texttt{Object}, but not with \texttt{String} (see Listing~\ref{lst:invarianceExample}).
+
+Invariance is overly restrictive in read-only or write-only
+contexts. Hence, Java incooperates use-site variance by allowing wildcards (\texttt{?}) in types.
+For example, the type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type)
 is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
 %The \texttt{?} is a wildcard type which can be replaced by any type as needed.
+%
+Listing~\ref{lst:wildcardIntro} shows a use of wildcards that renders the assignment \texttt{lo = ls} correct.
+The program still does not compile, because the addition of an \texttt{Integer} to \texttt{lo} is still incorrect.

-%Class instances in Java are mutable and passed by reference.
-Subtyping must be invariant in Java otherwise the integrity of data classes like \texttt{List} cannot be guaranteed.
-See listing \ref{lst:invarianceExample} for example
-where an \texttt{Integer} would be added to a list of \texttt{String}
-if not for the Java type system which rejects the assignment \texttt{lo = ls}.
-Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct.
-The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java.
-
-\begin{figure}
+\begin{figure}[tp]
 \begin{minipage}{0.48\textwidth}
 \begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
 List<String> ls = ...;
@@ -278,14 +275,13 @@ lo.add(new Integer(1)); // error!
 \end{minipage}
 \end{figure}

-Wildcard types are virtual types.
-There is no instantiation of a \texttt{List<?>}.
-It is a placeholder type which can hold any kind of list like
+Wildcard types like \texttt{List<?>} are virtual types, i.e., the run-time 
+type of an object is always a fully instantiated type like
 \texttt{List<String>} or \texttt{List<Object>}.
-This type can also change at any given time, for example when multiple threads
-share a reference to the same field.
-A wildcard \texttt{?} must be considered a different type everytime it is accessed.
-Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect.
+The issue is that the run-time type underlying a wildcard type can
+change at any time, for example when multiple threads share a reference to the same field.
+Hence, a wildcard \texttt{?} must be considered a different type everytime it is accessed.
+For that reason, the  call to the method \texttt{concat} with two wildcard lists in Listing~\ref{lst:concatError} is rejected.
 % The \texttt{concat} method does not create a new list,
 % but adds all elements from the second argument to the list given as the first argument.
 % This is allowed in Java, because both lists are of the polymorphic type \texttt{List<X>}.
@@ -293,50 +289,52 @@ Therefore calling the method \texttt{concat} with two wildcard lists in the exam
 % if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X}
 % of the \texttt{concat} function with \texttt{?}.

-\begin{figure}
+\begin{figure}[tp]
 \begin{lstlisting}[caption=Wildcard Example with faulty call to a concat method,label=lst:concatError]{java}
 <X> List<X> concat(List<X> l1, List<X> l2){
    return l1.addAll(l2);
 }

-List<String> ls = new List<String>();
-
-List<?> l1 = ls;
+List<?> l1 = new List<String>("foo");
 List<?> l2 = new List<Integer>(1); // List containing Integer

 concat(l1, l2); // Error! Would concat two different lists
 \end{lstlisting}
 \end{figure}

-To determine the correctness of method calls involving wildcard types Java's typecheck
-makes use of a concept called \textbf{Capture Conversion}.
+To determine the correctness of method calls involving wildcard types Java's typechecker
+makes use of a concept called \textbf{capture conversion}.
 %  was designed to make Java wildcards useful.
 % - without capture conversion 
 % - is used to open wildcard types
 % - 
-This process was formalized for Featherweight Java \cite{FJ} by replacing existential types with wildcards and capture conversion with let statements \cite{WildcardsNeedWitnessProtection}.
-We propose our own Featherweight Java derivative called \TamedFJ{} defined in chapter \ref{sec:tifj}.
-To express the example in listing \ref{lst:wildcardIntro} with our calculus we first have to translate the wildcard types:
-\texttt{List<? extends Object>} becomes $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
-The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
-and a type they are bound to.
-In this case the name is $\rwildcard{A}$ with the upper bound $\type{Object}$ and it's bound to the the type \texttt{List}.
-Before we can call the \texttt{add} method on this type we have to add a capture conversion via let statement:
+One way to formalize this concept is by replacing wildcards with
+existential types and modeling capture conversion with suitably
+inserted let statements \cite{WildcardsNeedWitnessProtection}. 
+Our Featherweight Java derivative called \TamedFJ{} is modeled after
+Bierhoff's calculus \cite{WildcardsNeedWitnessProtection} (see section~\ref{sec:tifj}).
+To express the example in Listing~\ref{lst:wildcardIntro} in our calculus we first translate the wildcard types:
+\texttt{List<? extends Object>} becomes
+$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$,
+where the existentially bound variable \texttt{A} has a lower bound
+$\bot$ and an upper bound $\type{Object}$.
+Before we can call the \texttt{add} method on this type we perform
+capture conversion by inserting a let statement:
 \begin{lstlisting}
 let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
 \end{lstlisting}
-\expr{lo} is assigned to a new variable \expr{v} bearing the type $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$,
-but inside the let statement the variable \expr{v} will be treated as $\exptype{List}{\rwildcard{A}}$.
-The idea is that every Wildcard type is backed by a concrete type.
-By assigning \expr{lo} to a immutable variable \expr{v} we unpack the concrete type $\exptype{List}{\rwildcard{A}}$
-that was concealed by \expr{lo}'s existential type.
-Here $\rwildcard{A}$ is a fresh variable or a captured wildcard so to say.
-The only information we have about $\rwildcard{A}$ is that it is any type inbetween the bounds $\bot$ and $\type{Object}$
+The variable \expr{lo} (from Listing~\ref{lst:wildcardIntro}) is
+assigned to a new immutable variable \expr{v} with type
+$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$, 
+but inside the let statement the variable \expr{v} will be treated as
+$\exptype{List}{\rwildcard{A}}$. 
+Here $\rwildcard{A}$ is a fresh variable or a captured wildcard.
+The only information we have about $\rwildcard{A}$ is that it is a
+supertype of $\bot$ and a subtype of $\type{Object}$
 It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
-With this formalization it gets obvious why the method call to \texttt{concat}
-in listing \ref{lst:concatError} is irregular (see \ref{lst:concatTamedFJ}).
-
-\begin{figure}
+This approach also clarifies why the method call to \texttt{concat}
+in listing \ref{lst:concatError} is rejected (see Listing~\ref{lst:concatTamedFJ}).
+\begin{figure}[tp]
 \begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, label=lst:concatTamedFJ]
 let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in
    let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in
@@ -385,321 +383,3 @@ let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) =
 % Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
 % In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).

-
-\section{Global Type Inference Algorithm}
-
-\begin{figure}[h]
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
-<A> List<A> add(List<A> l, A v)
-
-List<? super String> l = ...;
-add(l, "String");
-\end{lstlisting}
-\end{minipage}\hfill
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
-<A> List<A> add(List<A> l, A v)
-List<? super String> l = ...;
-let v:(*@$\tv{v}$@*) = l
-    in add(v, "String");
-\end{lstlisting}
-\end{minipage}\\
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
-(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
-(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
-(*@$\type{String} \lessdot \wtv{a}$@*)
-\end{lstlisting}
-\end{minipage}\hfill
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
-<A> List<A> add(List<A> l, A v)
-List<? super String> l = ...;
-let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
-    in <X>add(l2, "String");
-\end{lstlisting}
-\end{minipage}
-\end{figure}
-
-% \begin{description}
-%     \item[input] \tifj{} program
-%     \item[output] type solution
-%     \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
-% \end{description}
-
-%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
-Listings \ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
-\ref{lst:addExampleSolution} showcase our global type inference algorithm step by step.
-In this example we know that the type of the variable \texttt{l} is an existential type and has to undergo a capture conversion
-before being passed to a method call.
-This is done by converting the program to A-Normal form \ref{lst:addExampleLet},
-which introduces a let statement defining a new variable \texttt{v}.
-Afterwards unknown types are replaced by type placeholders ($\tv{v}$ for the type of \texttt{v}) and constraints are generated (see \ref{lst:addExampleCons}).
-These constraints mirror the type rules of our \TamedFJ{} calculus.
-% During the constraint generation step the type of the variable \texttt{v} is unknown
-% and given the type placeholder $\tv{v}$.
-The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
-Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint
-expressing that the left side of the constraint is subject to a capture conversion.
-Now our unification algorithm \unify{} (defined in chapter \ref{sec:unify}) is used to solve these constraints.
-In the starting set of constraints no type is assigned to $\tv{v}$ yet.
-During the course of \unify{} more and more types emerge.
-As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed.
-%The constraints where this is possible are marked as capture constraints.
-In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints:
-
-\begin{displaymath}
-\prftree[r]{Capture}{
-\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
-}{
-\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
-}
-\end{displaymath}
-
-%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
-%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
-The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
-allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
-Leaving us with the solution $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot \rwildcard{Y}$
-The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
-because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
-
-
-A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleSolution}.
-This program can be deducted from the type solution of our \unify{} algorithm presented in chapter \ref{sec:unify}.
-In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
-becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
-a type parameter to method call \texttt{<X>add(v, "String")}.
-
-% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
-% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
-% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
-% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
-% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
-% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
-% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
-% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
-% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
-
-% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
-% We try to keep the branching at a minimal amount to improve runtime behavior.
-% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
-% There are no informal parts in our \unify{} algorithm.
-% It solely consist out of transformation rules which are bound to simple checks.
-
-\subsection{Challenges}\label{challenges}
-%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
-
-% Wildcards are not reflexive.
-% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
-
-% do not substitute free type variables
-
-Global Type inference for Featherweight Java with generics but without wildcards is solved already.
-But adding Wildcards to the calculus creates new problems we did not foresee
-and which have not been recognized by an existing type unification algorithm for Java with wildcards \ref{plue09_1}.
-% what is the problem?
-% Java does invisible capture conversion steps 
-Java Wildcard types are represented as existential types and have to be opened before they can be used.
-This can either be done implicitly (\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or explicitly via let statements (\cite{WildcardsNeedWitnessProtection}).
-For all of those variations it is vital to know the argument types with which a method is called.
-But our input program does not contain any type annotations.
-We do not know where an existential type will emerge and where a capture conversion is necessary.
-This has to be figured out during the type inference algorithm.
-We detected three main challenges related to Java Wildcards and Global Type Inference:
-\begin{enumerate}
-\item \label{challenge:1}
-One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
-and rejects the program in listing \ref{lst:concatError}.
-The first one is a valid Java program,
-because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}.
-Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$
-it is safe to pass \texttt{"String"} for the first parameter of the function.
-
-The second program shown in listing \ref{lst:concatError} is incorrect.
-The method call to \texttt{concat} with two wildcard lists is unsound.
-Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
-The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}):
-\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
-$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
-For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
-exists to satisfy
-$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
-\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
-
-% \textbf{Solution:}
-% Capture Conversion during Unify.
-
-\item 
-\unify{} morphs a constraint set into a correct type solution
-gradually assigning types to type placeholders during that process.
-Solved constraints are removed and never considered again.
-In the following example \unify{} solves the constraint generated by the expression
-\texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
-\begin{verbatim}
-anyList() = new List<String>() :? new List<Integer>()
-
-add(anyList(), anyList().head());
-\end{verbatim}
-The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
-Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
-\texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
-An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-is solved by removing the wildcard $\rwildcard{X}$ if possible.
-
-this problem is solved by ANF transformation
-
-\item
-% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
-% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
-The program in listing \ref{shuffleExample} shows a challenge involving wildcards and subtyping.
-The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has the type
-$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
-Whereas $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
-$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ representing a list of lists, all of the same type $\rwildcard{X}$,
-and can savely be passed to \texttt{shuffle}.
-This behavior can also be explained by looking at the types and their capture converted versions:
-\begin{center}
-\begin{tabular}{l | l | l}
-Java type & \TamedFJ{} representation & Capture Conversion \\
-\hline
-$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
-$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
-%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
-\end{tabular}
-\end{center}
-%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
-%One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
-%A wildcard in the Java syntax has no name and is bound to its enclosing type:
-%$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-%During type checking \emph{intermediate types}
-%can emerge, which have no equivalent in the Java syntax.
-
-\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
-class List<X> extends Object {...}
-class List2D<X> extends List<List<X>> {...}
-
-<X> void shuffle(List<List<X>> list) {...}
-
-List<List<?>> l = ...;
-List2D<?> l2d = ...;
-
-shuffle(l); // Error
-shuffle(l2d); // Valid
-\end{lstlisting}
-% Java is using local type inference to allow method invocations which are not describable with regular Java types.
-% The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
-% which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
-% After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
-% and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
-% \begin{lstlisting}[style=TamedFJ]
-% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
-% \end{lstlisting}
-
-% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
-% \begin{constraintset}
-% \begin{center}
-%     $
-%     \begin{array}{l}
-%     \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
-%     \\
-%     \hline
-%     \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
-%     \\
-%     \hline
-%     \textit{Capture Conversion:}\ 
-%     \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
-%     \\
-%     \hline
-%     \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
-%     \end{array}
-%     $
-% \end{center}
-% \end{constraintset}
-
-Given such a program our type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
-decline the call to \texttt{shuffle(l)}.
-
-% The method call \texttt{shuffle(l)} is invalid however,
-% because \texttt{l} has the type
-% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-% There is no solution for the subtype constraint:
-% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
-
-\item \label{challenge3} \textbf{Free Variables cannot leaver their scope}:
-Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
-%When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
-and the following input program:
-
-\noindent
-\begin{minipage}{0.62\textwidth}
-\begin{lstlisting}
-let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
-\end{lstlisting}\end{minipage}
-  \hfill
-\begin{minipage}{0.36\textwidth}
-  \begin{lstlisting}[style=constraints]
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
-(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
-  \end{lstlisting}
-\end{minipage}
-% the variable z has to 
-
-Take the Java program in listing \ref{lst:mapExample} for example.
-It maps every element of a list
-$\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
-to a polymorphic \texttt{id} method.
-We want to use our \unify{} algorithm to determine the correct type for the
-variable \expr{l2}.
-Although we do not specify constraint generation for language constructs like
-lambda expressions used in this example,
-we can imagine that the constraints have to look something like this:
-
-\begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
-<X> List<X> id(List<X> l){ ... }
-List<List<?>> ls;
-l2 = l.map(x -> id(x));
-\end{lstlisting}\end{minipage}
-\hfill
-\begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
-(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
-(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
-(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
-\end{lstlisting}
-\end{minipage}
-
-The constraints
-$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
-\exptype{List}{\wtv{x}} \lessdot \tv{z}$
-stem from the body of the lambda expression
-\texttt{id(x)}.
-\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
-\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
-
-The T-Let rule prevents us from using free variables created by the method call to \expr{id}
-to be used in the return type $\tv{z}$.
-But this has to be signaled to the \unify{} algorithm, which does not know about the origin and context of
-the constraints.
-If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
-the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$.
-This type solution is unsound.
-The type of \expr{l2} is the same as the one of \expr{l}:
-$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
-
-\textbf{Solution:}
-We solve this by distinguishing between wildcard placeholders and normal placeholders.
-$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
-
-\end{enumerate}
-
-%TODO: Move this part. or move the third challenge some underneath.
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "TIforWildFJ"
-%%% End:
--- a/prolog.tex
+++ b/prolog.tex
@@ -132,6 +132,7 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
+\newcommand{\cctv}[1]{\ensuremath{\tv{#1}_!}}
 \newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
 %\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
--- a/relatedwork.tex
+++ b/relatedwork.tex
@@ -63,14 +63,14 @@ indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \
 algorithm for this type system, which he proved as sound and complete. 

 The problem of his type system is in the lossing reflexivity as shown in
-example \ref{intro-example1}. First approaches to solve this problem he gave in
+example \ref{lst:intro-example-typeless}. First approaches to solve this problem he gave in
 \cite{plue24_1}, where he fixes that no pairwise different nodes in the
 abstract syntax gets the same type variable and that no pairwise different type
 variables are equalized. In \cite{PH23} he showed how his type inference
 algorithm suffices theese properties.

-In Pl\"umicke's work there is indeed a formal definition of the subtying
-ordering and a correctness proof of the type unification algorithms but no
-soundness proof of the type system, itself. Therefore we choose for our type
-inference algorithms with wildcars the approach of ???????
+% In Pl\"umicke's work there is indeed a formal definition of the subtying
+% ordering and a correctness proof of the type unification algorithms but no
+% soundness proof of the type system, itself. Therefore we choose for our type
+% inference algorithms with wildcars the approach of ???????

--- a/soundness.tex
+++ b/soundness.tex
@@ -1,124 +1,115 @@
 \section{Soundness}

-\begin{lemma}
-A sound TypelessFJ program is also sound under LetFJ type rules.
-\begin{description}
-    \item[if:]
-$\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
-\end{description}
-\end{lemma}
+% \begin{lemma}
+% A sound TypelessFJ program is also sound under LetFJ type rules.
+% \begin{description}
+%     \item[if:]
+% $\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
+% \end{description}
+% \end{lemma}

-TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
-Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
-%what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
-% if the Y is later needed for an equals: same(id(x), x2)
-Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
-Or it is a generic method call: is it possible to use any free wildcards here?
-let empty 
+% TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+% Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
+% %what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
+% % if the Y is later needed for an equals: same(id(x), x2)
+% Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
+% Or it is a generic method call: is it possible to use any free wildcards here?
+% let empty 

-<X> Box<X> empty()
-same(Box<?>, empty())
-let p1 : X.Box<X> = Box<?> in let 
-X.Box<X> <. Box<x> 
-Box<e> <. Box<x>
+% <X> Box<X> empty()
+% same(Box<?>, empty())
+% let p1 : X.Box<X> = Box<?> in let 
+% X.Box<X> <. Box<x> 
+% Box<e> <. Box<x>

-boxin(empty()), Box2<?>
+% boxin(empty()), Box2<?>

-Where can a problem arise? When we use free wildcards before they are freed.
-But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
-Here y = Y and x = X but 
+% Where can a problem arise? When we use free wildcards before they are freed.
+% But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
+% Here y = Y and x = X but 

-<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
-<X> Pair<?, X> left() { return null; }
-<X> Pair<X, ?> right() { return null; }
+% <X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
+% <X> Pair<?, X> left() { return null; }
+% <X> Pair<X, ?> right() { return null; }

-<X> Box<X> id(Box<? extends Box<X>> x)
-here it could be beneficial to use a free wildcard as the parameter X to have it later
-Box<?> x = ...
-same(id(x), id(x)) <- this will be accepted by TI
+% <X> Box<X> id(Box<? extends Box<X>> x)
+% here it could be beneficial to use a free wildcard as the parameter X to have it later
+% Box<?> x = ...
+% same(id(x), id(x)) <- this will be accepted by TI

-let left : X,Y.Pair<X,Y> = left() in
- let right : Pair<X,Y> = right() in
+% let left : X,Y.Pair<X,Y> = left() in
+%  let right : Pair<X,Y> = right() in

-Compromise:
- Generate constraints so that they comply with LetFJ
- Propose a version which is close to Java
+% Compromise:
+% - Generate constraints so that they comply with LetFJ
+% - Propose a version which is close to Java

-Version for LetFJ:
-Is it still possible to do the capture conversion in form of constraints?
-X.C<X> <. C<x>
-T <. X.C<X>
-how to proof: X.C<X> ok
+% Version for LetFJ:
+% Is it still possible to do the capture conversion in form of constraints?
+% X.C<X> <. C<x>
+% T <. X.C<X>
+% how to proof: X.C<X> ok


-If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
-then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
-This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
+% If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+% then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
+% This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.


-Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
+% Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.

-\textit{Proof} by structural induction.
-\begin{description}
-    \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
-    $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
-    and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
+% \textit{Proof} by structural induction.
+% \begin{description}
+%     \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
+%     $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
+%     and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.

-$|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
+% $|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$

-\item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
-\item[$\texttt{e}.f$] given let x : T = e' in x 
-let x : T = e' in let xf = x.f in xf
+% \item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
+% \item[$\texttt{e}.f$] given let x : T = e' in x 
+% let x : T = e' in let xf = x.f in xf

-Required:
-$ \Delta | \Theta \vdash e' : \type{T}_1$
-$\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
-$\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
+% Required:
+% $ \Delta | \Theta \vdash e' : \type{T}_1$
+% $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
+% $\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$

-\end{description}
+% \end{description}


-\textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
-First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
-m(p) = e => let xp = p in [xp/p]e
-x1.m(x2) => let xm = x1.m(x2=) in xm
-x.f => let xf = x.f in xf
-Then we have to proof there is never a wildcard used before it is declared.
-Wildcards are introduced by the capture conversions and nothing else.
+% \textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
+% First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
+% m(p) = e => let xp = p in [xp/p]e
+% x1.m(x2) => let xm = x1.m(x2=) in xm
+% x.f => let xf = x.f in xf
+% Then we have to proof there is never a wildcard used before it is declared.
+% Wildcards are introduced by the capture conversions and nothing else.


-\begin{theorem}\label{testenv-theorem}
-Type inference produces a correctly typed program.
-\begin{description}
-    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
-    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
-    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
-    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
-    with $\ol{M} = $
-\end{description}
-\end{theorem}
+% \begin{lemma}{Well-formedness:}
+% TODO: 
+% \end{lemma}

-\begin{lemma}{Well-formedness:}
-TODO: 
-\end{lemma}
-
-\begin{lemma}{Soundness:}
+\begin{lemma}{Soundness:}\label{lemma:soundness}
    \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
    \begin{description}
-    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
-    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$
+    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
+    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ % and let $\Delta= \Delta_u \cup \Delta'$
+%    $\Delta, \Delta' \vdash $
 %    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
 %    and $\vdash \ol{L} : \mtypeEnvironment{}$
 %    and $\Gamma \subseteq \mtypeEnvironment{}$
 %    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
 %    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
-    \item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
+    %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
+    \item[then] $\Delta,\Delta'|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
    \end{description}
 \end{lemma}
-Regular type placeholders represent type annotations.
-These are the only types a \wildFJ{} program needs to be correctly typed.
-The type placeholders flagged as wildcard placeholders are intermediate types
-used in let statements and as type parameters for generic method calls.
+% Regular type placeholders represent type annotations.
+% These are the only types a \wildFJ{} program needs to be correctly typed.
+% The type placeholders flagged as wildcard placeholders are intermediate types
+% used in let statements and as type parameters for generic method calls.

 %Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
 % only used inside the constraint the wildcard variable occurs
@@ -129,24 +120,45 @@ used in let statements and as type parameters for generic method calls.
 \textit{Proof:}
 By structural induction over the expression $\texttt{e}$. 
 \begin{description}
-    \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
-    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
-    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
-    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
-    %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
+    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
+    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
+    $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
+        $\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
+        $\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
+        The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
+        We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
+        Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
+        and $\Delta, \Delta' \vdash  \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
+        given the constraint $\tv{e}_2 \lessdot \tv{a}$.
+    \item[$\expr{v}.\texttt{f}$]
+        We are alowwed to use capture conversion for $\expr{v}$ here.
+        $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
+        $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
+        $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
+    because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
+    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
+    % \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$] 
+    % $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
+    % $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
+    % $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
+    % \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
+    % then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
+    % $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
+    % %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
+    % %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
    
-    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
+    % The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
    
-    We now show
-    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
-    by the T-Field rule.
-    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
-    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
-    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
-    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
-    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
+    % We now show
+    % $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
+    % by the T-Field rule.
+    % $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
+    % $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
+    % because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
+    % $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
+    % and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.

-    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
+    % $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.

    % X.List<X> <. List<a?>
    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
@@ -157,77 +169,90 @@ By structural induction over the expression $\texttt{e}$.
    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok

    % If S ok and T <. S , then Unify generates a T ok
-    S typeinference:
-    T <: [S/Y]U
-    We apply the following lemma
-    Lemma
-    if T ok and T <: S then S ok

-    until
-    T = [S/Y]U
+    % S typeinference:
+    % T <: [S/Y]U
+    % We apply the following lemma
+    % Lemma
+    % if T ok and T <: S then S ok

-    and then we can say by 
-    Lemma:
-    If [S/Y]U ok then S ok (TODO: proof!)
+    % until
+    % T = [S/Y]U

-    So we do not have to proof S ok (but T)
+    % and then we can say by 
+    % Lemma:
+    % If [S/Y]U ok then S ok (TODO: proof!)

-    % T_r <: C<T> (S is in T)
-    % Is C<T> ok?
-    % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
-    % this together with the X <. N constraints proofs T_r ok
+    % So we do not have to proof S ok (but T)

-    $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
-    %Easy, because unify only generates substitutions for normal type placeholders which are OK
+    % % T_r <: C<T> (S is in T)
+    % % Is C<T> ok?
+    % % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
+    % % this together with the X <. N constraints proofs T_r ok

-    \item[$\texttt{e}.\texttt{m}(\ol{e})$]
-Lets have a look at the case where the receiver and parameter types are all named types.
-So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
-and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
-and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in
+    % $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
+    % %Easy, because unify only generates substitutions for normal type placeholders which are OK

-$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
-\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
+    \item[$\texttt{v}.\texttt{m}(\ol{v})$]
+    Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
+    We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
+        \ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
+        \ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
+        and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
+        then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
+            \ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
+            \ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
+            which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
+            %TODO: why does this call succeed?
+% Lets have a look at the case where the receiver and parameter types are all named types.
+% So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
+% and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
+% and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in

-%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
-% and which is a supertype of T_r (so no free variables in T_r)
-% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
-% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
+% $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
+% \texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$

-By lemma \ref{lemma:unifyWeakening} we know that 
-$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
-has a solution.
-Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
-$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
-Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
-which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
+% %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
+% % and which is a supertype of T_r (so no free variables in T_r)
+% % Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
+% % This is possible because free variables (except those in \Delta_in) are never used in wildcard environments

-    This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
-    $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
-    $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
-    and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
-    are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
-    $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
-    $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
-    $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
-    therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
-    by lemma \ref{lemma:wfHereditary} and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
-    The same goes for $\wcNtype{\Delta'}{N}$.
+% %By lemma \ref{lemma:unifyWeakening}
+% We know that 
+% $\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
+% has a solution.
+% Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
+% $\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
+% Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
+% which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.

-    % \begin{gather}
-%         \label{sp:0}
-%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
-%         \label{sp:1}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
-%         \label{sp:2}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
-%         \label{sp:3}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
-%         \label{sp:4}
-%         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-%     \end{gather}
+%     This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+%     $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
+%     $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
+%     are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
+%     $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
+%     $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
+%     $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
+%     therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
+%     %by lemma \ref{lemma:wfHereditary}
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
+%     The same goes for $\wcNtype{\Delta'}{N}$.

-Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
+%     % \begin{gather}
+% %         \label{sp:0}
+% %         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
+% %         \label{sp:1}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
+% %         \label{sp:2}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
+% %         \label{sp:3}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
+% %         \label{sp:4}
+% %         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+% %     \end{gather}
+
+% Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).

 \end{description}

@@ -270,29 +295,47 @@ by induction over every step of the \unify{} algorithm.
 Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
 This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.

-\textit{Proof: (Variant 2)}
-The GenSigma and GenDelta rules check for well-formedness.
+% \textit{Proof: (Variant 2)}
+% The GenSigma and GenDelta rules check for well-formedness.
+
+
+\begin{lemma}\label{lemma:wildcardWellFormedness}
+\unify{} generates well-formed existential types
+\begin{description}
+\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
+\item[and] $\forall \wcNtype{\Delta''}{N} \in C: \text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\item[and] $\sigma(\tv{a}) = \wcNtype{\Delta'}{N}$
+%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
+\item[then] $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\end{description}
+\end{lemma}
+\textit{Proof} is straightforward induction over the transformation rules of \unify{}
+under the assumption that all supplied existential types are satisfying the premise.
+All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
+with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
+Only the \rulename{Adapt} rule is able to produce types neglecting the premise,
+but is immediately corrected by the \rulename{Trim} rule.

 % All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
 % Both are well formed!

-\begin{lemma}\label{lemma:wfHereditary}
-    Well-formedness is hereditary
-    \begin{description}
-        \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
-        \item[Then] $\triangle \vdash \type{S} \ \ok$
-    \end{description}
-\end{lemma}
-\textit{Proof:}
+% \begin{lemma}\label{lemma:wfHereditary}
+%     Well-formedness is hereditary
+%     \begin{description}
+%         \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
+%         \item[Then] $\triangle \vdash \type{S} \ \ok$
+%     \end{description}
+% \end{lemma}
+% \textit{Proof} by induction on subtyping rules in figure \ref{fig:subtyping}

-\begin{lemma}
+% \begin{lemma}
    
-    \begin{description}
-        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
-        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
-    \end{description}
-\end{lemma}
-\textit{Proof:} by definition of WF-Class
+%     \begin{description}
+%         \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
+%         \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
+%     \end{description}
+% \end{lemma}
+% \textit{Proof:} by definition of WF-Class


 \begin{lemma} \label{lemma:tvsNoFV}
@@ -313,16 +356,29 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 % Delta |-  N <. T
 % \end{lemma}

-\begin{lemma} \label{lemma:unifyWeakening}
-Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
-If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
-\begin{description}
-    \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
-    \item[then] $ (\sigma', \Delta') = \unify{}( C')$
-\end{description}
+% \begin{lemma}\label{lemma:wildcardsStayInScope}
+% Free variables can only hop to another constraint if they share the same wildcard placeholder.
+% \begin{description}
+%     \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
+%     \item[and] $\tv{a}$ being a type placeholders used in $C$
+%     \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
+% \end{description}
+% \end{lemma}

-\end{lemma}
-\textit{Proof:}
+
+
+%TODO: use this to proof soundness. Wildcard placeholders are not shared with other constraints and therefore only the wildcards generated by capture conversion are used in a let statement.
+
+% \begin{lemma} \label{lemma:unifyWeakening}
+% Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
+% If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
+% \begin{description}
+%     \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$% and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
+%     \item[then] $ (\sigma', \Delta') = \unify{}( C')$
+% \end{description}
+
+% \end{lemma}
+%\textit{Proof:}
 %TODO
 % 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!
@@ -507,158 +563,195 @@ Same as Subst
 \end{description}


-\subsection{Converting to Wild FJ}
-Wildcards are existential types which have to be \textit{unpacked} before they can be used.
-In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
-The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
-Our type inference algorithm will accept an input program without let statements and add them where necessary.
+% \subsection{Converting to Wild FJ}
+% Wildcards are existential types which have to be \textit{unpacked} before they can be used.
+% In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
+% The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
+% Our type inference algorithm will accept an input program without let statements and add them where necessary.

-%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
-%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
+% %Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
+% %We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.

-Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
-They have been merged with let statements and simplified.
+% Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
+% They have been merged with let statements and simplified.

-The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
-are necessary for the soundness proof.
+% The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
+% are necessary for the soundness proof.

-%TODO: Show that well-formed implies witnessed!
-We change the type rules to require the well-formedness instead of the witnessed property.
-See figure \ref{fig:well-formedness}.
+% %TODO: Show that well-formed implies witnessed!
+% We change the type rules to require the well-formedness instead of the witnessed property.
+% See figure \ref{fig:well-formedness}.

-Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
-\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
-With \texttt{witnessed} being the stronger one.
-We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
-$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
-Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
-Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
+% Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
+% \cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
+% With \texttt{witnessed} being the stronger one.
+% We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
+% $\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
+% Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
+% Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.

-The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
-The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
-Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
-$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
+% The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
+% The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
+% Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
+% $\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.

-A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
-and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
+% A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
+% and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.

-\begin{figure}[tp]
-$\begin{array}{l}
-    \typerule{T-Var}\\
-    \begin{array}{@{}c}
-        x : \type{T} \in \Gamma
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash x : \type{T}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-New}\\
-    \begin{array}{@{}c}
-        \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
-        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
-        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
-        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
-        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
-        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-    \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-Field}\\
-    \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
-        \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-Call}\\
-    \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
-        \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
-        \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
-        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
-        \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-        \\
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
-        \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
-        {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-Elvis}\\
-    \begin{array}{@{}c}
-        \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad 
-        \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
-        \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
-        \Delta \vdash \type{T}_2 <: \type{T}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-        \typerule{T-Method}\\
-    \begin{array}{@{}c}
-        \text{dom}(\Delta)=\ol{X} \quad \quad
-        \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
-        \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
-        \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
-        \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad 
-        \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-        \typerule{T-Class}\\
-    \begin{array}{@{}c}
-        \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
-        \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
-        \Delta \vdash \type{N} \ \ok \quad \quad
-        \Delta \vdash \ol{M} \ \ok \texttt{ in C}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
-    \end{array}
-\end{array}$
-\caption{T-Call and T-Field} \label{fig:tletexpr}
-\end{figure}
+% \begin{figure}[tp]
+% $\begin{array}{l}
+%     \typerule{T-Var}\\
+%     \begin{array}{@{}c}
+%         x : \type{T} \in \Gamma
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash x : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-New}\\
+%     \begin{array}{@{}c}
+%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
+%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%     \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Field}\\
+%     \begin{array}{@{}c}
+%         \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad 
+%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+%         \textit{fields}(\type{N}) = \ol{U\ f} \\
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Call}\\
+%     \begin{array}{@{}c}
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+%         \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+%         \\
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+%         \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
+%         \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
+%         \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
+%         \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+%         \\
+%         \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+%         \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
+%         {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Elvis}\\
+%     \begin{array}{@{}c}
+%         \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad 
+%         \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
+%         \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
+%         \Delta \vdash \type{T}_2 <: \type{T}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%         \typerule{T-Method}\\
+%     \begin{array}{@{}c}
+%         \text{dom}(\Delta)=\ol{X} \quad \quad
+%         \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
+%         \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
+%         \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
+%         \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
+%         \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad 
+%         \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%         \typerule{T-Class}\\
+%     \begin{array}{@{}c}
+%         \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
+%         \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
+%         \Delta \vdash \type{N} \ \ok \quad \quad
+%         \Delta \vdash \ol{M} \ \ok \texttt{ in C}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
+%     \end{array}
+% \end{array}$
+% \caption{T-Call and T-Field} \label{fig:tletexpr}
+% \end{figure}

+
+\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} \doteq \type{S'} })$
+\item[Then] there exists a $\sigma'$ with: 
+
+\begin{itemize}
+\item $\sigma''(\overline{\cctv{x}}) = \overline{\wctype{\Delta''}{C}{\ol{T}}}$
+\item $\sigma' = \set{ \overline{\cctv{x}} \mapsto \overline{\exptype{C}{\ol{T}}} } \cup \sigma$
+\item $\Delta, \Delta', \overline{\Delta''} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\end{itemize}
+\end{description}
+\end{lemma}
+
+\textit{Proof:}
+For every step in the \unify{} algorithm:
+Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
+constraint set $C$ before the transformation.
+
+\unify{} terminates with $C = \emptyset$ for which the preposition holds:
+$\Delta \vdash \sigma(\emptyset)$
+
+We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
+the preposition holds for $C$ using the assumption that it holds for $C'$ :
+$\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
+
+\begin{description}
+\item[Reduce] Given $\wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
+we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
+\begin{itemize}
+\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
+\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
+\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
+
+\end{itemize}
+\end{description}
--- a/tRules.tex
+++ b/tRules.tex
@@ -5,24 +5,26 @@
 %Input language only described here. It is standard Featherweight Java
 % we use the transformation to proof soundness. this could also be moved to the end. 
 % the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
-We define our own calculus \TamedFJ{}, which is used as input aswell as output to our global type inference algorithm.
+This section defines the calculus \TamedFJ{}, which is used as input and output of our global type inference algorithm.
 %We assume that the input to our algorithm is a program, which carries none of the optional type annotations.
 %After calculating a type solution we can insert all missing types and generate a correct program.
 %The input to our algorithm is a typeless version of Featherweight Java.
-The syntax is shown in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
-The respective type rules are defined by figure \ref{fig:expressionTyping} and \ref{fig:typing}.
-\TamedFJ{} is practically a subset of the Featherweight Java calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}
-with the exception that method argument and return type annotations are optional.
+Figure~\ref{fig:syntax} contains the syntax with optional type annotations highlighted in yellow.
+The respective typing rules are defined in Figures~\ref{fig:expressionTyping} and~\ref{fig:typing}.
+\TamedFJ{} is a subset of the calculus defined by Bierhoff
+\cite{WildcardsNeedWitnessProtection}, but in addition we make the types for
+method arguments and return types optional. 
 The point is that a correct and fully typed \TamedFJ{} program is also a correct Featherweight Java program,
-which is vital for our soundness proof (see chapter \ref{sec:soundness}).
+which is vital for our soundness proof (chapter \ref{sec:soundness}).
 %The language is designed to showcase type inference involving existential types.

-A method assumption consists out of a method name, a list of type parameters, a list of argument types, and a return type.
+A method assumption consists of a method name, a list of type variables, a list of argument types, and a return type.
 The first type in the list of argument types is the type of the surrounding class also known as the \texttt{this} parameter.
-See figure \ref{fig:methodTypeExample} for an example:
-Here the \texttt{add} method internally is treated as a method with two arguments,
-because we add \texttt{this} to its argument list.
-Note that the type parameter $\type{A}$ of the surrounding class is part of the methods parameter list.
+See Figure~\ref{fig:methodTypeExample} for an example, where the
+\texttt{add} method is treated internally as a method with two
+arguments, because we add \texttt{this} to its argument list.
+The type variable $\type{A}$ of the surrounding class is part of the
+method's list of type parameters.
 %For example the \texttt{add} method in listing \ref{lst:tamedfjSample} is represented by the assumption
 %$\texttt{add} : \generics{\ol{X \triangleleft Object}}\ \type{X} \to \exptype{List}{\type{X}}$.
 \begin{figure}
@@ -38,7 +40,7 @@ class List<A extends Object> {
 \begin{minipage}{0.49\textwidth}
 \begin{align*}
 &\mathrm{\Pi} = \set{\\
-&\texttt{add} : \generics{\ol{A \triangleleft Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{X}} \\
+&\texttt{add} : \generics{\type{A} \triangleleft \type{Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{A}} \\
 &}
 \end{align*}
 \end{minipage}
@@ -55,23 +57,28 @@ class List<A extends Object> {
 \textit{Additional Notes:}%
 \begin{itemize}
 %\item Method parameters and return types are optional.
-\item We still require type annotations for fields and generic class parameters.
-This is a design choice by us,
-as we consider them as data declarations which are given by the programmer.
+\item We require type annotations for fields and generic class parameters,
+  as we consider them as data declarations which are given by the programmer.
 % They are inferred in for example \cite{plue14_3b}
-\item We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
-\item \textit{Note:} The \texttt{new} expression is not requiring generic parameters.
+\item We add the elvis operator ($\elvis{}$) to the syntax to easily showcase applications involving wildcard types.
+This operator is used to emulate Java's \texttt{if-else} expression but without the condition clause.
+Our operator just returns one of the two given statements at random.
+The point is that the return type of the elvis operator has to be a supertype of its two subexpressions.
+\item The \texttt{new} expression does not require generic parameters.
 \item Every method has an unique name.
-The calculus does not include method overriding for simplicity reasons.
-Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-\item The \textsc{T-Program} type rule ensures that there is one set of method assumptions used for all classes
+The calculus does not include method overriding for simplicity.
+Type inference with method overriding is described elsewhere
+\cite{TIforFGJ} and can be added to our algorithm in a similar way.
+\item The \textsc{T-Program} typing rule ensures that there is one set of method assumptions used for all classes
 that are part of the program.
-\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
-Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus
-needs to be restricted in that regard.
-Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
-and as close to it's Featherweight Java correspondent as possible,
-simplifying the soundness proof.
+\item Unlike previous work \cite{TIforFGJ},  the typing rules for expressions shown in
+  Figure~\ref{fig:expressionTyping} allow for polymorphic recursion.
+  Type inference for polymorphic recursion is undecidable
+  \cite{wells1999typability} and when proving completeness the calculus needs to be restricted in that regard (cf.\
+  \cite{TIforFGJ}).
+  Our algorithm is not complete (see discussion in section
+  \ref{sec:completeness}), so we keep the \TamedFJ{} calculus as simple as possible
+  and close to Featherweight Java to simplify the soundness proof. 
 \end{itemize}

 %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
@@ -123,18 +130,20 @@ $\begin{array}{l}
    \begin{array}{@{}c}
        \Delta \vdash \type{T} <: \type{T}
    \end{array}
-\end{array}$
+ \end{array}$
+ \qquad
 $\begin{array}{l}
    \typerule{S-Trans}\\
    \begin{array}{@{}c}
-        \Delta \vdash \type{S} <: \type{T}' \quad \quad
-        \Delta \vdash \type{T}' <: \type{T}
+        \Delta \vdash \type{S} <: \type{T} \quad \quad
+        \Delta \vdash \type{T} <: \type{U}
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \Delta \vdash \type{S} <: \type{T}
+        \Delta \vdash \type{S} <: \type{U}
    \end{array}
-\end{array}$
+ \end{array}$
+ \qquad
 $\begin{array}{l}
    \typerule{S-Upper}\\
    \begin{array}{@{}c}
@@ -144,7 +153,8 @@ $\begin{array}{l}
    \vspace*{-0.9em}\\
        \Delta \vdash \type{X} <: \type{U}
    \end{array}
-\end{array}$
+ \end{array}$
+ \qquad
 $\begin{array}{l}
    \typerule{S-Lower}\\
    \begin{array}{@{}c}
@@ -166,7 +176,8 @@ $\begin{array}{l}
    \vspace*{-0.3cm}\\
        \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
    \end{array}
-\end{array}$
+ \end{array}$
+ \quad
 $\begin{array}{l}
    \typerule{S-Exists}\\
    \begin{array}{@{}c}
@@ -193,6 +204,7 @@ $\begin{array}{l}
        \Delta \vdash \bot \ \ok
    \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
    \typerule{WF-Top}\\
    \begin{array}{@{}c}
@@ -203,6 +215,7 @@ $\begin{array}{l}
        \Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object}
    \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
    \typerule{WF-Var}\\
    \begin{array}{@{}c}
@@ -363,14 +376,14 @@ $\begin{array}{l}
 $\begin{array}{l}
    \typerule{T-Elvis}\\
    \begin{array}{@{}c}
-        \triangle | \Gamma \vdash \texttt{t} : \type{T}_1 \quad \quad
-        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T}_2 \quad \quad
-        \triangle \vdash \type{T}_1 <: \type{T} \quad \quad
-        \triangle \vdash \type{T}_2 <: \type{T} \quad \quad
+        \triangle | \Gamma \vdash \texttt{t}_1 : \type{S} \quad \quad
+        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T} \quad \quad
+        \triangle \vdash \type{S} <: \type{U} \quad \quad
+        \triangle \vdash \type{T} <: \type{U} \quad \quad
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
+        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{U}
    \end{array}
 \end{array}$
 \end{center}
@@ -443,4 +456,8 @@ $\begin{array}{l}
    \end{array}
 \end{array}$
 \caption{Field access}
-\end{figure}
+\end{figure}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:
--- a/typeinference.tex
+++ b/typeinference.tex
@@ -0,0 +1,416 @@
+
+\section{Global Type Inference Algorithm}
+\label{sec:glob-type-infer}
+
+This section gives an overview of the global type inference algorithm
+with examples and identifies the challenges that we had to overcome in
+the design of the algorithm.
+
+\begin{figure}[h]
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
+<A> List<A> add(List<A> l, A v)
+
+List<? super String> l = ...;
+add(l, "String");
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
+<A> List<A> add(List<A> l, A v)
+List<? super String> l = ...;
+let v:(*@$\tv{v}$@*) = l
+    in add(v, "String");
+\end{lstlisting}
+\end{minipage}\\
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
+(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
+(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
+(*@$\type{String} \lessdot \wtv{a}$@*)
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=Type solution, label=lst:addExampleSolution]
+<A> List<A> add(List<A> l, A v)
+List<? super String> l = ...;
+let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
+    in <X>add(l2, "String");
+\end{lstlisting}
+\end{minipage}
+\end{figure}
+
+% \begin{description}
+%     \item[input] \tifj{} program
+%     \item[output] type solution
+%     \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
+% \end{description}
+
+%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Listings~\ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
+\ref{lst:addExampleSolution} showcase the global type inference algorithm step by step.
+Note that regular Java code snippets are displayed in a grey box, \TamedFJ{} programs are yellow
+and constraints have a red background.
+%This example is fully typed except for the method call \texttt{add} missing its type parameters.
+In the Java code in Listing~\ref{lst:addExample}, the type of variable
+\texttt{l} is an existential type so that it has to undergo a capture conversion
+before being passed to a method call.
+To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
+which introduces a let statement defining a new variable \texttt{v}.
+The constraint generation step also assigns type placeholders to all variables missing a type annotation.
+%In this case the variable \texttt{v} gets the type placeholder $\tv{v}$ (also shown in listing \ref{lst:addExampleCons})
+%during the constraint generation step.
+In this case the algorithm puts the type
+placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
+These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
+% During the constraint generation step the type of the variable \texttt{v} is unknown
+% and given the type placeholder $\tv{v}$.
+The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
+This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
+expresses that the left side of the constraint is subject to a capture conversion.
+Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
+Havin the constraints in listing \ref{lst:addExampleCons} as an input \unify{} changes the constraint
+$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$
+to $\tv{v} \doteq \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+therby finding a type solution for $\tv{v}$.
+Afterwards every occurence of $\tv{v}$ in the constraint set is replaced by $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+leaving us with the following constraints which are now subject to a capture conversion by the \unify{} algorithm:
+% Initially, no type is assigned to $\tv{v}$.
+% % During the course of \unify{} more and more types emerge.
+% As soon as a concrete type for $\tv{v}$ is appears during constraint
+% solving,  \unify{} can conduct a capture conversion if needed.
+% %The constraints where this is possible are marked as capture constraints.
+% In this example, $\tv{v}$ will be set to
+% $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+% leaving us with the following constraints: 
+
+\begin{displaymath}
+\prftree[r]{Capture}{
+\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
+}{
+\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+}
+\end{displaymath}
+
+%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
+%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
+The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
+allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+The captured wildcard $\rwildcard{X}$ gets a fresh name \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
+Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
+solved: $\exptype{List}{\rwildcard{Y}} \lessdot
+\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
+\rwildcard{Y}$. 
+The first constraint is obviously satisfied and $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
+
+
+A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in Listing \ref{lst:addExampleSolution}.
+This program can be deduced from the solution of the \unify{} algorithm.% presented in Section~\ref{sec:unify}.
+In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
+becomes $\exptype{List}{\rwildcard{X}}$ and the capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
+a type parameter of the call \texttt{<X>add(v, "String")}.
+
+% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
+% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
+% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
+% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
+% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
+% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
+% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
+% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
+% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
+
+% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
+% We try to keep the branching at a minimal amount to improve runtime behavior.
+% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
+% There are no informal parts in our \unify{} algorithm.
+% It solely consist out of transformation rules which are bound to simple checks.
+
+\subsection{Notes on Capture Constraints}
+Capture constraints must be stored in a multiset so that it is possible that two syntactically equal constraints remain in the same set.
+The equality relation on Capture constraints is not reflexive.
+
+Capture Constraints are bound to a variable.
+For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
+$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
+This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
+Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
+creating the constraints \ref{lst:sameConstraints}.
+
+\begin{figure}
+  \begin{minipage}[t]{0.49\textwidth}
+    \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat,style=TamedFJ]{tamedfj}
+  List<?> v = ...;
+  
+  let x = v in 
+      let y = v in
+        concat(x, y) // Error!
+    \end{lstlisting}\end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.49\textwidth}
+  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
+  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
+  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
+    \end{lstlisting}
+    \end{minipage}
+\end{figure}
+
+
+During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
+but they are not the same because they are each linked to a different let introduced variable.
+In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
+resulting in:
+%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
+\begin{displaymath}
+  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
+\end{displaymath}
+Thanks to the original annotations we can still see that those are different constraints.
+After \unify{} uses the \rulename{Capture} rule on those constraints
+it gets obvious that this constraint set is unsolvable:
+\begin{displaymath}
+  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
+\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
+\end{displaymath}
+
+%In this paper we do not annotate capture constraint with their source let statement.
+This paper will not annotate capture constraints with variable names.
+Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
+because we know that each of them originates from a different let statement.
+\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
+and has to allow doubles in the constraint set.
+
+% %We see the equality relation on Capture constraints is not reflexive.
+% A capture constraint is never equal to another capture constraint even when structurally the same
+% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
+% This is necessary to solve challenge \ref{challenge:1}.
+% A capture constraint is bound to a specific let statement.
+
+\textit{Note:}
+In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
+and we could actually delete one of them without loosing information.
+But this case will never occur in our algorithm, because the let
+statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
+
+
+\subsection{Challenges}\label{challenges}
+%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
+
+% Wildcards are not reflexive.
+% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
+
+% do not substitute free type variables
+
+Global type inference for Featherweight Generic Java without wildcards
+has been considered elsewher \cite{TIforFGJ}.
+Adding wildcards to the calculus created new problems, which have not
+been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
+% what is the problem?
+% Java does invisible capture conversion steps 
+Java's wildcard types are represented as existential types that have to be opened before they can be used.
+Opening can either be done implicitly
+(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
+explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
+For all variations it is vital to know the argument types with which a method is called.
+In the absence of type annotations,
+we do not know where an existential type will emerge and where a capture conversion is necessary.
+Rather, the type inference algorithm has to figure out the placement
+of existentials.
+We identified three main challenges related to Java wildcards and global type inference.
+\begin{enumerate}
+\item \label{challenge:1}
+One challenge is to design the algorithm in a way that it finds a
+correct solution for programs like the one shown in Listing~\ref{lst:addExample}
+and rejects programs like the one in Listing~\ref{lst:concatError}.
+The first one is a valid Java program,
+because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
+which is used as the generic method parameter for the call to \texttt{add} as shown in Listing~\ref{lst:addExampleLet}.
+Because we know that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$,
+it is safe to pass \texttt{"String"} for the first parameter of the function.
+
+The second program shown in Listing~\ref{lst:concatError} is incorrect.
+The method call to \texttt{concat} with two wildcard lists is unsound.
+The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
+The problem gets apparent if we try to write the \texttt{concat}
+method call in the \TamedFJ{} calculus
+(Listing~\ref{lst:concatTamedFJ}): 
+\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
+$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
+For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
+exists to satisfy
+$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
+\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
+
+% \textbf{Solution:}
+% Capture Conversion during Unify.
+
+% \item 
+% \unify{} transforms a constraint set into a correct type solution by
+% gradually assigning types to type placeholders during that process.
+% Solved constraints are removed and never considered again.
+% In the following example, \unify{} solves the constraint generated by the expression
+% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
+% \begin{verbatim}
+% anyList() = new List<String>() :? new List<Integer>()
+
+% add(anyList(), anyList().head());
+% \end{verbatim}
+% The type for \texttt{l} can be an arbitrary list, but it has to be a invariant one.
+% Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
+% \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
+% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+% is solved by removing the wildcard $\rwildcard{X}$ if possible.
+
+% This problem is solved by ANF transformation
+
+\item
+% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
+% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
+The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
+The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
+However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
+$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
+and can be passed safely to \texttt{shuffle}.
+This behavior can also be explained by looking at the types and their capture converted versions:
+\begin{center}
+\begin{tabular}{l | l | l}
+Java type & \TamedFJ{} representation & Capture Conversion \\
+\hline
+$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
+$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
+%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
+\end{tabular}
+\end{center}
+%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+%One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+%A wildcard in the Java syntax has no name and is bound to its enclosing type:
+%$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+%During type checking \emph{intermediate types}
+%can emerge, which have no equivalent in the Java syntax.
+
+\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
+class List<X> extends Object {...}
+class List2D<X> extends List<List<X>> {...}
+
+<X> void shuffle(List<List<X>> list) {...}
+
+List<List<?>> l = ...;
+List2D<?> l2d = ...;
+
+shuffle(l); // Error
+shuffle(l2d); // Valid
+\end{lstlisting}
+% Java is using local type inference to allow method invocations which are not describable with regular Java types.
+% The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
+% which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+% After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
+% and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
+% \begin{lstlisting}[style=TamedFJ]
+% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
+% \end{lstlisting}
+
+% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
+% \begin{constraintset}
+% \begin{center}
+%     $
+%     \begin{array}{l}
+%     \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+%     \\
+%     \hline
+%     \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+%     \\
+%     \hline
+%     \textit{Capture Conversion:}\ 
+%     \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
+%     \\
+%     \hline
+%     \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
+%     \end{array}
+%     $
+% \end{center}
+% \end{constraintset}
+
+Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
+decline the call to \texttt{shuffle(l)}.
+
+% The method call \texttt{shuffle(l)} is invalid however,
+% because \texttt{l} has the type
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+% There is no solution for the subtype constraint:
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
+
+\item \label{challenge3}
+% \textbf{Free variables cannot leave their scope}:
+% Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
+% %When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
+% and the following program:
+
+% \noindent
+% \begin{minipage}{0.62\textwidth}
+% \begin{lstlisting}
+% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
+% \end{lstlisting}\end{minipage}
+%   \hfill
+% \begin{minipage}{0.36\textwidth}
+%   \begin{lstlisting}[style=constraints]
+% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
+% (*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
+%   \end{lstlisting}
+% \end{minipage}
+% % the variable z must not contain free variables (TODO)
+
+Take the Java program in listing \ref{lst:mapExample} for example.
+It uses map to apply a polymorphic method \texttt{id} to every element of a list
+$\expr{l} :
+\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$. 
+
+How do we get the \unify{} algorithm to determine the correct type for the
+variable \expr{l2}?
+Although we do not specify constraint generation for language constructs like
+lambda expressions used in this example,
+we can imagine that the constraints have to look like in Listing~\ref{lst:mapExampleCons}.
+
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
+<X> List<X> id(List<X> l){ ... }
+List<List<?>> ls;
+l2 = l.map(x -> id(x));
+\end{lstlisting}\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
+(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
+(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
+(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
+\end{lstlisting}
+\end{minipage}
+
+The constraints
+$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
+\exptype{List}{\wtv{x}} \lessdot \tv{z}$
+stem from the body of the lambda expression
+\texttt{id(x)}.
+\textit{For clarification:} This method call would be represented as the following expression in \TamedFJ{}:
+
+\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
+
+The T-Let rule prevents us from using free variables created by the method call to \expr{id}
+to be used in the return type $\tv{z}$.
+But this restriction has to be communicated to the \unify{} algorithm,
+which does not know about the origin and context of 
+the constraints.
+If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
+the return type of the \texttt{map} function would be the type
+$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
+
+% The type of \expr{l2} is the same as the one of \expr{l}:
+% $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
+
+% \textbf{Solution:}
+% We solve this issue by distinguishing between wildcard placeholders
+% and normal placeholders and introducing them as needed.
+% $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
+\end{enumerate}
--- a/unify.tex
+++ b/unify.tex
@@ -225,27 +225,6 @@ We define two types as equal if they are mutual subtypes of each other.
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
-   \rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
-   %It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
-   & 
-   $
-   \begin{array}[c]{@{}ll}
-   \begin{array}[c]{l}
-       \wildcardEnv \vdash 
-       C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\ 
-     \hline
-     \vspace*{-0.4cm}\\
-       \wildcardEnv \vdash 
-       C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\ 
-   \end{array}
-    %\quad \ol{Y} = \textit{fresh}(\ol{X})
-    \quad \begin{array}[c]{l}
-     \text{fv}(\type{N'}) \subseteq \Delta_{in} \\
-     \text{wtv}(\type{N'}) = \emptyset
-     \end{array}
-   \end{array}
-   $
-\\\\
 \rulename{Trim}
 & 
 $
@@ -421,6 +400,42 @@ After \rulename{Subst} and \rulename{Same} the remaining constraints are $\tv{b}
 $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rwildcard{A}}$
 %which is equal to $\tv{a} \lessdot \exptype{List}{\type{Integer}}$ and additionally we have $\tv{b} \doteq \type{Integer}$.

+\begin{figure}
+\begin{mathpar}
+\inferrule[Reduce]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\quad \text{wtv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+\and
+\inferrule[Reduce-Empty]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\and
+\inferrule[Exclude]{
+\wildcardEnv \vdash 
+C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} }
+}{
+\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} } \\  
+}\quad \Delta \neq \emptyset,
+\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
+\end{mathpar}
+\end{figure}
+
 \begin{figure}
    \begin{center}
        \leavevmode
@@ -458,7 +473,7 @@ $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rw
        \begin{array}[c]{@{}ll}
        \begin{array}[c]{l}
            \wildcardEnv \vdash 
-            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
          \hline
          \vspace*{-0.4cm}\\
@@ -498,24 +513,24 @@ $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rw
      \end{array}
      $
    \\\\
-        \rulename{Adopt}
-        & $
-        \begin{array}[c]{@{}ll}
-        \begin{array}[c]{l}
-          \wildcardEnv \vdash C \cup \, \set{
-           \tv{b} \lessdot_1 \tv{a},
-\tv{a} \lessdot_2 \type{N}, \tv{b} \lessdot_3 \type{N'}} \\ 
-          \hline
-          \vspace*{-0.4cm}\\
-          \wildcardEnv \vdash C \cup \, \set{
- \tv{b} \lessdot \type{N},
-           \tv{b} \lessdot_1 \tv{a},
-\tv{a} \lessdot_2 \type{N} , \tv{b} \lessdot_3 \type{N'}
-           }
-        \end{array}
-        \end{array}
-        $
-      \\\\
+%         \rulename{Adopt} // is already covered by Raise and Settle
+%         & $
+%         \begin{array}[c]{@{}ll}
+%         \begin{array}[c]{l}
+%           \wildcardEnv \vdash C \cup \, \set{
+%            \tv{b} \lessdot_1 \tv{a},
+% \tv{a} \lessdot_2 \type{N}, \tv{b} \lessdot_3 \type{N'}} \\ 
+%           \hline
+%           \vspace*{-0.4cm}\\
+%           \wildcardEnv \vdash C \cup \, \set{
+%  \tv{b} \lessdot \type{N},
+%            \tv{b} \lessdot_1 \tv{a},
+% \tv{a} \lessdot_2 \type{N} , \tv{b} \lessdot_3 \type{N'}
+%            }
+%         \end{array}
+%         \end{array}
+%         $
+%       \\\\
  \rulename{Adapt}
  & 
  $
@@ -575,6 +590,18 @@ gets the same wildcard twice.
                      \ntv{a} \notin \type{T} \\
                      \text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
                     \end{array}$\\
+\\
+      \rulename{Subst} &
+                       $\begin{array}[c]{l}
+  \wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
+                         \hline
+  [\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
+  C \cup \set{\ntv{a} \doteq \type{T}}
+                       \end{array}
+                     \quad \begin{array}{c}
+                      \ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
+                      \text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
+                     \end{array}$\\
 \\
 \rulename{Subst-WC} &$
                \begin{array}[c]{l}
@@ -680,16 +707,13 @@ exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and
 % }
 % \end{lstlisting}

-Take the introduction example from listing \ref{lst:intro-example}.
-Constraints for the untyped \texttt{genList} method:
-\begin{constraintset}
-$\begin{array}{l}
-\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}},
-\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}
-\end{array}$
-\end{constraintset}
-
+Let's have a look at the constraints generated by the introduction example in listing \ref{lst:intro-example-typeless}:
+\begin{lstlisting}[style=constraints]
+(*@$\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}}$@*),
+(*@$\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}$@*)
+\end{lstlisting}

+\unify{} executes the following steps to generate a solved constraint set:
 \begin{displaymath}
 \prftree[r]{\rulename{Subst}}
 {
@@ -735,28 +759,28 @@ After a substitution all $\tv{r}$ are replaced with this new existential type.

 In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$.
 Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$
-leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$.
+leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$:

-\begin{lstlisting}
+\begin{lstlisting}[style=tamedfj]
 List<? extends Object> someList(){
  return new List("String") :? new List(42);
 }
 \end{lstlisting}

-\subsection{Wildcard Elimination Example}
-\begin{lstlisting}
-  <X> List<X> concat(List<X> l, List<X> l2){ ... }
-  someList(){
-    return new List("String") :? new List(42);
-  }
+% \subsection{Wildcard Elimination Example}
+% \begin{lstlisting}
+%   <X> List<X> concat(List<X> l, List<X> l2){ ... }
+%   someList(){
+%     return new List("String") :? new List(42);
+%   }

-  concat(someList(), someList());
-\end{lstlisting}
+%   concat(someList(), someList());
+% \end{lstlisting}

-Let's add an additional method call to the previous example.
-The \texttt{concat} method takes two lists of the same generic type.
-\texttt{concat} cannot be invoked with two existential lists.
-%TODO: Explain capture conversion
+% Let's add an additional method call to the previous example.
+% The \texttt{concat} method takes two lists of the same generic type.
+% \texttt{concat} cannot be invoked with two existential lists.
+% %TODO: Explain capture conversion


 %\subsection{Description}
@@ -786,55 +810,22 @@ The \texttt{concat} method takes two lists of the same generic type.
 % 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}
+% \subsection{Algorithm}

-With \texttt{C} being class names and \texttt{A} being wildcard names.
-The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
-and a name $\mathtt{X}$.
+% With \texttt{C} being class names and \texttt{A} being wildcard names.
+% The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
+% and a name $\mathtt{X}$.

-The \rulename{Tame} rule eliminates wildcards. %TODO
-This is done by setting the upper and lower bound to the same value.
+% The \rulename{Tame} rule eliminates wildcards. %TODO
+% This is done by setting the upper and lower bound to the same value.

-The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
-Their upper and lower bounds are fresh type variables.
+% The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
+% Their upper and lower bounds are fresh type variables.

-\unify{} is able to remove wildcards by assigning their upper and lower bounds the same type
-(Def: $\type{Object} = \wildcard{A}{Object}{Object}$ by definition \ref{def:equal}).
-This is used by the \rulename{Tame} rule.
+% \unify{} is able to remove wildcards by assigning their upper and lower bounds the same type
+% (Def: $\type{Object} = \wildcard{A}{Object}{Object}$ by definition \ref{def:equal}).
+% This is used by the \rulename{Tame} rule.

-\textbf{Helper functions:}
-\begin{description}
-\item[$\tph{}$] returns all type placeholders inside a given type.
-
-\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
-
-%\textbf{Wildcard renaming}\\
-\item[Wildcard renaming:]
-The \rulename{Reduce} rule separates wildcards from their environment.
-At this point each wildcard gets a new and unique name.
-To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
-($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
-\begin{align*}
-  [\type{A}/\type{B}]\type{B} &= \type{A} \\
-  [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
-  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
-  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
-\end{align*}
-\item[Free Variables:]
-The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
-% TODO: describe a function which determines free variables? or do an example?
-\begin{align*}
-\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
-\text{fv}(\tv{a}) &= \emptyset \\
-%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
-\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
-\end{align*}
-
-\item[Fresh Wildcards:]
-$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
-The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
-which are used for the upper and lower bounds.
-\end{description}
 % \noindent
 % \textbf{Example: (reduce-rule)}
 % %The \ruleReduceWC{} resembles the \texttt{S-Exists} subtyping rule.
@@ -1219,7 +1210,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
  \label{fig:step2-rules2}
  \end{figure}

-Figure \ref{fig:step2-rules2} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
+Figure \ref{fig:step2-rules} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
 Usually \rulename{Upper} takes care of $\rwildcard{X} \lessdot \tv{a}$ constraints,
 but if $\rwildcard{X}$ is an element of $\Delta_{in}$ we can also treat it as a regular type.
 This leaves us with the two possibilities \rulename{Subst-X} and \rulename{Gen-X} which is the same as \rulename{Upper}.
@@ -1317,49 +1308,47 @@ $
 \label{fig:generation-rules}
 \end{figure}

-\subsection{Explanations}

-%The type reduction is done by the rules in figure \ref{fig:reductionRules}
+% \subsection{Examples}

-\subsection{Examples}
-\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input 
-$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
-The first step is the \rulename{Capture} rule.
-%The right side of the constraint does not contain any free variables.
-$\begin{array}{c}
-\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
-\hline %Capture
-\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
-\end{array}$
+% \textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input 
+% $\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
+% The first step is the \rulename{Capture} rule.
+% %The right side of the constraint does not contain any free variables.
+% $\begin{array}{c}
+% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
+% \hline %Capture
+% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
+% \end{array}$

-\begin{NiceTabular}{l}
-  $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
-  $\nextdeduction{
-    \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
-  } $\\
-  $\nextdeduction{
-    \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
-  } $\\
-  $\nextdeduction{
-    \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
-  } $\\
-  $\nextdeduction{
-      \wildcard{X}{Object}{\type{String}} \vdash
-      \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
-  } $\\
-  $\nextdeduction{
-      \wildcard{X}{Object}{\type{String}} \vdash
-      \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
-  } $\\
-      \CodeAfter
-      \begin{tikzpicture}
-          \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ; 
-          \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ; 
-          \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ; 
-          \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ; 
-          \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ; 
-      \end{tikzpicture}
-  \end{NiceTabular}
+% \begin{NiceTabular}{l}
+%   $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
+%   $\nextdeduction{
+%     \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
+%   } $\\
+%   $\nextdeduction{
+%     \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
+%   } $\\
+%   $\nextdeduction{
+%     \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
+%   } $\\
+%   $\nextdeduction{
+%       \wildcard{X}{Object}{\type{String}} \vdash
+%       \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
+%   } $\\
+%   $\nextdeduction{
+%       \wildcard{X}{Object}{\type{String}} \vdash
+%       \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
+%   } $\\
+%       \CodeAfter
+%       \begin{tikzpicture}
+%           \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ; 
+%           \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ; 
+%           \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ; 
+%           \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ; 
+%           \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ; 
+%       \end{tikzpicture}
+%   \end{NiceTabular}

 % \subsection{Capture Conversion during Unification}
 % % The \unify{} algorithm applies a capture conversion when needed.
@@ -1412,48 +1401,48 @@ $\begin{array}{c}
 % \end{itemize}


-\subsection{Completeness}\label{sec:completeness}
-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}.
-%thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
-Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.
+% \subsection{Completeness}\label{sec:completeness}
+% 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}.
+% %thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
+% Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.

-\letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java
+% \letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java

-%Loss of completeness:
-% a <. b, b <c List<x>
+% %Loss of completeness:
+% % a <. b, b <c List<x>

-% Example
-\begin{lstlisting}
-m(l){
-  return let x = l in x.add(1);
-}
-\end{lstlisting}
-Here generality is lost.
-Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$
+% % Example
+% \begin{lstlisting}
+% m(l){
+%   return let x = l in x.add(1);
+% }
+% \end{lstlisting}
+% Here generality is lost.
+% Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$

-Correct solution would be:
-\begin{lstlisting}
-m(List<? super Int> l){
-  return let x = l in x.add(1);
-}
-\end{lstlisting}
+% Correct solution would be:
+% \begin{lstlisting}
+% m(List<? super Int> l){
+%   return let x = l in x.add(1);
+% }
+% \end{lstlisting}

-Our solution:
-\begin{lstlisting}
-<X extends List<Integer> m(X l){
-  return let x = l in x.add(1);
-}
-m(List<? super Integer>)
-\end{lstlisting}
-$\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
-because there will be a capture conversion.
-We do not cover this and only apply capture conversion when the left side is known.
-So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.
+% Our solution:
+% \begin{lstlisting}
+% <X extends List<Integer> m(X l){
+%   return let x = l in x.add(1);
+% }
+% m(List<? super Integer>)
+% \end{lstlisting}
+% $\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
+% because there will be a capture conversion.
+% We do not cover this and only apply capture conversion when the left side is known.
+% So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.

-If all of the program is given this may be not much of an issue.
-The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
-is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.
+% If all of the program is given this may be not much of an issue.
+% The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
+% is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.

 % Problem: There are infinite subtypes to a type Pair<x,y> when capture conversion is allowed 

@@ -1462,12 +1451,12 @@ is called and $\tv{a}$ gets a type, then this type can be an existential type as
 % ( is this complete? X,Y.Pair<X,Y> <c X.Pair<X,X>)


-\subsection{Implementation}
-%List this under implementation details
-Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable
+% \subsection{Implementation}
+% %List this under implementation details
+% Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable

-The new constraint generated by the adopt rule may be eliminated by the match rule.
-The adopt rule still needs to be applied only once per constraint.
+% The new constraint generated by the adopt rule may be eliminated by the match rule.
+% The adopt rule still needs to be applied only once per constraint.


 % \textbf{Eliminating Wildcards}
Author	SHA1	Message	Date
JanUlrich	0c260eef12	Start with cctv and soundness proof	2024-07-23 10:47:20 +02:00
Andreas Stadelmeier	2b57b092be	Fixes for Soundness Proof. Start with Capture Conversion at Subst-Step and introduce ccTVs	2024-07-17 16:15:24 +02:00
Andreas Stadelmeier	fb22548d38	Remove Adopt	2024-06-04 01:55:48 +02:00
Andreas Stadelmeier	f699cc075f	Final Version and Submission to ESOP Round 1	2024-05-31 13:52:18 +02:00
Andreas Stadelmeier	0e157cf427	Fix Related Work. Adapt Soundness proof	2024-05-31 11:49:44 +02:00
Andreas Stadelmeier	c86dc891f3	Cleanup, Fixes and Restructuring	2024-05-31 00:10:22 +02:00
Peter Thiemann	7e1ef7b3c1	intro	2024-05-29 14:31:13 +02:00
Peter Thiemann	8b0e77cf50	cosmetics	2024-05-29 12:07:10 +02:00
Peter Thiemann	e42b0aaafe	Merge branch 'master' of https://gitea.hb.dhbw-stuttgart.de/stan/Ecoop2024_TIforWildFJ	2024-05-29 11:01:32 +02:00
Peter Thiemann	8428ebdc70	changes	2024-05-29 11:01:30 +02:00