Start with cctv and soundness proof

modified:   relatedwork.tex

.gitignore

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

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
+\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,32 +38,32 @@
 \usepackage{arydshln}
 \usepackage{dashbox}
 
+\usepackage{mathpartir}
+
 \input{prolog}
 
+\begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 
 \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}{}{}
+%% END ANON
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\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.'
+%\category{} %optional, e.g. invited paper
 
-\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
-
-\category{} %optional, e.g. invited paper
-
-\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
 %\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
 
 %\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -77,28 +77,36 @@
 
 
 
-%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\EventEditors{John Q. Open and Joan R. Access}
-\EventNoEds{2}
-\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-\EventShortTitle{CVIT 2016}
-\EventAcronym{CVIT}
-\EventYear{2016}
-\EventDate{December 24--27, 2016}
-\EventLocation{Little Whinging, United Kingdom}
-\EventLogo{}
-\SeriesVolume{42}
-\ArticleNo{23}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \EventEditors{John Q. Open and Joan R. Access}
+% \EventNoEds{2}
+% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+% \EventShortTitle{CVIT 2016}
+% \EventAcronym{CVIT}
+% \EventYear{2016}
+% \EventDate{December 24--27, 2016}
+% \EventLocation{Little Whinging, United Kingdom}
+% \EventLogo{}
+% \SeriesVolume{42}
+% \ArticleNo{23}
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
 
 \maketitle
 
 %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,50 +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}
 
 \bibliography{martin}
 
 \appendix
+
+\include{soundness}
+\include{helpers}
 %\include{examples}
 %\input{exampleWildcardParameter}
 %\input{commonPatternsProof}

conclusion.tex

@@ -1,11 +1,138 @@
+%TODO: how are the challenges solved: Describe this in the last chapter with examples!
+\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}.
+
+When it comes to wildcards there is a limitation we couldn't find a good workaround:
+\begin{example} This example does not work:
+
+\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{lstlisting}
+  \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
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
+$\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{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}
+
+% 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>
+
+% % 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){}
+
+% Pair<?,?> p ...
+% List<?> l ...
+
+% make(t) { return t; }
+% triple(make(sameP(p)));
+% triple(make(sameL(l)));
+% \end{lstlisting}
+
+% \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 proof 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,7 +1,5 @@
-\section{Constraint generation}\label{chapter:constraintGeneration}
-% Our type inference algorithm is split into two parts.
-% A constraint generation step \textbf{TYPE} and a \unify{} step.
 
+\section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
 % It is possible to define the same method in multiple classes.
 % The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -14,26 +12,99 @@
 % 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
 
 The constraint generation works on the \TamedFJ{} language.
-This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation.
-We will focus on those parts.
-Here the new capture constraints and wildcard type placeholders are introduced.
+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.
 
-Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}
-Unknown types at the time of the constraint generation step are replaced with type placeholders.
-\begin{verbatim}
+%In \TamedFJ{} capture conversion is implicit.
+%To emulate Java's behaviour we assume the input program not to contain any let statements.
+%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
+
+Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
+
+%Constraints are generated on the basis of the program in A-Normal form.
+%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
+
+%This is shown in chapter \ref{sec:soundness}
+
+%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
+
+% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
+% Even variables have to be catched by a let statement first.
+% This behaviour emulates Java's implicit capture conversion.
+
+\subsection{ANF transformation}\label{sec:anfTransformation}
+\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
+%https://en.wikipedia.org/wiki/A-normal_form)
+Featherweight Java's syntax involves no \texttt{let} statement
+and terms can be nested freely similar to Java's syntax.
+Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
+but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
+To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
+%To convert it to \TamedFJ{} additional let statements have to be added.
+This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
+After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
+See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
+\begin{figure}
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
 m(l, v){
-  let x = x in x.add(v)
+    return l.add(v);
 }
-\end{verbatim}
+\end{lstlisting}
+    \end{minipage}%
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
+m(l, v) = 
+    let x1 = l in
+        let x2 = v in x1.add(x2)
+\end{lstlisting}
+\end{minipage}
+\end{figure}
 
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+\begin{figure}
+    \begin{center}
+$\begin{array}{lrcl}
+%\text{ANF}
+& \anf{\expr{x}} & = & \expr{x} \\
+& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
+& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
+& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
+& \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 $\tau$}\label{fig:anfTransformation}
+\end{figure}
 
