From 2702bf6cab26c8235d9e9bc4feb8896735025c57 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Mon, 10 Jun 2024 09:03:46 +0200
Subject: [PATCH] Start Implication Rules

---
 aspUnify.tex | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/aspUnify.tex b/aspUnify.tex
index ae526c6..9a48cb3 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -19,6 +19,11 @@
 %\renewcommand\UrlFont{\color{blue}\rmfamily}
 %\urlstyle{rm}
 %
+\include{prolog}
+\usepackage{mathpartir}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
 \begin{document}
 %
 \title{Global Type Inference for Java using SAT Solvers}
@@ -70,4 +75,78 @@ Java has adopted more and more type inference features over time.
 Currently Java only has local type inference.
 We want to bring type inference for Java to the next level.
 
+\section{Unify}
+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}
+}{
+    \type{N} \lessdot \type{T}
+}
+\and
+\inferrule[Subst-R]{
+    \tv{a} \doteq \type{N} \\
+    \type{T} \lessdot \tv{a} 
+}{
+    \type{T} \lessdot \type{N}
+}
+\and
+\inferrule[Fail]{
+    \type{T} \lessdot \type{N}\\
+    \type{T} \nless : \type{N} 
+}{
+    \emptyset
+}
+\and
+\inferrule[Fail]{
+    \exptype{C}{\ldots} \doteq \exptype{D}{\ldots}\\
+    \type{C} \neq \type{D}
+}{
+    \emptyset
+}
+\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
+}{
+    \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
+% --------------
+% N <. T
+
+% how to proof completeness and termination?
+% TODO: how to proof termination?
+
+\section{Completeness}
+To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
+
 \end{document}