Start with cctv and soundness proof

.gitignore

@@ -17,3 +17,7 @@
 *-blx.aux
 *-blx.bib
 *.run.xml
+*.vtc
+*.synctex.gz
+auto
+_region_.tex

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass{llncs}
+\documentclass[anonymous,USenglish]{llncs}
 %This is a template for producing LIPIcs articles. 
 %See lipics-v2021-authors-guidelines.pdf for further information.
 %for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -38,6 +38,8 @@
 \usepackage{arydshln}
 \usepackage{dashbox}
 
+\usepackage{mathpartir}
+
 \input{prolog}
 
 \begin{document}
@@ -45,22 +47,19 @@
 
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
 
-%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% ANON
 
-\author{Andreas Stadelmeier}{DHBW Stuttgart, Campus Horb, Germany}{a.stadelmeier@hb.dhbw-stuttgart.de}{}{}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.
+% \author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}}
+% \institute{DHBW Stuttgart, Campus Horb, Germany\\
+% \email{a.stadelmeier@hb.dhbw-stuttgart.de} \and
+% Universität Freiburg, Institut für Informatik, Germany\\
+% \email{thiemann@informatik.uni-freiburg.de}}
 
-\author{Martin Plümicke}{DHBW Stuttgart, Campus Horb, Germany}{pl@dhbw.de}{}{}
+% \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann}
 
-\author{Peter Thiemann}{Universität Freiburg, Institut für Informatik, Germany}{thiemann@informatik.uni-freiburg.de}{}{}
-
-\authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
-
-%\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
-
-%\ccsdesc[500]{Software and its engineering~Language features}
-%\ccsdesc[300]{Software and its engineering~Syntax}
-
-\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
+%% END ANON
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %\category{} %optional, e.g. invited paper
 
@@ -97,8 +96,17 @@
 
 %TODO mandatory: add short abstract of the document
 \begin{abstract}
-TODO: Abstract
+  Type inference is a hallmark of functional programming. Its use in
+  object-oriented programming is often restricted to type inference
+  for local variables and the instantiation of generic type
+  parameters.
+
+  Global type inference for Featherweight Generic Java is a
+  whole-program analysis that infers omitted method signatures.
+  Compared to previous work, its results are more general as it infers
+  types with wildcards. Global type inference is proved sound.
 \end{abstract}
+\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
 
 \input{introduction}
 
@@ -106,51 +114,26 @@ TODO: Abstract
 
 \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}

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}

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()
+ 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){}
 
@@ -508,3 +431,7 @@ cannot be used anywhere else then inside the constraints generated by the method
 % \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}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:

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}

introduction.tex

@@ -26,30 +26,62 @@
 % It's only restriction is that no polymorphic recursion is allowed.
 % \end{recap}
 
+\section{Introduction}
+\label{sec:introduction}
 
-\section{Type Inference for Java}
-- Type inference helps rapid development
-- used in Java already (var keyword)
-- keeps source code clean
+Type inference is a hallmark of functional programming, where it
+improves readability and conciseness while 
+enabling safe rapid prototyping by allowing the compiler to deduce
+types automatically without explicit type annotations. It allows
+developers to safely refactor their programs before fixing function
+signatures.  In object-oriented programming (OOP), however, the use of
+type inference is more restricted. It is often employed for local
+variables and the instantiation of generic type parameters, offering
+similar readability and conciseness benefits as in functional
+programming. In languages like Java, the overall architecture of
+method signatures must be designed by the programmer up-front.
 
-Java comes with a local type inference algorithm
-used for lambda expressions, method calls, and the \texttt{var} keyword.
+Java features a limited form of local type inference for local
+variables defined with  the \texttt{var} keyword, lambda expressions,
+and method calls. Java infers the type of variables defined with
+\texttt{var}. The rationale here is that instantiations of generic 
+types (e.g., maps of maps) are often unwiedly and they can be easily
+inferred from the initializing expression. The type of a lambda
+expression is inferred from the target type, i.e., the type of the
+method argument that accepts the lambda. The rationale is the intended
+use of lambdas as callback functions for listeners etc. For calls
+to generic methods, Java infers the most specific instantiation of the
+generic parameters for each individual call. 
 
