Change Prepare rule to simpler version
This commit is contained in:
Andreas Stadelmeier
parent
521dee7fa2
commit
bc4fcaf43c
@ -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:
|
||||
@ -271,7 +273,25 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
|
||||
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
|
||||
\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(\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 \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.
|
||||
|
||||
12
unify.tex
12
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}
|
||||
$
|
||||
|
||||
Loading…
Reference in New Issue
Block a user