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

Add Result rules

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-11 16:29:34 +02:00
parent 5fc1972c41
commit 255e3854ef
1 changed files with 44 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
aspUnify.tex
View File

@ -187,6 +187,13 @@ Those can be directly translated to ASP.
\emptyset
}
\and
\inferrule[Fail-Sigma]{
\tv{a} \doteq \type{N} \\
\tv{a} \in \type{N}
}{
\emptyset
}
\and
\inferrule[Fail]{
\tv{a} \lessdot \type{N}_1 \\
\tv{a} \lessdot \type{N}_2 \\
@ -196,6 +203,24 @@ Those can be directly translated to ASP.
\emptyset
}
\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 \\
\sigma(\tv{a}) = \emptyset
}{
\sigma'(\tv{a}) = \type{N}
}
\end{mathpar}
% Subst
% a =. N, a <. T, N <: T
% --------------
@ -232,6 +257,10 @@ constraints in the original constraint set and
there exists a typing for the remaining type placeholders
so that the constraint set is satisfied.
Proof:
Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
Or algorithm terminates with $\emptyset$.
Proof:
\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
\newcommand*\ncasesmakelabel[1]{Case #1}
@ -245,13 +274,24 @@ Proof:
\begin{proof}
Some text or \texttt{\string\leavevmode} (so the enumerate starts in another line)
\begin{enumerate}[ncases]
\item $\tv{a} \lessdot \type{T}$ where $\tv{a} \notin \type{T}$.
\item $\tv{a} \lessdot \type{N}$.
\begin{subproof}
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
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 Bar.
\item $\tv{a} \doteq \type{N}$.
\begin{subproof}
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
$\sigma(\tv{a}) = \type{N}$
\end{subproof}
\item $C \cup \tv{a} \lessdot \tv{b}$.
If
\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.