Big Cleanup (delete comments in soundness proof
This commit is contained in:
Andreas Stadelmeier
parent
5e8a961e77
commit
01a9165a9e
188
soundness.tex
188
soundness.tex
@ -9,97 +9,6 @@ The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that
|
||||
travel one hop at the time through a constraint set.
|
||||
And the second one is the fact that normal type placeholders never contain free variables.
|
||||
|
||||
% \begin{lemma}
|
||||
% A sound TypelessFJ program is also sound under LetFJ type rules.
|
||||
% \begin{description}
|
||||
% \item[if:]
|
||||
% $\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
|
||||
% \end{description}
|
||||
% \end{lemma}
|
||||
|
||||
% TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
|
||||
% Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
|
||||
% %what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
|
||||
% % if the Y is later needed for an equals: same(id(x), x2)
|
||||
% Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
|
||||
% Or it is a generic method call: is it possible to use any free wildcards here?
|
||||
% let empty
|
||||
|
||||
% <X> Box<X> empty()
|
||||
% same(Box<?>, empty())
|
||||
% let p1 : X.Box<X> = Box<?> in let
|
||||
% X.Box<X> <. Box<x>
|
||||
% Box<e> <. Box<x>
|
||||
|
||||
% boxin(empty()), Box2<?>
|
||||
|
||||
% Where can a problem arise? When we use free wildcards before they are freed.
|
||||
% But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
|
||||
% Here y = Y and x = X but
|
||||
|
||||
% <X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
|
||||
% <X> Pair<?, X> left() { return null; }
|
||||
% <X> Pair<X, ?> right() { return null; }
|
||||
|
||||
% <X> Box<X> id(Box<? extends Box<X>> x)
|
||||
% here it could be beneficial to use a free wildcard as the parameter X to have it later
|
||||
% Box<?> x = ...
|
||||
% same(id(x), id(x)) <- this will be accepted by TI
|
||||
|
||||
% let left : X,Y.Pair<X,Y> = left() in
|
||||
% let right : Pair<X,Y> = right() in
|
||||
|
||||
% Compromise:
|
||||
% - Generate constraints so that they comply with LetFJ
|
||||
% - Propose a version which is close to Java
|
||||
|
||||
% Version for LetFJ:
|
||||
% Is it still possible to do the capture conversion in form of constraints?
|
||||
% X.C<X> <. C<x>
|
||||
% T <. X.C<X>
|
||||
% how to proof: X.C<X> ok
|
||||
|
||||
|
||||
% If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
|
||||
% then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
|
||||
% This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
|
||||
|
||||
|
||||
% Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
|
||||
|
||||
% \textit{Proof} by structural induction.
|
||||
% \begin{description}
|
||||
% \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
|
||||
% $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
|
||||
% and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
|
||||
|
||||
% $|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
|
||||
|
||||
% \item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
|
||||
% \item[$\texttt{e}.f$] given let x : T = e' in x
|
||||
% let x : T = e' in let xf = x.f in xf
|
||||
|
||||
% Required:
|
||||
% $ \Delta | \Theta \vdash e' : \type{T}_1$
|
||||
% $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
|
||||
% $\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
|
||||
|
||||
% \end{description}
|
||||
|
||||
|
||||
% \textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
|
||||
% First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
|
||||
% m(p) = e => let xp = p in [xp/p]e
|
||||
% x1.m(x2) => let xm = x1.m(x2=) in xm
|
||||
% x.f => let xf = x.f in xf
|
||||
% Then we have to proof there is never a wildcard used before it is declared.
|
||||
% Wildcards are introduced by the capture conversions and nothing else.
|
||||
|
||||
|
||||
% \begin{lemma}{Well-formedness:}
|
||||
% TODO:
|
||||
% \end{lemma}
|
||||
|
||||
\unify{} calculates solutions for all normal type placeholders.
|
||||
Those are used for all untyped method's argument and return type.
|
||||
A correct typing for method calls can be deducted from those type informations.
|
||||
@ -108,28 +17,9 @@ A correct typing for method calls can be deducted from those type informations.
|
||||
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
|
||||
\begin{description}
|
||||
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
|
||||
and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ % and let $\Delta= \Delta_u \cup \Delta'$
|
||||
% $\Delta, \Delta' \vdash $
|
||||
% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
|
||||
% and $\vdash \ol{L} : \mtypeEnvironment{}$
|
||||
% and $\Gamma \subseteq \mtypeEnvironment{}$
|
||||
% \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
|
||||
% and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
|
||||
%\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
|
||||
\item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
% Regular type placeholders represent type annotations.
|
||||
% These are the only types a \wildFJ{} program needs to be correctly typed.
|
||||
% The type placeholders flagged as wildcard placeholders are intermediate types
|
||||
% used in let statements and as type parameters for generic method calls.
|
||||
|
||||
%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
|
||||
% only used inside the constraint the wildcard variable occurs
|
||||
% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost
|
||||
|
||||
% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?
|
||||
|
||||
\textit{Proof:}
|
||||
By structural induction over the expression $\texttt{e}$.
|
||||
\begin{description}
|
||||
@ -175,14 +65,6 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
|
||||
\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
|
||||
\end{itemize}
|
||||
|
||||
% method call: a1 <c C<a>, a2 <c C<b>, a3 <c b?
|
||||
% here lemma:freeVariablesOnlyTravelOneHop can be used too
|
||||
|
||||
%TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
|
||||
% but it also works with a subset of the initial constraints.
|
||||
% the generated constraints do not share wildcard placehodlers with other constraints.
|
||||
% can they contain free variables from other places? They could, but isolation prevents that.
|
||||
% TODO: but how to proof?
|
||||
%generated constraints: t1 <. x, x <. N, T <. t2
|
||||
We are allowed to use capture conversion for $\expr{v}$ here.
|
||||
$\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
|
||||
@ -190,70 +72,22 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
|
||||
$\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
|
||||
because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
|
||||
$\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
|
||||
% \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$]
|
||||
% $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
|
||||
% $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
|
||||
% $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
|
||||
% \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
|
||||
% then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
|
||||
% $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
|
||||
% %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
|
||||
% %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
|
||||
|
||||
% The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
|
||||
|
||||
% We now show
|
||||
% $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
|
||||
% by the T-Field rule.
|
||||
% $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
|
||||
% $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
|
||||
% because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
|
||||
% $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
|
||||
% and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
|
||||
|
||||
% $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
|
||||
|
||||
% X.List<X> <. List<a?>
|
||||
% $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
|
||||
% $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
|
||||
% TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
|
||||
% by proving every substitution in Unify is ok aslong as every type in the inputs is ok
|
||||
% S ok when all variables are in the environment and every L <: U and U <: Class-bound
|
||||
% This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
|
||||
|
||||
% If S ok and T <. S , then Unify generates a T ok
|
||||
|
||||
% S typeinference:
|
||||
% T <: [S/Y]U
|
||||
% We apply the following lemma
|
||||
% Lemma
|
||||
% if T ok and T <: S then S ok
|
||||
|
||||
% until
|
||||
% T = [S/Y]U
|
||||
|
||||
% and then we can say by
|
||||
% Lemma:
|
||||
% If [S/Y]U ok then S ok (TODO: proof!)
|
||||
|
||||
% So we do not have to proof S ok (but T)
|
||||
|
||||
% % T_r <: C<T> (S is in T)
|
||||
% % Is C<T> ok?
|
||||
% % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
|
||||
% % this together with the X <. N constraints proofs T_r ok
|
||||
|
||||
% $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
|
||||
% %Easy, because unify only generates substitutions for normal type placeholders which are OK
|
||||
|
||||
\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\
|
||||
\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
|
||||
generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
|
||||
\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
|
||||
We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
|
||||
\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
|
||||
where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$.
|
||||
|
||||
%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
|
||||
%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
|
||||
%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$.
|
||||
We omit the case where a capture conversion is not needed and
|
||||
assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$.
|
||||
We have to show T-Let and T-Call which leaves us with:
|
||||
\begin{itemize}
|
||||
\item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
|
||||
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
|
||||
\item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash $
|
||||
\end{itemize}
|
||||
\item[$\texttt{v}.\texttt{m}(\ol{v})$]
|
||||
Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
|
||||
We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
|
||||
|
||||
Loading…
Reference in New Issue
Block a user