Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ

constraints.tex

@@ -175,7 +175,7 @@ Those type variables count as regular types and can be held by normal type place
                       \orCons\set{
                       \set{ &
                       \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
+                      \tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
                       \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                       } \\
                       & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
@@ -348,6 +348,184 @@ 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)}.
 
+\subsection{Constraint Generation}
+The constraint generation is defined on a subset of Java displayed in figure \ref{fig:miniJavaSyntax}.
+The input language includes only a small set of expressions like method calls, field access and a elvis operator $\elvis$
+which acts as a replacement for if-else expressions.
+\begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
+$
+\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} & ::= & \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}})\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
+%\hline
+\end{array}
+$
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:miniJavaSyntax}
+\end{figure}
+
+We explain the process using the following example input.
+The classes \texttt{List} and \texttt{Id} are already fully typed and we want to create constraints for the class
+\texttt{CExample} now.
+
+\begin{lstlisting}{java}
+class Id{
+  <X> X id(X x){ return x; }
+}
+
+class List<X> {
+  <Y extends X> List<X> concat(List<Y> l){ ... }
+}
+
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}
+
+The first step of constraint generation is to assign type placeholders to every expression in the input program.
+Type placeholders also fill in for missing type annotations in method headers.
+
+\begin{lstlisting}{java}
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}  
+\begin{lstlisting}{java}
+class CExample{
+  (*@$\tv{a}$@*) example((*@$\tv{b}$@*) p1, (*@$\tv{c}$@*) p2) {
+    return ((p1:(*@$\tv{b}$@*)).id(p2:(*@$\tv{c}$@*)):(*@$\tv{d}$@*)).concat(p2:(*@$\tv{c}$@*)) : (*@$\tv{e}$@*);
+  }
+}
+\end{lstlisting}  
+
+The placeholders $\tv{a}-\tv{e}$ are freshly created in this example and added to every expression.
+The type of local variable expressions like \expr{p1} and \expr{p2} is already known and can be assigned directly.
+$\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case.
+The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$.
+
+Afterwards we create a method type environment $\mtypeEnvironment$ containing all method declarations.
+Each entry has the form $\texttt{m} : \generics{\ol{X \triangleleft N}} \ol{T} \to \type{T}$.
+The type arguments of the surrounding class and the type arguments of each method are merged together
+leading to the list $\generics{\type{X}, \type{Y} \triangleleft \type{X}}$ for the \texttt{concat} method
+($\triangleleft$ is short for \texttt{extends}).
+Also the type of the surrounding class is added to the parameter list of the method.
+This leads to the \texttt{id} method having two arguments.
+One is the \texttt{Id} class itself and the second one is the actual arguemnt of the method.
+
+$\mtypeEnvironment{} = \left\{ \begin{array}{l}
+\texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\
+\texttt{concat} : \generics{\type{X}, \type{Y} \triangleleft \type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{Y}} \to \exptype{List}{\type{X}}, \\
+\texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\
+\end{array} \right\} 
+$
+
+Note: type placeholders are used for the \texttt{example} method.
+
+Our constraint generation rules have the form:
+$\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$,
+that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$.
+
+%Inference-rule in the style of: https://dl.acm.org/doi/pdf/10.1145/345099.345100
+\begin{mathpar}
+  \inferrule[Method-Cons]{
+      \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{m} : \generics{\ol{Y \triangleleft N}}\type{T}_r, \overline{\type{T}} \to \type{T} \in { \mtypeEnvironment }\\
+      \overline{\wtv{b}}, \tv{x}, \overline{\tv{x}} \ \text{fresh} \\
+      C_m = \set{\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}} \cup
+      [\overline{\wtv{b}}/\ol{Y}]\set{ \tv{x} \lessdotCC \type{T}_r, \overline{\tv{x} \lessdotCC \type{T}}, \type{T} \lessdot \tv{a}, \overline{Y \lessdot N} } 
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m
+  }
+  \and
+%  \inferrule[Field-Cons]{
+%    \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+%    C_f = \set{}
+%  }{
+%    \mtypeEnvironment \vdash \expr{e}.\texttt{f} : \tv{a} \implies C \cup C_f \\
+%  }
+%  \and
+  \inferrule[Var-Cons]{
+  }{
+    \mtypeEnvironment \vdash \expr{x} : \tv{a} \implies \emptyset
+  }
+  \and
+  \inferrule[Elvis-Cons]{
+    \mtypeEnvironment \vdash \expr{e}_1 : \tv{e}_1 \implies C_1 \\
+    \mtypeEnvironment \vdash \expr{e}_2 : \tv{e}_2 \implies C_2
+  }{
+    \mtypeEnvironment \vdash \expr{e}_1 \elvis{} \expr{e}_2 : \tv{a} \implies C_1 \cup C_2 \cup \set{\tv{e}_1 \lessdot \tv{a}, \tv{e}_2 \lessdot \tv{a}}
+  }
+  \and
+  \inferrule[New-Cons]{
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{class} \ \exptype{D}{\ol{X \triangleleft N}} \set{ \ol{T\ f}; \ldots }
+  }{
+    \mtypeEnvironment \vdash \texttt{new}\ \type{D}(\ol{e}) : \tv{a} \implies \overline{C} \cup [\ol{\wtv{b}}/\ol{X}]\set{ \overline{\tv{e} \lessdot \type{T}}, \exptype{D}{\ol{X}} \lessdot \tv{a}, \ol{X \lessdot N} }
+  }
+\end{mathpar}
+
+According to the Method-Cons rule the constraints generated by the call to \texttt{id} are:
+$\mtypeEnvironment \vdash (p1:\tv{b}).id(p2:\tv{c}):\tv{d} \implies \set{\tv{b} \lessdot \tv{x}_1, \tv{c} \lessdot \tv{x}_2, \tv{x}_1 \lessdotCC \type{Id},
+\tv{x}_2 \lessdotCC \wtv{b}, \wtv{b} \lessdot \tv{d}}$.
+
+\subsection{Or-Constraints}
+In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated.
+Usually Java is able to determine which method to call based on the argument's types passed to the method. %'
+During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target.
+
+\begin{lstlisting}
+class String{
+  bool equals(String s){ .. }
+}
+class Int{
+  bool equals(Int i){ .. }
+}
+class OrConsExample{
+  m(a, b){
+    return a.equals(b);
+  }
+}
+\end{lstlisting}
+
+The method call to \texttt{equals} now has multiple possibilities.
+It could either be a call to the method in the class \texttt{Int} or in \texttt{String}.
+The method type environment therfore contains two versions of the \texttt{equals} method:
+
+$\mtypeEnvironment{} = \set{ \texttt{equals}_1 : \type{String}, \type{String} \to \type{bool}, 
+\texttt{equals}_2 : \type{Int}, \type{Int} \to \type{bool}}$
+
+The Or-Cons rule considers multiple declarations of the same method separately and joins all of them into a Or-Constraint.
+
+\begin{mathpar}
+  \inferrule[Or-Cons]{
+    \texttt{m}_1 \ldots \texttt{m}_n \in \text{dom}(\mtypeEnvironment{}) \\
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_1(\overline{\expr{e}}) : \tv{a} \implies C_1 \quad
+    \ldots \quad
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_n(\overline{\expr{e}}) : \tv{a} \implies C_n
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies \orCons{}(C_1, \ldots, C_n)
+  }
+\end{mathpar}
+
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}
 

