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

Soundness

Browse Source
This commit is contained in:
JanUlrich 2024-07-25 10:36:53 +02:00
parent a98c4b0486
commit 5e8a961e77
1 changed files with 22 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
soundness.tex
View File

@ -1,5 +1,14 @@
\section{Soundness}
The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
During a let statement the environment $\Delta$ is extended by capture converted wildcards,
but only for the scope of the body of the let statement.
The capture converted wildcards must not be used outside of the let statement.
This is ensured by two things:
The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
travel one hop at the time through a constraint set.
And the second one is the fact that normal type placeholders never contain free variables.
% \begin{lemma}
% A sound TypelessFJ program is also sound under LetFJ type rules.
% \begin{description}
@ -150,14 +159,14 @@ $\sigma(\tv{a}) = \type{T}_2$ then
First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
%and lemma \ref{lemma:unifySoundness}.
%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}:
%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}.
%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$
and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}
and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
we can finally say
$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
@ -167,7 +176,7 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
\end{itemize}
% method call: a1 <c C<a>, a2 <c C<b>, a3 <c b?
% here lemma:unifyNoFreeVariablesInSupertype can be used too
% here lemma:freeVariablesOnlyTravelOneHop can be used too
%TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
% but it also works with a subset of the initial constraints.
@ -237,6 +246,14 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
% $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
% %Easy, because unify only generates substitutions for normal type placeholders which are OK
\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\
\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$.
\item[$\texttt{v}.\texttt{m}(\ol{v})$]
Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
@ -621,7 +638,7 @@ Same as Subst
\end{description}
\begin{lemma}
\label{lemma:unifyNoFreeVariablesInSupertype}
\label{lemma:freeVariablesOnlyTravelOneHop}
A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
$\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
Only free variables, which are part of the left side are used on the right side.