-A type inference algorithm that is able to recreate any type annotation
-even when no type information is given at all is called a global type inference algorithm.
-The global type inference algorithm presented here is able to deal with all Java types including wildcard types.
-It can also be used for regular Java programs.
+The local type inference features of Java add some convenience, but
+programmers still have to provide method signatures beforehand. So there
+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, 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.
-Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
-finding better type solutions for already typed Java programs (for example more generical ones),
-or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm.
+Our algorithm enables programmers to write Java code with only a
+minimum of type annotations (class headers and types of field
+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.
 
-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}.
@@ -57,125 +89,8 @@ are infered and inserted by our algorithm.
 %This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
 
-\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
-%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]
-<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]
-emptyList().add(new List<String>())
-    .get(0)
-    .get(0); //Typing Error
-\end{lstlisting}
-%List<String> <. A
-%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.
-
-\end{description}
-% %motivate constraints: 
-% To solve this example our Type Inference algorithm will create constraints
-% $
-% \exptype{List}{\tv{a}} \lessdot \tv{b},
-% \tv{b} \lessdot \exptype{List}{\tv{c}},
-% \tv{c} \lessdot \exptype{List}{\tv{d}}
-% $
-
-
-
-%\subsection{Conclusion}
-% Additions: TODO
-% - Global Type Inference Algorithm, no type annotations are needed
-% - Soundness Proof 
-% - Easy to implement
-% - Capture Conversion support
-% - Existential Types support
-Our contributions are
-\begin{itemize}
-\item
-We introduce the language \tifj{} (chapter \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}.
-\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.
-\item
-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}
-% class SuperPair<A,B>{
-%     A a;
-%     B b;
-% }
-% class Pair<A,B> extends SuperPair<B,A>{
-%     A a;
-%     B b;
-
-%     <X> X choose(X a, X b){ return b; }
-
-%     String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
-%         return choose(choose(a,b).value.a,b.value.b);
-%     }
-% }
-% \end{verbatim}
-
-
-\begin{figure}
+\begin{figure}[tp]
 \begin{minipage}{0.43\textwidth}
 \begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
 genList() {
@@ -201,6 +116,118 @@ List<?> genList() {
 \end{minipage}
 \end{figure}
   
+
+
+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. 
+
+
+%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.
+
+
+\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}
+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
+\end{lstlisting}
+%List<String> <. A
+%List<A> <: List<B>, B <: List<C> 
+% B = A and therefore A on the left and right side of constraints.
+% this makes matching impossible
+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.
+
+
+% %motivate constraints: 
+% To solve this example our Type Inference algorithm will create constraints
+% $
+% \exptype{List}{\tv{a}} \lessdot \tv{b},
+% \tv{b} \lessdot \exptype{List}{\tv{c}},
+% \tv{c} \lessdot \exptype{List}{\tv{d}}
+% $
+
+
+
+%\subsection{Conclusion}
+% Additions: TODO
+% - Global Type Inference Algorithm, no type annotations are needed
+% - Soundness Proof 
+% - Easy to implement
+% - Capture Conversion support
+% - Existential Types support
+We summarize our contributions:
+\begin{itemize}
+\item
+We introduce the language \tifj{} (section \ref{sec:tifj}), 
+a Featherweight Java derivative including generics, wildcards, and type inference.
+\item
+  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.
+\item
+  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}
+% class SuperPair<A,B>{
+%     A a;
+%     B b;
+% }
+% class Pair<A,B> extends SuperPair<B,A>{
+%     A a;
+%     B b;
+
+%     <X> X choose(X a, X b){ return b; }
+
+%     String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
+%         return choose(choose(a,b).value.a,b.value.b);
+%     }
+% }
+% \end{verbatim}
+
+
 % \subsection{Wildcards}
 % Java subtyping involving generics is invariant.
 % For example \texttt{List<String>} is not a subtype of \texttt{List<Object>}.
@@ -210,25 +237,25 @@ List<?> genList() {
 % 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 = ...;
@@ -248,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>}.
@@ -263,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
@@ -355,269 +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
-
-Lets have a look at a few challenges:
-\begin{itemize}
-\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 \textbf{Wildcards as Existential Types:}
-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}
-
-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}:
-
-\begin{example}
-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{example}
-
-\end{itemize}
-
-%TODO: Move this part. or move the third challenge some underneath.

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}}

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 ???????
 

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}

tRules.tex

@@ -5,38 +5,80 @@
 %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
