From 0678f96ef41317ba6b498a4a90f8961e96ea08a7 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Wed, 12 Jun 2024 00:31:36 +0200
Subject: [PATCH] Add Split rules. Add Soundness, Completeness definitions

---
 aspUnify.tex | 52 ++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 38 insertions(+), 14 deletions(-)

diff --git a/aspUnify.tex b/aspUnify.tex
index 3e19a70..fd03ebc 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -164,14 +164,32 @@ Those can be directly translated to ASP.
 \end{mathpar}
 
 \begin{mathpar}
-\inferrule[Super]{
-    \type{T} \lessdot \tv{a}\\
-    \type{T} <: \type{N} 
-}{
-    \tv{a} \doteq \type{N}
-}
+    \inferrule[Super]{
+        \type{T} \lessdot \tv{a}\\
+        \type{T} <: \type{N} 
+    }{
+        \tv{a} \doteq \type{N}
+    }
 \end{mathpar}
 
+\begin{mathpar}
+    \inferrule[Split-L]{
+        \tv{a} \lessdot \tv{b}\\
+        \tv{a} \lessdot \type{N}\\
+    }{
+        \tv{b} \lessdot \type{N}
+    }
+    \and
+    \vline
+    \and
+    \inferrule[Split-R]{
+        \tv{a} \lessdot \tv{b}\\
+        \tv{a} \lessdot \type{N}\\
+    }{
+        \type{N} \lessdot \tv{b}
+    }
+\end{mathpar}
+            
 \begin{mathpar}
 \inferrule[Fail]{
     \type{T} \lessdot \type{N}\\
@@ -216,9 +234,9 @@ Result:
 \inferrule[Solution-Sub]{
     \tv{a} \lessdot \type{N}_1, \ldots, \tv{a} \lessdot \type{N}_n \\
     \forall i: \type{N} <: \type{N}_i \\
-    \sigma(\tv{a}) = \emptyset
+    \text{not}\ \tv{a} \doteq \type{N}
 }{
-    \sigma'(\tv{a}) = \type{N}
+    \sigma(\tv{a}) = \type{N}
 }
 \end{mathpar}
 % Subst
@@ -257,16 +275,22 @@ constraints in the original constraint set and
 there exists a typing for the remaining type placeholders 
 so that the constraint set is satisfied.
 
+\begin{theorem}{Soundness}\label{lemma:soundness}
+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}
+$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$.
+\end{theorem}
+%Problem: We do not support multiple inheritance
+
 \begin{lemma} \label{lemma:subtypeOnly}
-If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the right side of $\tv{a} \lessdot \type{T}$ constraints.
-\end{lemma}
-\begin{lemma} \label{lemma:reduceToSigma}
-If algorithm is successfull and $\type{T} \lessdot \tv{a}$ or $\tv{a} \doteq \type{T}$ or $\type{T} \doteq \tv{a}$ then $\sigma(\tv{a}) \neq \emptyset$
+If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
 \end{lemma}
 Proof:
 Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
-Then either the Solution-Sub generates a $\sigma'$ or the Solution rule can be used due to lemma \ref{lemma:reduceToSigma}.
-Or algorithm terminates with $\emptyset$.
+Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
 
 The Solution-Sub rule is always correct.