+\begin{figure}
+  \center
+$
+\begin{array}{lrcl}
+%\hline
+\text{Terms} & t & ::= & \expr{x} \\
+& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
+& & \ \ | & t \elvis{} t \\
+%\hline
+\end{array}
+$
+\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
+\end{figure}
+
+\subsection{Constraint Generation Algorithm}
+% Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
+% Unknown types at the time of the constraint generation step are replaced with type placeholders.
+
+% The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+% Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
 
 The parameter types given to a generic method also affect their return type.
 During constraint generation the algorithm does not know the parameter types yet.
 We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
 $\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
+% TODO: Challenge examples!
 
 At points where a well-formed type is needed we use a normal type placeholder.
 Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
@@ -42,25 +113,12 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
+This is used for class generics see figure \ref{fig:constraints-for-classes}.
+The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
+containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 
-
-There are two different types of constraints:
-\begin{description}
-\item[$\lessdot$] \textit{Example:}
-
-$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
-
-\noindent
-Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
-which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
-This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
-For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
-\item[$\lessdotCC$] TODO
-% The \fjtype{} algorithm assumes capture conversions for every method parameter.
-\end{description}
-
 %Why do we need a constraint generation step?
 %% The problem is NP-Hard
 %% a method call, does not know which type it will produce
@@ -68,42 +126,37 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
-  \begin{align*}
-    % Type
-    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
-    \type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
-    % Constraints
-    \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
-    \consSet &::= \set{\constraints} && \text{constraint set}\\
-    % Method assumptions:
-    \methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
-                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
-                                                                \text{method
-                                                                type assumption}\\
-    \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
-                                                       assumption}\\
-    \mtypeEnvironment & ::= \overline{\methodAssumption} &
-                & \text{method type environment} \\
-    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
-  \end{align*}
-  \caption{Syntax of constraints and type assumptions}
+  \center
+\begin{tabular}{lcll}
+    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
+    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
+    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
+    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
+    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
+    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
+    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
+\end{tabular}
+  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
   \label{fig:syntax-constraints}
 \end{figure}
 
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{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
                   \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
-              \textbf{in} 
-                  & \begin{array}[t]{l}
+              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
+              & C = \begin{array}[t]{l}
                 \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
               \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
                \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
-                  \end{array}
+                  \end{array} \\
+              \textbf{in} 
+                  & (\Delta, C)
                 \end{array}
     \end{array}
   \end{gather*}
@@ -113,11 +166,11 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 \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{ &
@@ -136,12 +189,12 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 \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}
@@ -154,7 +207,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 \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} \\
@@ -164,16 +217,55 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
       \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() { ... }
@@ -184,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:
@@ -200,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
@@ -209,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}$
@@ -254,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.
@@ -263,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{\tv{r}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
-                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{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{a}}}}
-                  \end{array} 
-  \end{array}
-\end{displaymath}
-
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}
 
@@ -384,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}

martin.bib

@@ -50,6 +50,8 @@ keywords = {subtyping, type inference, principal types}
   SERIES       = {Lecture Notes in Artificial Intelligence}
 }
 
+
+
 @article{DM82,
     author={Luis Damas and Robin Milner},
     title={Principal type-schemes for functional programs},
@@ -66,13 +68,38 @@ keywords = {subtyping, type inference, principal types}
     month=Jan,
     year={1965}}
     