-
-The input to our algorithm is a typeless version of Featherweight Java.
-The syntax is shown in figure \ref{fig:syntax}
-and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
-Method parameters and return types are optional.
-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.
-% They are inferred in for example \cite{plue14_3b}
-Note the \texttt{new} expression not requiring generic parameters,
-which are also inferred by our algorithm.
-The method call naturally has type inferred generic parameters aswell.
-We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
-The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
-It is possible to exclude all optional types.
-\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
+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.
+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 (chapter \ref{sec:soundness}).
 %The language is designed to showcase type inference involving existential types.
-The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
-which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
 
-\noindent
-\textit{Notes:}
+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, 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}
+\center
+\begin{minipage}{0.49\textwidth}
+    %[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
+\begin{lstlisting}
+class List<A extends Object> {
+    List<A> add(A v){..,}
+}
+\end{lstlisting}
+\end{minipage}
+\begin{minipage}{0.49\textwidth}
+\begin{align*}
+&\mathrm{\Pi} = \set{\\
+&\texttt{add} : \generics{\type{A} \triangleleft \type{Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{A}} \\
+&}
+\end{align*}
+\end{minipage}
+% \begin{minipage}{0.49\textwidth}
+% \begin{lstlisting}[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
+% class List<A extends Object> {}
+% <A extends Object> List<A>
+%     add(List<A> this, A v){..,}
+% \end{lstlisting}
+% \end{minipage}
+\caption{\TamedFJ{} class and its corresponding method type environment}\label{fig:methodTypeExample}
+\end{figure}
+
+\textit{Additional Notes:}%
 \begin{itemize}
-\item 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.
-%\textit{Note:}
-\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 \cite{WildcardsNeedWitnessProtection} as possible.
-Our soundness proof works either way.
+%\item Method parameters and return types are optional.
+\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 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.
+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 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.
@@ -73,6 +115,7 @@ $
 & & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
 & & \ \ | & \expr{e} \elvis{} \expr{e}\\
 \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
 %\hline
 \end{array}
 $
@@ -87,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}
@@ -108,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}
@@ -130,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}
@@ -157,6 +204,7 @@ $\begin{array}{l}
         \Delta \vdash \bot \ \ok
     \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
     \typerule{WF-Top}\\
     \begin{array}{@{}c}
@@ -167,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}
@@ -327,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}
@@ -408,3 +457,7 @@ $\begin{array}{l}
 \end{array}$
 \caption{Field access}
 \end{figure}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:

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}

unify.tex

@@ -6,6 +6,102 @@
 % the algorithm only removes wildcards, never adds them
 
 \section{Unify}\label{sec:unify}
