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

Rework Implementation rules. Add comments to Completeness

Browse Source
This commit is contained in:
JanUlrich 2024-06-10 17:59:40 +02:00
parent 4efda6cae2
commit 5f549ae540
1 changed files with 98 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

130
aspUnify.tex
View File

@ -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}