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

fix capture soundness proof

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-22 01:03:58 +01:00
parent ba8e2fadbb
commit e3a393520d
1 changed files with 11 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
soundness.tex
View File

@ -294,11 +294,17 @@ $\text{fv}(\sigma(\wctype{\Delta'}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(
\item[Capture] \item[Capture]
Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$. Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
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 From this point on they are treated like global variables and therefore we can assume there is a $\sigma'$ %and a $\Delta'$
$\Delta, \Delta' \vdash \sigma([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}}) with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}})
<: \sigma(\wctype{\Delta}{C}{\ol{T}})$, <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$.
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}})$. Only the wildcards from $\lessdotCC$ constraints are added to $\wildcardEnv$.
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$). %only the \rulename{Capture} step does that.
Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\exptype{C}{\ol{S}})
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$.
%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}})$ %with $\type{N}= \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}})$
%We can rename a fresh wildcard $\rwildcard{C}$ freely. %We can rename a fresh wildcard $\rwildcard{C}$ freely.