+
+%\newcommand{\tw}[1]{\tv{#1}_?}
+\begin{description}
+  \item[Input:] An environment $\Delta'$
+and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}, \type{T} \doteq \type{T} \ldots}$
+
+\item[Output:]
+Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$
+\end{description}
+
+%The transformation steps are not applied all at once but in a specific order:
+\unify{} executes the following steps until a type solution is found:
+\begin{description}
+\item[Step 1:]
+Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
+starting with the \rulename{circle} rule.
+
+\item[Step 2:]
+%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
+%resume with step 4.
+
+The second step is nondeterministic.
+%\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
+%The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
+For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
+The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
+%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
+If atleast one transformation was applied in this step revert to step 1.
+Otherwise proceed with step 3.
+%This builds a search tree over multiple possible solutions.
+%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
+
+%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
+
+\textit{Hint:}
+When implementing this step via backtracking
+the rules \rulename{General} and \rulename{Super} should be tried first.
+% is the Same rule really necessary?
+The \rulename{Settle} and \rulename{Raise} rules should only be used when none of the rules in figure \ref{fig:step2-rules} can be applied.
+
+
+\item[Step 3:]
+Apply the rules in figure \ref{fig:cleanup-rules} exhaustively.
+\rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables.
+If a type placeholder is solely used as lower bound \rulename{Ground} can replace it with the bottom type.
+Otherwise the \rulename{Flatten} rule has to remove the wildcards responsible for the free variable.
+\text{Note:} Only one of those rules has to be applied per constraint.
+If the constraint set has been changed by one of these rules the algorithm must return to step 1.
+But if only the \rulename{SubElim} rule is applied or the constraint set is not changed at all,
+the algorithm can proceed with step 4.
+
+The cleanup step prepares the constraint set for the last step by applying the following concepts:
+%Two transformations are done which also help to remove unnecessary types from the solution set.
+\begin{description}
+\item[Bottom type]
+The bottom type $\bot$ is used to generate \texttt{? extends} wildcard definitions.
+This is the only possible solution when dealing with multiple upper bounds:
+$\tv{a} \lessdot \type{T}, \tv{a} \lessdot \type{S}$ is usually not a correct solution (given $\type{S}$ and $\type{T}$ are no subtypes of eachother).
+But if $\tv{a}$ is a lower bound of a wildcard it can be set to $\bot$.
+Those constraints only stay in the constraint set after the first step if $\type{S}$ and $\type{T}$ do not have a common subtype.
+The \rulename{Ground} rule uses this concept to generate \texttt{extends} Wildcards.
+
+\end{description}
+
+\item[Step 4:] \textit{(Generating Result)} 
+Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
+The resulting $\Delta, \sigma$ is a correct solution.
+
+For this step to succeed there should only be four kinds of constraints left.
+\begin{enumerate}
+%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
+\item $\tv{a} \doteq \tv{b}$
+%\item $\wtv{a} \doteq \type{G}$
+\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) \subseteq \Delta_in$
+\item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
+\item\label{item:3} $\tv{a} \doteq \rwildcard{X}$
+\end{enumerate}
+
+%Each type placeholder $\tv{a}$ must solely appear on the left side of a constraint.
+\unify{} fails if there is any $\tv{a} \doteq \type{T}$ such that $\tv{a}$ occurs in $\type{T}$.
+For the cases \ref{item:1}, \ref{item:2}, and \ref{item:3} the placeholder $\tv{a}$
+cannot appear anywhere else in the constraint set.
+Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will not be able to process every constraint.
+
+% \begin{displaymath}
+% \deduction{
+% \wildcardEnv \cup \set{\wildcard{B}{\type{G}}{\type{G'}}} \vdash C \implies \Delta, \sigma
+% }{
+% \wildcardEnv \vdash C \implies \Delta \cup \set{\wildcard{B}{\type{G}}{\type{G'}}}, \sigma
+% }\quad \text{tph}(\type{G}) = \emptyset, \text{tph}(\type{G'}) = \emptyset,
+% \rwildcard{B} \notin \text{dom}(\Delta)
+% \quad \rulename{AddDelta}
+% \end{displaymath}
+\end{description}
+
+\subsection{Transformation Rules (Step 1)}
 Our \unify{} process uses a similar concept as the standard unification by Martelli and Montanari \cite{MM82},
 consisting of terms, relations and variables.
 Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
@@ -129,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}
 & 
 $
@@ -325,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
@@ -362,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}\\
@@ -402,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}
   & 
   $
@@ -462,7 +573,87 @@ and every added wildcard gets a fresh unique name.
 This ensures the wildcard environment $\wildcardEnv{}$ never
 gets the same wildcard twice.
 
-\subsection{Branching Step}
+
+\begin{figure}
+  \begin{center}
+    \leavevmode
+    \fbox{
+    \begin{tabular}[t]{l@{~}l}
+      \rulename{Subst} &
+                       $\begin{array}[c]{l}
+  \wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
+                         \hline
+  [\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
+  C \cup \set{\ntv{a} \doteq \type{T}}
+                       \end{array}
+                     \quad \begin{array}{c}
+                      \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}
+\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
+                  \hline
+[\type{T}/\wtv{a}]\wildcardEnv \vdash [\type{T}/\wtv{a}]C 
+                \end{array} \quad \wtv{a} \notin \type{T}
+$\\
+\\
+  \rulename{Normalize} &
+                   $\begin{array}[c]{l}
+\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
+                     \hline
+[\ntv{b}/\wtv{b}]\wildcardEnv \vdash [\ntv{b}/\wtv{b}]
+C \cup \set{\ntv{a} \doteq [\ntv{b}/\wtv{b}]\type{T}}
+                   \end{array}
+                 \quad \begin{array}{c}
+                  \wtv{b} \in \text{wtv}(\type{T})\\
+                  \ntv{b} \ \text{fresh}
+                 \end{array}$\\
+\\
+\rulename{Contract} &
+                 $\begin{array}[c]{l}
+\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
+                   \hline
+[\type{U}/\type{A}]\wildcardEnv \vdash [\type{U}/\type{A}]
+C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}}
+                 \end{array}
+               \quad \begin{array}{c}
+                \rwildcard{A} \in \text{fv}(\type{T})\\
+               \end{array}$\\
+\end{tabular}}
+\end{center}
+\caption{Substitution rules}\label{fig:subst-rules}
+\end{figure}
+
+\unify{} must not replace normal type placeholders with free variables
+except variables initially passed by $\Delta_{in}$.
+The \rulename{Subst} rule checks if a type $\type{T}$ contains any
+free variables or wildcard placeholders before replacing a normal type placeholder with it.
+%This ensures that free variables are never substituted for normal type placeholders.
+This ensures that a normal type placeholder is never replaced by a type containing free variables.
+A type solution for a normal type placeholder will never contain free variables.
+This is needed to guarantee well-formed type solutions and also keep free variables inside their scope
+(see challenge \ref{challenge3}).
+\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
+We do not keep replacements for wildcard placeholders and they will not show up in the final type solution.
+If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
+or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
+wildcards.
+
+\subsection{Branching Step (Step 2)}
 \unify{} is described as a nondeterministic algorithm.
 Some constraints allow for multiple transformations from which
 the algorithm has to pick the right one.
@@ -474,7 +665,9 @@ and gathers all possible type solutions.
 We skip the definition of this practice, because it is already described in \cite{TIforFGJ}
 and only needed for a proof of completeness.
 
-
+\subsection{Generate Result (Step 4)}
+The generation rules defined in figure \ref{fig:generation-rules} are similar to the other transformation rules but contain an additional part,
+the result output consisting of a wildcard environment and a set of unifier $\sigma$.
 
 \subsection{Adding Wildcards to the mix}
 %\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
@@ -514,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}}
 {
@@ -569,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}
@@ -620,150 +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}
 
