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

Fixes for Soundness Proof. Start with Capture Conversion at Subst-Step and introduce ccTVs

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-17 16:15:24 +02:00
parent fb22548d38
commit 2b57b092be
3 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
prolog.tex
View File

@ -132,6 +132,7 @@
\newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
%\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
\newcommand{\cctv}[1]{\ensuremath{\tv{#1}_!}}
\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
%\newcommand{\ntv}[1]{\tv{#1}}
\newcommand{\wcstore}{\ensuremath{\Delta}}

4
soundness.tex
View File

@ -193,7 +193,7 @@ By structural induction over the expression $\texttt{e}$.
% $\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[$\texttt{e}.\texttt{m}(\ol{e})$]
\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{
\ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
@ -313,6 +313,8 @@ This fact together with the presumption that every supplied type is well-formed
under the assumption that all supplied existential types are satisfying the premise.
All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
Only the \rulename{Adapt} rule is able to produce types neglecting the premise,
but is immediately corrected by the \rulename{Trim} rule.
% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!

12
unify.tex
View File

@ -575,6 +575,18 @@ gets the same wildcard twice.
\ntv{a} \notin \type{T} \\
\text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
\end{array}$\\
\\
\rulename{Subst} &
$\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
\hline
[\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
C \cup \set{\ntv{a} \doteq \type{T}}
\end{array}
\quad \begin{array}{c}
\ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
\text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
\end{array}$\\
\\
\rulename{Subst-WC} &$
\begin{array}[c]{l}