From 5f549ae5400d8b2b6f295837a17928e0b71f6699 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Mon, 10 Jun 2024 17:59:40 +0200
Subject: [PATCH] Rework Implementation rules. Add comments to Completeness

---
 aspUnify.tex | 130 ++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 98 insertions(+), 32 deletions(-)

diff --git a/aspUnify.tex b/aspUnify.tex
index 9a48cb3..fbd05dc 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -76,23 +76,86 @@ Currently Java only has local type inference.
 We want to bring type inference for Java to the next level.
 
 \section{Unify}
+Input: Every type placeholder must have an upper bound.
+Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a 
+
 We have to formulate the unification algorithm with implication rules.
 Those can be directly translated to ASP.
 \begin{mathpar}
 \inferrule[Subst-L]{
-    \tv{a} \doteq \type{N} \\
-    \tv{a} \lessdot \type{T}
+    \tv{a} \doteq \type{T}_1 \\
+    \tv{a} \lessdot \type{T}_2
 }{
-    \type{N} \lessdot \type{T}
+    \type{T}_1 \lessdot \type{T}_2
 }
 \and
 \inferrule[Subst-R]{
-    \tv{a} \doteq \type{N} \\
-    \type{T} \lessdot \tv{a} 
+    \tv{a} \doteq \type{T}_1 \\
+    \type{T}_2 \lessdot \tv{a} 
 }{
-    \type{T} \lessdot \type{N}
+    \type{T}_2 \lessdot \type{T}_1
 }
 \and
+\inferrule[Subst-Equal]{
+    \tv{a} \doteq \type{T}_1 \\
+    \tv{a} \doteq \type{T}_2 
+}{
+    \type{T}_1 \doteq \type{T}_2
+}
+\and
+\inferrule[Swap]{
+    \type{T}_1 \doteq \type{T}_2
+}{
+    \type{T}_2 \doteq \type{T}_1
+}
+\and
+\inferrule[Match]{
+    \tv{a} \lessdot \type{N}_1 \\
+    \tv{a} \lessdot \type{N}_2 \\
+    \type{N}_1 << \type{N}_2
+}{
+    \type{T}_1 \lessdot \type{T}_2
+}
+\and
+\inferrule[Adopt]{
+    \tv{a} \lessdot \tv{b} \\
+    \tv{b} \lessdot \type{T}
+}{
+    \tv{a} \lessdot \type{T}
+}
+\and
+\inferrule[Subst-Param]{
+    \tv{a} \doteq \type{N} \\
+    \tv{a} = \type{T}_i \\
+    \exptype{C}{\type{T}_1 \ldots \type{T}_n} <: \type{T} \\
+}{
+    \type{T}_i \doteq \type{N} \\
+}
+\and
+\inferrule[Adapt]{
+    \type{N}_1 \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
+    \type{N}_1 <: \exptype{C}{\type{S}_1 \ldots \type{S}_n} \\
+}{
+    \exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
+}
+\and
+\inferrule[Reduce]{
+    \exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
+}{
+    \type{S}_i \doteq \type{T}_i \\
+}
+\end{mathpar}
+
+\begin{mathpar}
+\inferrule[Super]{
+    \type{T} \lessdot \tv{a}\\
+    \type{T} <: \type{N} 
+}{
+    \tv{a} \doteq \type{N}
+}
+\end{mathpar}
+
+\begin{mathpar}
 \inferrule[Fail]{
     \type{T} \lessdot \type{N}\\
     \type{T} \nless : \type{N} 
@@ -108,35 +171,13 @@ Those can be directly translated to ASP.
 }
 \and
 \inferrule[Fail]{
-\tv{a} \lessdot \type{T}_1 \\
-\tv{a} \lessdot \type{T}_2 \\
-\type{T}_1 \nless : \type{T}_2 \\
-\type{T}_2 \nless : \type{T}_1
+\tv{a} \lessdot \type{N}_1 \\
+\tv{a} \lessdot \type{N}_2 \\
+\text{not}\ \type{N}_1 << \type{N}_2 \\
+\text{not}\ \type{N}_2 << \type{N}_1
 }{
     \emptyset
 }
-\and
-\inferrule[Swap]{
-    \type{T}_1 \doteq \type{T}_2
-}{
-    \type{T}_2 \doteq \type{T}_1
-}
-\and
-\inferrule[Adopt]{
-    \tv{a} \lessdot \type{T}_1 \\
-    \tv{a} \lessdot \type{T}_2 \\
-    \type{T}_1 <: \type{T}_2
-}{
-    \type{T}_1 \lessdot \type{T}_2
-}
-\and
-\inferrule[Subst-Param]{
-    \tv{a} \doteq \type{N} \\
-    \tv{a} = \type{T}_i \\
-    \exptype{C}{\type{T}_1 \ldots \type{T}_n} <: \type{T} \\
-}{
-    \type{T}_i \doteq \type{N} \\
-}
 \end{mathpar}
 % Subst
 % a =. N, a <. T, N <: T
@@ -149,4 +190,29 @@ Those can be directly translated to ASP.
 \section{Completeness}
 To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
 
+Completeness -> we never exclude a solution
+Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
+Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
+Proof:
+%Induction over every possible constraint variation:
+a =. T -> induction start
+a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
+in latter case: a <. T, a <. T'
+
+Proof that every type can be replaced by a Type Placeholder.
+% Whats with a =. T, can T be replaced by a Type Placeholder?
+% What is our finish condition? a <. T constraints stay, a =. b constraints stay.
+% Algorithm does not fail -> \emptyset if a solution exists
+% Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
+% by: a <. T -> a =.T
+%     a =. b, b =. T -> use the solution generation from other paper
+% TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
+
+Soundness -> we never make a wrong implication
+%$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
+If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
+constraints in the original constraint set and
+there exists a typing for the remaining type placeholders 
+so that the constraint set is satisfied.
+
 \end{document}