stan/WLP2024
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add Split rules. Add Soundness, Completeness definitions

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-12 00:31:36 +02:00
parent 837bed5752
commit 0678f96ef4
1 changed files with 38 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
aspUnify.tex
View File

@ -164,12 +164,30 @@ 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}
@ -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.