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

Fix Capture Soundness

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-17 12:53:36 +01:00
parent 8907cac94a
commit 5578415ed3
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
soundness.tex
View File

@ -277,7 +277,10 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
Given a constraint $ \wctype{\Delta'}{C}{\ol{S}} \lessdot \wctype{\Delta''}{C}{\ol{T}}$ first the \rulename{Prepare} rule
then the \rulename{Capture} rule is applied.
Therefore we can assume $\Delta, \Delta' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta''}{C}{\ol{T}})$ (see proof for \rulename{Capture})
which implies $\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\Delta''}{C}{\ol{T}})$.
which implies $\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\Delta''}{C}{\ol{T}})$ by S-Exists:
$\text{fv}(\sigma(\wctype{\Delta''}{C}{\ol{T}})) = \emptyset$ implies $\text{dom}(\Delta'') \cap \text{fv}(\sigma(\wctype{\Delta''}{C}{\ol{T}})) = \emptyset$.
$\text{fv}(\sigma(\wctype{\Delta'}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta')$.
% Under the assumption there exists a $\Delta''$ with
% $\Delta, \Delta'' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$
@ -294,9 +297,10 @@ Everytime the \rulename{Capture} rule is invoked we add the freshly generated fr
They are from this point on treated like global variables and therefore we can assume $\sigma(\wildcardEnv \cup \ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ in
$\Delta, \Delta' \vdash \sigma([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}})
<: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
which implies $\Delta, \Delta'/\set{\ol{\wildcard{C}{U}{L}}} \vdash \type{N} <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
with $\wcNtype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{N} = \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}})$
We can rename a fresh wildcard $\rwildcard{C}$ freely.
which implies $\Delta, \Delta'/\set{\ol{\wildcard{C}{U}{L}}} \vdash \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
As long as $\ol{C} \notin \text{fv}(\sigma(\wctype{\Delta}{C}{\ol{T}}))$ (TODO: do we need to set the right side to not contain free variables?: NO! because all free variables are inside $\Delta$).
%with $\type{N}= \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}})$
%We can rename a fresh wildcard $\rwildcard{C}$ freely.
% If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
% If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ the preposition holds because