Add Solution rules

aspUnify.tex

@@ -126,6 +126,8 @@ Those can be directly translated to ASP.
     \type{T}_2 \doteq \type{T}_1
 }
 \and
+\inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
+\and
 \inferrule[Match]{
     \tv{a} \lessdot \type{N}_1 \\
     \tv{a} \lessdot \type{N}_2 \\
@@ -141,13 +143,13 @@ Those can be directly translated to ASP.
     \tv{a} \lessdot \type{T}
 }
 \and
-\inferrule[Subst-Param]{
+% \inferrule[Subst-Param]{
-    \tv{a} \doteq \type{N} \\
+%     \tv{a} \doteq \type{N} \\
-    \tv{a} = \type{T}_i \\
+%     \tv{a} = \type{T}_i \\
-    \exptype{C}{\type{T}_1 \ldots \type{T}_n} <: \type{T} \\
+%     \exptype{C}{\type{T}_1 \ldots \type{T}_n} \lessdot \type{T} \\
-}{
+% }{
-    \type{T}_i \doteq \type{N} \\
+%     \type{T}_i \doteq \type{N} \\
-}
+% }
 \and
 \inferrule[Adapt]{
     \type{N}_1 \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
@@ -190,6 +192,45 @@ Those can be directly translated to ASP.
     }
 \end{mathpar}
 
+Result:
+\begin{mathpar}
+\inferrule[Solution]{
+    \tv{a} \doteq \type{N} \\
+    \tv{a} \notin \type{N}
+}{
+    \sigma(\tv{a}) = \type{N}
+}
+\and
+\inferrule[Solution-Sub]{
+    \tv{a} \lessdot \exptype{C_1}{\ol{T_1}}, \ldots, \tv{a} \lessdot \exptype{C_n}{\ol{T_n}} \\
+    \forall i: \type{C_m} << \type{C_i} \\
+    \text{not}\ \tv{a} \doteq \type{N}
+}{
+    \sigma(\tv{a}) = \exptype{C_m}{\ol{T_m}}
+}
+\and
+\inferrule[Solution]{
+    \tv{a} \doteq \type{G}
+}{
+    \sigma(\tv{a}) = \type{N}
+}
+\and
+\inferrule[Unfold]{
+    \tv{b} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} 
+}{
+    \type{T}_i \doteq \type{T}_i 
+}
+\and
+\inferrule[Subst-Param]{
+    \tv{a} \doteq \type{G} \\
+    \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
+}{
+    \type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{G}, \ldots \type{T}_n}
+}
+\end{mathpar}
+
+Fail:
+            
 \begin{mathpar}
 \inferrule[Fail]{
     \type{T} \lessdot \type{N}\\
@@ -222,31 +263,18 @@ Those can be directly translated to ASP.
 }
 \end{mathpar}
 
-Result:
-\begin{mathpar}
-\inferrule[Solution]{
-    \tv{a} \doteq \type{N} \\
-    \tv{a} \notin \type{N}
-}{
-    \sigma(\tv{a}) = \type{N}
-}
-\and
-\inferrule[Solution-Sub]{
-    \tv{a} \lessdot \type{N}_1, \ldots, \tv{a} \lessdot \type{N}_n \\
-    \forall i: \type{N} <: \type{N}_i \\
-    \text{not}\ \tv{a} \doteq \type{N}
-}{
-    \sigma(\tv{a}) = \type{N}
-}
-\end{mathpar}
 % Subst
 % a =. N, a <. T, N <: T
 % --------------
 % N <. T
 
+% a <. List<b>, b <. List<a>
+
 % how to proof completeness and termination?
 % TODO: how to proof termination?
 
+The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
+
 \section{Completeness}
 To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
 
@@ -280,10 +308,36 @@ if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
 then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
 \end{theorem}
 
-\begin{theorem}{Completeness}
+\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
-$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$.
+\newcommand*\ncasesmakelabel[1]{Case #1}
-\end{theorem}
+
-%Problem: We do not support multiple inheritance
+\newenvironment{subproof}
+  {\def\proofname{Subproof}%
+   \def\qedsymbol{$\triangleleft$}%
+   \proof}
+  {\endproof}
+Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
+\begin{proof}
+  \begin{enumerate}[ncases]
+    \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
+        Solution-Sub
+    Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
+    \item $\tv{a} \doteq \type{N}$.
+    Solution
+    \item $\tv{a} \lessdot \tv{b}$.
+    There must be a $\tv{a} \lessdot \type{N}$
+    \begin{subproof}
+    $\sigma(\tv{a}) = \type{Object}$, 
+    $\sigma(\tv{b}) = \type{Object}$.
+    \end{subproof}
+    \item $\type{N} \lessdot \tv{a}$.
+    \begin{subproof}
+    $2$
+    \end{subproof}
+  \end{enumerate}
+  And more text.
+\end{proof}
+
 
 \begin{lemma} \label{lemma:subtypeOnly}
 If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
@@ -295,28 +349,20 @@ Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be us
 The Solution-Sub rule is always correct.
 
 Proof:
-\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
-\newcommand*\ncasesmakelabel[1]{Case #1}
-
-\newenvironment{subproof}
-  {\def\proofname{Subproof}%
-   \def\qedsymbol{$\triangleleft$}%
-   \proof}
-  {\endproof}
 
+\begin{theorem}{Completeness}
+$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
+and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
+\end{theorem}
+%Problem: We do not support multiple inheritance
 \begin{proof}
   \begin{enumerate}[ncases]
     \item $\tv{a} \lessdot \type{N}$.
-    \begin{subproof}
+        Solution-Sub
-    If $\tv{a} \notin \type{N}$ then $\sigma(\tv{a}) = \type{N}$ otherwise there is no type solution.
-    $\sigma(\tv{a}) = \type{B}$ with $type{B} \triangleleft [\type{B}/\tv{a}]\type{N}$
-    \end{subproof}
     \item $\tv{a} \doteq \type{N}$.
-    \begin{subproof}
+    Solution
-    $\sigma(\tv{a}) = \type{N}$
+    \item $\tv{a} \lessdot \tv{b}$.
-    \end{subproof}
+    There must be a $\tv{a} \lessdot \type{N}$
-    \item $C \cup \tv{a} \lessdot \tv{b}$.
-    If 
     \begin{subproof}
     $\sigma(\tv{a}) = \type{Object}$, 
     $\sigma(\tv{b}) = \type{Object}$.