-%\newcommand{\tw}[1]{\tv{#1}_?}
-\begin{description}
-  \item[Input:] An environment $\Delta'$
-and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}, \type{T} \doteq \type{T} \ldots}$
+% 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}$.
 
-\item[Output:]
-Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$
-\end{description}
+% The \rulename{Tame} rule eliminates wildcards. %TODO
+% This is done by setting the upper and lower bound to the same value.
 
-%The transformation steps are not applied all at once but in a specific order:
-\unify{} executes the following steps until a type solution is found:
-\begin{description}
-\item[Step 1:]
-Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
-starting with the \rulename{circle} rule.
+% The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
+% Their upper and lower bounds are fresh type variables.
 
-\item[Step 2:]
-%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
-%resume with step 4.
+% \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.
 
-The second step is nondeterministic.
-%\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
-%The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
-For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
-The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
-%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
-If atleast one transformation was applied in this step revert to step 1.
-Otherwise proceed with step 3.
-%This builds a search tree over multiple possible solutions.
-%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
-
-%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
-
-\textit{Hint:}
-When implementing this step via backtracking
-the rules \rulename{General} and \rulename{Super} should be tried first.
-% is the Same rule really necessary?
-The \rulename{Settle} and \rulename{Raise} rules should only be used when none of the rules in figure \ref{fig:step2-rules} can be applied.
-
-
-\item[Step 3:]
-Apply the rules in figure \ref{fig:cleanup-rules} exhaustively.
-\rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables.
-If a type placeholder is solely used as lower bound \rulename{Ground} can replace it with the bottom type.
-Otherwise the \rulename{Flatten} rule has to remove the wildcards responsible for the free variable.
-\text{Note:} Only one of those rules has to be applied per constraint.
-If the constraint set has been changed by one of these rules the algorithm must return to step 1.
-But if only the \rulename{SubElim} rule is applied or the constraint set is not changed at all,
-the algorithm can proceed with step 4.
-
-The cleanup step prepares the constraint set for the last step by applying the following concepts:
-%Two transformations are done which also help to remove unnecessary types from the solution set.
-\begin{description}
-\item[Bottom type]
-The bottom type $\bot$ is used to generate \texttt{? extends} wildcard definitions.
-This is the only possible solution when dealing with multiple upper bounds:
-$\tv{a} \lessdot \type{T}, \tv{a} \lessdot \type{S}$ is usually not a correct solution (given $\type{S}$ and $\type{T}$ are no subtypes of eachother).
-But if $\tv{a}$ is a lower bound of a wildcard it can be set to $\bot$.
-Those constraints only stay in the constraint set after the first step if $\type{S}$ and $\type{T}$ do not have a common subtype.
-The \rulename{Ground} rule uses this concept to generate \texttt{extends} Wildcards.
-
-\end{description}
-
-\item[Step 4:] \textit{(Generating Result)} 
-Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
-The resulting $\Delta, \sigma$ is a correct solution.
-
-For this step to succeed there should only be four kinds of constraints left.
-\begin{enumerate}
-%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
-\item $\tv{a} \doteq \tv{b}$
-%\item $\wtv{a} \doteq \type{G}$
-\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) \subseteq \Delta_in$
-\item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
-\item\label{item:3} $\tv{a} \doteq \rwildcard{X}$
-\end{enumerate}
-
-%Each type placeholder $\tv{a}$ must solely appear on the left side of a constraint.
-\unify{} fails if there is any $\tv{a} \doteq \type{T}$ such that $\tv{a}$ occurs in $\type{T}$.
-For the cases \ref{item:1}, \ref{item:2}, and \ref{item:3} the placeholder $\tv{a}$
-cannot appear anywhere else in the constraint set.
-Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will not be able to process every constraint.
-
-% \begin{displaymath}
-% \deduction{
-% \wildcardEnv \cup \set{\wildcard{B}{\type{G}}{\type{G'}}} \vdash C \implies \Delta, \sigma
-% }{
-% \wildcardEnv \vdash C \implies \Delta \cup \set{\wildcard{B}{\type{G}}{\type{G'}}}, \sigma
-% }\quad \text{tph}(\type{G}) = \emptyset, \text{tph}(\type{G'}) = \emptyset,
-% \rwildcard{B} \notin \text{dom}(\Delta)
-% \quad \rulename{AddDelta}
-% \end{displaymath}
-\end{description}
-
-
-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{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.
-
-\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.
@@ -820,73 +882,6 @@ which are used for the upper and lower bounds.
 
 % if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set.
 
-\begin{figure}
-  \begin{center}
-    \leavevmode
-    \fbox{
-    \begin{tabular}[t]{l@{~}l}
-      \rulename{Subst} &
-                       $\begin{array}[c]{l}
-  \wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
-                         \hline
-  [\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
-  C \cup \set{\ntv{a} \doteq \type{T}}
-                       \end{array}
-                     \quad \begin{array}{c}
-                      \ntv{a} \notin \type{T} \\
-                      \text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
-                     \end{array}$\\
-\\
-\rulename{Subst-WC} &$
-                \begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
-                  \hline
-[\type{T}/\wtv{a}]\wildcardEnv \vdash [\type{T}/\wtv{a}]C 
-                \end{array} \quad \wtv{a} \notin \type{T}
-$\\
-\\
-  \rulename{Normalize} &
-                   $\begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
-                     \hline
-[\ntv{b}/\wtv{b}]\wildcardEnv \vdash [\ntv{b}/\wtv{b}]
-C \cup \set{\ntv{a} \doteq [\ntv{b}/\wtv{b}]\type{T}}
-                   \end{array}
-                 \quad \begin{array}{c}
-                  \wtv{b} \in \text{wtv}(\type{T})\\
-                  \ntv{b} \ \text{fresh}
-                 \end{array}$\\
-\\
-\rulename{Contract} &
-                 $\begin{array}[c]{l}
-\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
-                   \hline
-[\type{U}/\type{A}]\wildcardEnv \vdash [\type{U}/\type{A}]
-C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}}
-                 \end{array}
-               \quad \begin{array}{c}
-                \rwildcard{A} \in \text{fv}(\type{T})\\
-               \end{array}$\\
-\end{tabular}}
-\end{center}
-\caption{Substitution rules}\label{fig:subst-rules}
-\end{figure}
-
-\unify{} must not replace normal type placeholders with free variables
-except variables initially passed by $\Delta_{in}$.
-The \rulename{Subst} rule checks if a type $\type{T}$ contains any
-free variables or wildcard placeholders before replacing a normal type placeholder with it.
-%This ensures that free variables are never substituted for normal type placeholders.
-This ensures that a normal type placeholder is never replaced by a type containing free variables.
-A type solution for a normal type placeholder will never contain free variables.
-This is needed to guarantee well-formed type solutions and also keep free variables inside their scope
-(see challenge \ref{challenge3}).
-\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
-We do not keep replacements for wildcard placeholders and they will not show up in the final type solution.
-If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
-or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
-wildcards.
-
 % \begin{example}{Free variables must not leave the scope of the surrounding \texttt{let} statement}
 
 % \noindent
@@ -1215,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}.
@@ -1313,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.
@@ -1408,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 
 
@@ -1458,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}