rebuttal.md

@@ -0,0 +1,11 @@
+Thank you very much for your in depth reviews. We submitted the paper in an early stage to get early feedback and we'd appreciate the chance to submit a revised version. We are already working on the shortcomings you exposed in your reviews.
+
+A prototype implementation of the type inference algorithm is currently in development. We expect to use the prototype to explore the boundaries of what the algorithm is capable of. In the next revision of the paper we will report positive and negative examples as well as measurements of the algorithm's runtime.
+
+We plan to address the following points before submitting the revision:
+* Implementation of the algorithm and a showcase of working use cases.
+* Reworked and detailed soundness proof.
+* Provide better explanations and examples on constraint generation.
+* Fix typos, errors, ambiguous explanations, etc..
+* Discussion of the algorithm's complexity, our minimal aim is NP-Hardness, but we will try to draw comparisons to similar algorithms like the ones from Plümicke or Stadelmeier already mentioned in the paper.
+* A discussion on completeness and why a complete type inference algorithm for Java is not possible.

soundness.tex

@@ -1,95 +1,13 @@
 \section{Soundness}
 
-% \begin{lemma}
+The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
-% A sound TypelessFJ program is also sound under LetFJ type rules.
+During a let statement the environment $\Delta$ is extended by capture converted wildcards,
-% \begin{description}
+but only for the scope of the body of the let statement.
-%     \item[if:]
+The capture converted wildcards must not be used outside of the let statement.
-% $\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
+This is ensured by two things:
-% \end{description}
+The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
-% \end{lemma}
+travel one hop at the time through a constraint set.
-
+And the second one is the fact that normal type placeholders never contain free variables.
-% 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>
-
-% 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 
-
-% <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
-
-% 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
-
-% 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$.
-
-
-% 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}$.
-
-% $|\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
-
-% 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}
-
-
-% \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{lemma}{Well-formedness:}
-% TODO: 
-% \end{lemma}
 
 \unify{} calculates solutions for all normal type placeholders.
 Those are used for all untyped method's argument and return type.
@@ -99,28 +17,9 @@ A correct typing for method calls can be deducted from those type informations.
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
     \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] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
     \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.
-
-%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
-% only used inside the constraint the wildcard variable occurs
-% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost
-
-% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?
-
 \textit{Proof:}
 By structural induction over the expression $\texttt{e}$. 
 \begin{description}