+@article{DBLP:journals/jcss/Milner78, 
+  author    = {Robin Milner},
+  title     = {A Theory of Type Polymorphism in Programming},
+  journal   = {Journal of Computer and Systems Sciences},
+  volume    = {17},
+  number    = {3},
+  pages     = {348--375},
+  year      = {1978},
+  url       = {https://doi.org/10.1016/0022-0000(78)90014-4},
+  doi       = {10.1016/0022-0000(78)90014-4},
+  timestamp = {Tue, 16 Feb 2021 14:04:22 +0100},
+  biburl    = {https://dblp.org/rec/journals/jcss/Milner78.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}   
+
 @article{MM82,
-    author={A. Martelli and U. Montanari},
-    title={An Efficient Unification Algorithm},
-    journal={ACM Transactions on Programming Languages and Systems},
-    volume={4},
-    pages={258-282},
-    year={1982}}
+author = {Martelli, Alberto and Montanari, Ugo},
+title = {An Efficient Unification Algorithm},
+year = {1982},
+issue_date = {April 1982},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {4},
+number = {2},
+issn = {0164-0925},
+url = {https://doi.org/10.1145/357162.357169},
+doi = {10.1145/357162.357169},
+journal = {ACM Trans. Program. Lang. Syst.},
+month = {apr},
+pages = {258–282},
+numpages = {25}
+}
 
 @InProceedings{Plue07_3,
   author = 	 {Martin Pl{\"u}micke},
@@ -326,6 +353,14 @@ articleno = {138},
 numpages = {22},
 keywords = {Null, Java Wildcards, Existential Types}
 }
+@inproceedings{AT16,
+author = {Amin, Nada and Tate, Ross},
+year = {2016},
+month = {10},
+pages = {838-848},
+title = {Java and scala's type systems are unsound: the existential crisis of null pointers},
+doi = {10.1145/2983990.2984004}
+}
 @InProceedings{TIforFGJ,
   author =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
   title =	{{Global Type Inference for Featherweight Generic Java}},
@@ -352,6 +387,16 @@ keywords = {Null, Java Wildcards, Existential Types}
   publisher={Addison-Wesley Professional}
 }
 
+@Book{GoJoStBrBuSm23,
+  author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex and Smith, Daniel},
+  title = "{The Java\textsuperscript{\textregistered} {L}anguage {S}pecification}",
+  Optpublisher = "Addison-Wesley",
+  url = {https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf},
+  edition = {{J}ava {S}{E} 21},
+  year = 2023,
+  OPtseries = {The Java series}
+}
+
 @inproceedings{semanticWildcardModel,
   title={Towards a semantic model for Java wildcards},
   author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
@@ -388,7 +433,7 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
 
-@inproceedings{10.1145/1449764.1449804,
+@inproceedings{javaTIisBroken,
 author = {Smith, Daniel and Cartwright, Robert},
 title = {Java type inference is broken: can we fix it?},
 year = {2008},
@@ -466,3 +511,61 @@ keywords = {Compilation, Java, generic classes, language design, language semant
   publisher={ACM New York, NY, USA}
 }
 
+@InProceedings{PH23,
+  author = 	 {Martin Pl{\"u}micke  and Daniel Holle},
+  title = 	 {Principal generics in {J}ava--{T}{X}},
+  crossref = {kps2023},
+  pages = 	 {122--143},
+  year = 	 {2023},
+  Opteditor = 	 {Thomas Noll and Ira Fesefeldt},
+  address = 	 {Aachen},
+  Optnumber = 	 {AIB-2023-03},
+  month = 	 {September},
+  series = {Aachener Informatik-Berichte (AIB)},
+  url = {https://publications.rwth-aachen.de/record/972197/files/972197.pdf#%5B%7B%22num%22%3A281%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C89.292%2C740.862%2Cnull%5D},
+  Optdoi = {10.18154/RWTH-2023-10034},
+  Optnote = {(to appear)}
+}
+
+@Proceedings{kps2023,
+  booktitle = 	 {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
+  year = 	 {2023},
+  editor = 	 {Noll, Thomas and Fesefeldt, Ira Justus},
+  number = 	 {AIB-2023-03},
+  series = 	 {Technical report / Department of Computer Science. - Informatik},
+  month = 	 {September},
+  organization = {RWTH Aachenen},
+  doi = {10.18154/RWTH-2023-10034}
+}
+
+@InProceedings{plue24_1,
+  author = 	 {Martin Pl{\"u}micke},
+  title = 	 {Avoiding the Capture Conversion in {J}ava--{T}{X}},
+  crossref =  {HKPTW24},
+  pages = 	 {109--115},
+  year = 	 {2023}
+}
+
+@proceedings{HKPTW24,
+  author = 	 {Daniel Holle and Jens Knoop and Martin Pl\"umicke and Peter Thiemann and Baltasar Tranc\'{o}n y Widemann},
+  booktitle = 	 {Proceedings of the 38th and 39th Annual Meeting of the GI Working Group Programming Languages and
+Computing Concepts},
+  institution =  {DHBW Stuttgart},
+  year = 	 {2024},
+  series = 	 {INSIGHTS -- Schriftenreihe der Fakult\"at Technik},
+  number = 	 {01/2024},
+  ISSN =         {2193-9098},
+  url =          {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights}
+}
+
+@article{wells1999typability,
+  title={Typability and type checking in System F are equivalent and undecidable},
+  author={Wells, Joe B},
+  journal={Annals of Pure and Applied Logic},
+  volume={98},
+  number={1-3},
+  pages={111--156},
+  year={1999},
+  publisher={Elsevier}
+}
+

prolog.tex

@@ -11,14 +11,21 @@
   escapeinside={(*@}{@*)},
   captionpos=t,float,abovecaptionskip=-\medskipamount
 }
+
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
 \lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
+\lstdefinestyle{constraints}{
+  basicstyle=\normalfont,
+  backgroundcolor=\color{red!20}
+}
 
 \newtheorem{recap}[note]{Recap}
 
+\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
+
 \newcommand{\tifj}{\texttt{TamedFJ}}
 
 \newcommand{\wcSep}{\vdash}
@@ -71,6 +78,9 @@
 \newcommand\subeq{\mathbin{\texttt{<:}}}
 \newcommand\extends{\ensuremath{\triangleleft}}
 
+\newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
+\newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
+
 \newcommand\rulename[1]{\textup{\textsc{(#1)}}}
 \newcommand{\generalizeRule}{General}
 
@@ -97,7 +107,8 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
-\newcommand{\type}[1]{\mathtt{#1}}
+\newcommand{\gtype}[1]{\type{#1}}
+\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
 \newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
@@ -105,7 +116,7 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 
-\newcommand{\letfj}{\emph{LetFJ}}
+\newcommand{\letfj}{\textbf{LetFJ}}
 \newcommand{\tph}{\text{tph}}
 
 \newcommand{\expr}[1]{\texttt{#1}}
@@ -121,8 +132,9 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
-\newcommand{\ntv}[1]{\tv{#1}}
+\newcommand{\cctv}[1]{\ensuremath{\tv{#1}_!}}
+\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

relatedwork.tex

@@ -0,0 +1,76 @@
+
+\section{Related Work}
+Igarashi et al \cite{FJ} define Featherweight Java
+and its generic sibling, Featherweight Generic Java. Their language is
+a functional calculus reduced to the bare essentials, they develop the full metatheory, they
+support generics, and study the type erasing transformation used by
+the Java compiler. Stadelmeier et. al. extends this approach by global type
+inference \cite{TIforFGJ}.
+
+\subsection{Wildcards in formal Java models}
+Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
+\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
+contains a formal description of wildcards. The Java Language Specification
+\cite{GoJoStBrBuSm23}  refers to \textsf{Wild~FJ} for the introduction of
+wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
+is introduced and proven as sound. Additionally, for a subset of Java a
+translation to the formal model is given, such that this subset is proven as
+sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
+introduced, which is proven as 
+sound, too. In this paper it is shown that the unsoundness of Java which is
+discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
+system. In \cite{TamingWildcards} finally a framework is presented which combines
+use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
+instance, it can be used to add use-site variance to Scala and extend the Java
+type system to infer the definition-site variance.
+
+Our calculus is mixture ...
+
+\subsection{Type inference}
+Some object-oriented languages like Scala, C\#, and Java perform
+\emph{local} type inference \cite{PT98,OZZ01}. Local type
+inference means that missing type annotations are recovered using only
+information from adjacent nodes in the syntax tree without long distance
+constraints. For instance, the type of a variable initialized with a
+non-functional expression or the return type of a method can be
+inferred. However, method argument types, in particular for recursive
+methods, cannot be inferred by local type inference.
+
+Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
+the gold standard for global type inference for languages with
+parametric polymorphism, which is used by ML-style languages. The fundamental idea
+of the algorithm is to enforce type equality by many-sorted type
+unification \cite{Rob65,MM82}. This approach is effective and results
+in so-called principal types because many-sorted unification is
+unitary, which means that there is at most one most general result.
+
+Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
+approach to Java. However, the presence of subtyping means that type
+unification is no longer unitary, but still finitary. Thus, there is
+no longer a single most general type, but any type is an instance of a
+finite set of maximal types (for more details see Section
+\ref{sec:unification}). Further work by the same author
+\cite{plue15_2,plue17_2},
+refines this approach by moving to a constraint-based algorithm and by
+considering lambda expressions and Scale-like function types.
+
+Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
+allows wildcards as any subsitution for type variables and disclaim the
+capture conversion. Instead he extended
+the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
+indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
+\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
+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{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 ???????
+

soundness.tex

@@ -1,126 +1,115 @@
 \section{Soundness}
 
-\newcommand{\CC}{\text{CC}}
+% \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
@@ -131,105 +120,139 @@ 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}}$,
     % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
     % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
-    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
+    % by proving every substitution in Unify is ok aslong as every type in the inputs is ok
     % S ok when all variables are in the environment and every L <: U and U <: Class-bound
     % 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}
 
@@ -272,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}
@@ -315,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!
@@ -388,6 +442,8 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Settle] Assumption, S-Trans
 \item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
 \item[\generalizeRule{}] by Assumption, because $C \subset C'$
+\item[Same] by S-Exists
+\item[SameW] %TODO
 \item[Adapt] Assumption, S-Extends, S-Trans
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
@@ -424,7 +480,7 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 % List<X> <. Y.List<Y>, free variables are either in 
 If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
 Otherwise 
-$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
+$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
 holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
 \item[Match] Assumption, S-Trans
 \item[Trim] Assumption and S-Exists
@@ -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

@@ -1,32 +1,85 @@
-\section{Syntax and Typing}\label{sec:tifj}
 
-The input syntax for our algorithm is shown in figure \ref{fig:syntax}
-and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
+\section{\TamedFJ{}}\label{sec:tifj}
+%LetFJ -> Output language!
+%TamedFJ -> ANF transformed input langauge
+%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
+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.
 
-Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
-The input language is designed to showcase type inference involving existential types.
-Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
-where existential types are implicitly \textit{opened} and \textit{closed}.
-
-Example: %TODO
-\begin{verbatim}
-class List<A> {
-    A head;
-    List<A> tail;
-
-    add(v) = new List(v, this);
+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{verbatim}
+\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}
 
-%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
-
-%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
-%and is solely used for examples.
-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.
-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}.
+\textit{Additional Notes:}%
+\begin{itemize}
+%\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.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
@@ -38,200 +91,38 @@ Additional language constructs can be added by implementing the respective const
 % on overriding methods, because their type is already determined.
 % Allowing overriding therefore has no implication on our type inference algorithm.
 
-The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
-Even variables have to be catched by a let statement first.
-This behaviour emulates Java's implicit capture conversion.
+% The output is a valid Featherweight Java program.
+% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
+% calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
 
+\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
 \begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
 $
 \begin{array}{lrcl}
-\hline
+%\hline
 \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
 \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
 \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
-\text{Terms} & t & ::= & \expr{x} \\
-& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
-& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
-& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
-& & \ \ | & t \elvis{} t \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e}.f\\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \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}}\\
-\hline
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
+%\hline
 \end{array}
 $
-\caption{\TamedFJ{} Syntax}\label{fig:syntax}
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:syntax}
 \end{figure}
 
-% \begin{figure}
-% $
-% \begin{array}{lrcl}
-% \hline
-% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
-% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
-% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
-% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
-% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
-% \text{Values} & v & ::= & \expr{x} \\
-% \text{Terms} & t & ::= & v \\
-% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\
-% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\
-% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\
-% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\
-% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
-% \hline
-% \end{array}
-% $
-% \caption{Input Syntax}\label{fig:syntax}
-% \end{figure}
-
-% \begin{figure}
-% $
-% \begin{array}{lrcl}
-% \hline
-% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
-% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
-% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
-% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
-% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
-% \text{Terms} & t & ::= & \expr{x} \\
-% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\
-% & & \ \ | & \expr{x}.f \\
-% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
-% & & \ \ | & t \elvis{} t \\
-% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
-% \hline
-% \end{array}
-% $
-% \caption{Input Syntax}\label{fig:syntax}
-% \end{figure}
-
-
-% \begin{figure}
-% $
-% \begin{array}{lrcl}
-% \hline
-% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
-% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
-% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
-% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
-% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{x}) = t \\
-% \text{Terms} & t & ::= & x \\
-% & & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
-% & & \ \ | & t.f\\
-% & & \ \ | & t.\texttt{m}(\overline{t})\\
-% & & \ \ | & t \elvis{} t\\
-% \text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
-% \hline
-% \end{array}
-% $
-% \caption{Input Syntax}\label{fig:syntax}
-% \end{figure}
-
-\subsection{ANF transformation}
-\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
-%https://en.wikipedia.org/wiki/A-normal_form)
-Featherweight Java's syntax involves no \texttt{let} statement
-and terms can be nested freely.
-This is similar to Java's syntax.
-To convert it to \TamedFJ{} additional let statements have to be added.
-This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
-The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
-and the output is a \TamedFJ{} program.
-
-\textit{Example:}\\
-\noindent
-\begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[style=fgj,caption=Featherweight Java]
-m(l, v){
-    return l.add(v);
-}
-\end{lstlisting}
-    \end{minipage}%
-    \hfill
-    \begin{minipage}{0.5\textwidth}
-\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
-m(l, v) = 
-    let x1 = l in
-        let x2 = v in x1.add(x2)
-\end{lstlisting}
-\end{minipage}
-
-
-% $
-% \begin{array}{|lrcl|l}
-% \hline
-% & & & \textbf{Featherweight Java Terms}\\
-% \text{Terms} & t & ::=
-% & \expr{x}
-% \\
-% & & \ \ |
-% & \texttt{new} \ \type{C}(\overline{t})
-% \\
-% & & \ \ |
-% & t.f
-% \\
-% & & \ \ | 
-% & t.\texttt{m}(\overline{t})
-% \\
-% & & \ \ | 
-% & t \elvis{} t\\
-% %
-% \hline
-% \end{array}
-% $
-
-\begin{figure}
-    \begin{center}
-$\begin{array}{lrcl}
-%\text{ANF}
-& \anf{\expr{x}} & = & \expr{x} \\
-& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
-& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
-& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
-& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2}
-\end{array}$
-\end{center}
-\caption{ANF Transformation}\label{fig:anfTransformation}
-\end{figure}
-
-% $
-% \begin{array}{lrcl|l}
-% \hline
-% & & & \textbf{Featherweight Java} & \textbf{A-Normal form}  \\
-% \text{Terms} & t & ::=
-% & \expr{x}
-% & \expr{x}
-% \\
-% & & \ \ |
-% & \texttt{new} \ \type{C}(\overline{t})
-% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
-% \\
-% & & \ \ |
-% & t.f
-% & \texttt{let}\ x = t \ \texttt{in}\ x.f
-% \\
-% & & \ \ | 
-% & t.\texttt{m}(\overline{t})
-% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
-% \\
-% & & \ \ | 
-% & t \elvis{} t
-% & t \elvis{} t\\
-% %
-% \hline
-% \end{array}
-% $
-
-
-% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
-% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
-% which can be used inside the type parameters $\ol{T}$.
-
 \begin{figure}[tp]
 \begin{center}
 $\begin{array}{l}
@@ -239,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}
@@ -260,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}
@@ -282,14 +176,15 @@ $\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}
         \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
         \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
         \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
-        \text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
+        \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -309,6 +204,7 @@ $\begin{array}{l}
         \Delta \vdash \bot \ \ok
     \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
     \typerule{WF-Top}\\
     \begin{array}{@{}c}
@@ -319,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}
@@ -479,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}
@@ -498,9 +395,10 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Method}\\
     \begin{array}{@{}c}
-        (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
-        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad 
+        \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
+        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \\
+        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
         \text{dom}(\triangle) = \ol{X} \quad \quad
         %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
         \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
@@ -508,37 +406,33 @@ $\begin{array}{l}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
     \typerule{T-Class}\\
     \begin{array}{@{}c}
-        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
-        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
-            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
+        %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
+        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
     \end{array}
 \end{array}$
-\\[1em]
+%\\[1em]
+\hfill
 $\begin{array}{l}
     \typerule{T-Program}\\
     \begin{array}{@{}c}
-        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
-        \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad 
-        \ldots \quad \quad 
-        \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad 
+        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \vdash \ol{L} : \mathtt{\Pi}_n
+    \mathtt{\Pi} \vdash \overline{D}
     \end{array}
 \end{array}$
 \end{center}
@@ -563,3 +457,7 @@ $\begin{array}{l}
 \end{array}$
 \caption{Field access}
 \end{figure}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:

todo-11.4.24

@@ -0,0 +1,16 @@
+- Eingangsbeispiel
+- Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
+- Zeile 52 steht LetFJ, muss eingeführt werden
+	- Operatoren motivieren. Denotable expressable types
+	Java macht CC implizit. Wir machen es mit let statements. Dadurch LetFJ einführen
+	- Java macht es anders. es gibt keine let statements
+	- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ
+
+- constraints nicht zu früh erwähnen
+	- informal erwähnen. um capture conversion zu behandeln braucht es neue constraints
+	- ganz vorne auflisten. Capture Conversion ist eine Neuheit
+
+Figure 4 und 5 in ein Bild
+ - man könnte die syntax unterlegen und sagen die unterlegten elemente fallen weg
+ - in beiden Syntaxen die Methodendeklarationen sollen gleich sein. beides return benutzen
+	- anschließend bei der convertierung zu TamedFJ nur die Änderungen beschreiben (Änderungen nur in Expressions)

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}