Soundness for Prepare and Capture
This commit is contained in:
Andreas Stadelmeier
parent
e3a393520d
commit
b775045d17
@ -272,62 +272,24 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
|
||||
\item[Adopt] Assumption, because $C \subset C'$
|
||||
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
|
||||
\item[Prepare]
|
||||
%To show
|
||||
%$\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$ by S-Exists we have to proof:
|
||||
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}})$ 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')$.
|
||||
Given a $\wctype{\Delta_c}{C}{\ol{S}} \lessdot \wcNtype{\Delta''}{N}$
|
||||
we get $\Delta, \Delta', \overline{\Delta} \vdash \exptype{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$ with $\Delta_c \subseteq \overline{\Delta}$.
|
||||
|
||||
$\text{fv}(\sigma'(\wctype{\Delta_c}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta_c)$
|
||||
and $\text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$ implies $\text{dom}(\Delta_c) \cap \text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$.
|
||||
|
||||
% 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}})$
|
||||
% and $\Delta' \subseteq \Delta''$ and $\text{fv}(\Delta) = \emptyset$.
|
||||
% Due to $\text{fv}(\sigma(\wctype{\Delta'}{C}{\ol{S}})) = \emptyset$
|
||||
% and $\text{fv}(\sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})) = \emptyset$
|
||||
% we can say %TODO: Can we really say that? Weakening does not apply (it is the other direction than weakening)
|
||||
% $\Delta, \Delta' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$
|
||||
% which implies
|
||||
% $\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$.
|
||||
No free variables on both sides also mean we do not need $\overline{\Delta}$.
|
||||
Therefore we can say $\Delta, \Delta' \vdash \wctype{\Delta_c}{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$.
|
||||
|
||||
\item[Capture]
|
||||
Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
|
||||
From this point on they are treated like global variables and therefore we can assume there is a $\sigma'$ %and a $\Delta'$
|
||||
with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}})
|
||||
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$.
|
||||
Only the wildcards from $\lessdotCC$ constraints are added to $\wildcardEnv$.
|
||||
%only the \rulename{Capture} step does that.
|
||||
We get a $\sigma'$ %and a $\Delta'$
|
||||
with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}}) <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$
|
||||
where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ by assumption.
|
||||
\unify{} performs a capture conversion only on $\lessdotCC$ constraints.
|
||||
Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\exptype{C}{\ol{S}})
|
||||
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$.
|
||||
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.
|
||||
|
||||
%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
|
||||
% $\Delta, \Delta' \vdash [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} <: \wctype{\Delta}{C}{\ol{T}}$ $\implies$
|
||||
% $\Delta' \Delta \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$
|
||||
|
||||
%we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
|
||||
%which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.
|
||||
|
||||
% If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$
|
||||
% we have to show $\set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}, \Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
|
||||
% which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$.
|
||||
% The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.
|
||||
|
||||
%If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
|
||||
%$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and
|
||||
%the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh).
|
||||
%The assumption implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{C}{\type{U'}}{\type{L'}}}})$
|
||||
%, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$.
|
||||
|
||||
%We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation.
|
||||
\item[Reduce]
|
||||
|
||||
%Assumption and S-Exists.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user