@@ -141,32 +40,31 @@ that suffices the T-Let and T-Field type rules.
 The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely.
 We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$.
 %Constraints t1 <. x, x <. C<a>, T <. t2
-Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$ then
+Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
+$\sigma(\tv{a}) = \type{T}_2$ then
 \begin{itemize}
 \item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption
 \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}
 \item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$
-$\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var,
+First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
-$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
+%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
-and lemma \ref{lemma:unifySoundness}.
+%and lemma \ref{lemma:unifySoundness}.
-The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}:
+%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
-$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
+%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
-
+%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
-% The constraint a =. [a?/X]T finishes this case
+%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
-
+By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
-%TODO: WIP
+$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ 
-
+and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
-We know $\type{T}_2 f \in \text{fields}(\type{N})$ because 
+and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
-
+we can finally say 
-
+$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
-\item $\Delta, \Delta' | \Gamma \vdash t_1 : \type{T}_1$ by lemma \ref{lemma:unifySoundness} and the constraint $\tv{t_1} \lessdot \tv{x}$
+With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
+and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
+we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
+\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
 \end{itemize}
 
-    %TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
-    % but it also works with a subset of the initial constraints.
-    % the generated constraints do not share wildcard placehodlers with other constraints.
-    % can they contain free variables from other places? They could, but isolation prevents that.
-    % TODO: but how to proof?
 %generated constraints: t1 <. x, x <. N, T <. t2
         We are allowed to use capture conversion for $\expr{v}$ here.
         $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
@@ -174,62 +72,33 @@ We know $\type{T}_2 f \in \text{fields}(\type{N})$ because
         $\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}$
-    
-    % 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}.
-
-    % 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 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
-
-    % and then we can say by 
-    % Lemma:
-    % If [S/Y]U ok then S ok (TODO: proof!)
-
-    % So we do not have to proof S ok (but T)
-
-    % % 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
-
-    % $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
-    % %Easy, because unify only generates substitutions for normal type placeholders which are OK
 
+\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ 
+\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
+generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
+\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
+%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
+%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
+%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$,  $\sigma(\tv{a}) = \type{T}_2$.
+We omit the case where a capture conversion is not needed and
+assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$.
+We have to show T-Let and T-Call which leaves us with:
+\begin{itemize}
+    \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
+    \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
+    \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied.
+    Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are
+    solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$.
+    \begin{itemize}
+        \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
+        \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
+        there must be some $\ol{S}$ satisfying this premise.
+        
+        % what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints
+        %TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
+        \item 
+    \end{itemize}
+\end{itemize}
     \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{
@@ -293,6 +162,56 @@ We know $\type{T}_2 f \in \text{fields}(\type{N})$ because
 
 \end{description}
 
+
+During the unification process free variables can only move one hop at a time.
+Free variables originate from capture constraints.
+By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$
+are now free in the constraint $\type{N} \lessdot \type{T}$.
+The other way of free variables traveling into a constraint is by substitution.
+This is only possible if a constraint contains wildcard placeholders.
+And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in.
+
+This effect is transitive. Free variables travel from constraint to constraint.
+If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint,
+then free variables cannot travel there.
+
+\begin{lemma}
+    Free variables travel only 
+\end{lemma}
+
+\begin{lemma}{Free variables}\label{lemma:freeVariableScope}
+    Free variables never leave their scope.
+    If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set,
+    then it will never contain free variables used outside of it.
+$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
+
+and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
+and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
+
+then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
+\end{lemma}
+\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.
+
+If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders
+used for the method call.
+No other free variables can move into that scope.
+With this lemma we can further proof that during a method call only the generated free variables are used.
+
+% \begin{lemma}
+%     Free variables never leave their scope.
+%     $C' = \set{
+%         \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}},
+%         \overline{\tv{r} \lessdot \tv{a}}
+%     }$
+% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
+
+% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
+% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
+
+% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
+% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him
+% \end{lemma}
+
 % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
 % \begin{description}
 %     \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
@@ -419,11 +338,24 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 %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!
-
 \begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
 \unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
 \begin{description}
 \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
+\item[Then] there exists a substitution $\sigma'$ with:
+\begin{itemize}
+\item $\sigma \subseteq \sigma'$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$
+\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
+\end{itemize}
+\end{description}
+\end{lemma}
+
+\begin{lemma}{\unify{} Soundness:}%\label{lemma:unifySoundness}
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
+\begin{description}
+\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
 with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
 \item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
 \item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
@@ -614,7 +546,7 @@ Same as Subst
 \end{description}
 
 \begin{lemma}
-\label{lemma:unifyNoFreeVariablesInSupertype}
+\label{lemma:freeVariablesOnlyTravelOneHop}
 A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
 $\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
 Only free variables, which are part of the left side are used on the right side.