From bc4fcaf43c6244ea9afeffe2dcf5c45ae0cefcd8 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 16 Jan 2024 18:03:54 +0100 Subject: [PATCH] Change Prepare rule to simpler version --- soundness.tex | 53 +++++++++++++++++++++++++++++++++++++++------------ unify.tex | 12 ++++-------- 2 files changed, 45 insertions(+), 20 deletions(-) diff --git a/soundness.tex b/soundness.tex index ae338c2..1c594f5 100644 --- a/soundness.tex +++ b/soundness.tex @@ -196,14 +196,16 @@ This rule is only applied for the outer wildcard environments for each type. \begin{lemma} The \unify{} algorithm only produces correct output for constraints not containing free variables. \begin{description} -\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ +\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ %\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ -\item[Then] there exists a $\Delta'$ with: -$\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ -and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ +\item[Then] there exists a $\sigma'$ with: +$\sigma \subseteq \sigma'$ and +$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$ +and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$, +otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$ % and $\sigma(\type{T'}) = \sigma(\type{T'})$. -The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ +% The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ % Unify cannot guarantee that only wildcards declared on the left side are used. Example input: @@ -269,9 +271,27 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$ \item[Adapt] Assumption, S-Extends, S-Trans \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{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}}) <: \sigma(\wcNtype{\Delta''}{N})$ by S-Exists we have to proof: + + + +We set $\Delta' = \sigma(\wildcardEnv)$. + +\begin{gather} +\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\ +\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\ +\label{rp:3} +\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\ +\label{rp:4} +\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset\\ +[\ol{A}/\ol{T}] = \ol{T} %TODO: rename T +\end{gather} + \item[Prepare] To show -$\Delta \vdash \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof: +$\Delta \vdash \sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$ by S-Exists we have to proof: \begin{gather} \Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\ \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\ @@ -284,11 +304,12 @@ $\Delta \vdash \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} We know \begin{gather} - \ol{S} = [\ol{\wtv{a}}/\ol{A}]\ol{T}\\ + \sigma(\ol{S}) = [\ol{\wtv{a}}/\ol{A}]\ol{T}\\ + \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\ol{A}]\ol{U}\\ + [\ol{\wtv{a}}/\ol{A}]\ol{L} \lessdot \ol{\wtv{a}}\\ \text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\ \label{rp:fv2} \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset - %TODO \end{gather} \ref{rp:fv2} implies \ref{rp:4}. @@ -297,10 +318,18 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U}}{\type and therefore \ref{rp:3}. \item[Capture] -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}})$ +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 +$\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. + +% 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. diff --git a/unify.tex b/unify.tex index c061718..91cfd4b 100644 --- a/unify.tex +++ b/unify.tex @@ -380,19 +380,15 @@ Their upper and lower bounds are fresh type variables. \begin{array}[c]{@{}ll} \begin{array}[c]{l} \wildcardEnv \vdash - C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ + C \cup \, \set{ \wcNtype{\Delta}{S} \lessdot \wcNtype{\Delta'}{N} } \\ \hline \vspace*{-0.4cm}\\ - \wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}} - \vdash C \cup \, \set{ - \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}}, - \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} } + \wildcardEnv \vdash + C \cup \, \set{ \wcNtype{\Delta}{S} \lessdotCC \wcNtype{\Delta'}{N} } \\ \end{array} %\quad \ol{Y} = \textit{fresh}(\ol{X}) \quad \begin{array}[c]{l} - \ol{\rwildcard{C}} \ \text{fresh}\\ - \text{fv}(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}}) = \emptyset\\ - \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset + \text{fv}(\wcNtype{\Delta}{S}, \wcNtype{\Delta'}{N}) = \emptyset \end{array} \end{array} $