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

Cleanup

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-11 23:30:09 +01:00
parent cbd0a48ca6
commit 5074c21943
1 changed files with 1 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
soundness.tex
View File

@ -235,15 +235,10 @@ If there is a solution for a constraint set $C$, then there is also a solution f
\item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$
\item[then] $ (\sigma', \Delta') = \unify{}( C')$ \item[then] $ (\sigma', \Delta') = \unify{}( C')$
\end{description} \end{description}
\textit{Proof:}
%TODO
\end{lemma} \end{lemma}
\textit{Proof:} \textit{Proof:}
%TODO: is it true even? %TODO
The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.
\begin{lemma}\label{lemma:unifySoundness} \begin{lemma}\label{lemma:unifySoundness}
The \unify{} algorithm only produces correct output. The \unify{} algorithm only produces correct output.