Commit 01de136a authored by Mickael Laurent's avatar Mickael Laurent
Browse files

completeness (version 1)

parent 64a3d646
......@@ -1159,12 +1159,14 @@
\end{definition}
\begin{lemma}
Let $t$ a type and $\ts$ a type scheme.
We have $\tsrep{t\tsand\ts} \leq \tsrep{t} \land \tsrep{\ts}$.
\begin{align*}
&\forall t,\ts.\ \tsrep{t\tsand\ts} \leq t \land \tsrep{\ts}\\
&\forall \ts_1,\ts_2.\ \tsrep{\apply {\ts_1}{\ts_2}} \leq \apply {\tsrep {\ts_1}}{\tsrep {\ts_2}}
\end{align*}
\end{lemma}
\begin{proof}
Straightfoward, by induction on the structure of $\ts$.
Straightfoward, by induction on the structure of $\ts$.
\end{proof}
\begin{lemma}[Monotonicity of the algorithm] Let $\Gamma$, $\Gamma'$ and $e$ such that $\Gamma'\leqA^e \Gamma$ and $\tyof e \Gamma \neq \tsempty$. We have:
......@@ -1181,8 +1183,7 @@
Let's prove the first property: $\tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}$.
We will focus on showing $\tyof e {\Gamma'} \leq \tyof e {\Gamma}$. The property $\tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}$
can be proved in a very similar way, by using the fact that $\tsrep {t \tsand \ts} \leq t \land \tsrep {\ts}$,
$\tsrep {\ts_1 \tsor \ts_2} = \tsrep {\ts_1} \vee \tsrep {\ts_2}$ and $\tsrep {\ts_1 \tstimes \ts_2} = \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}$.
can be proved in a very similar way, by using the fact that operators on type schemes like $\tsand$ or $\apply {} {}$ are also monotone.
(Note that the only rule that introduces the type scheme constructor $\tsfun {\_}$ is \Rule{Abs\Aa}.)
If $\Gamma' = \bot$ we can conclude directly with the rule \Rule{Efq}.
......@@ -1299,7 +1300,7 @@
$\bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma',e,t} (\varpi) \leq \bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi)$.
The rest follows.
\end{proof}
\end{proof}
\begin{theorem}[Completeness of the algorithm for positive derivations]
For any $\Gamma$, $e$, $t$ such that we have a positive derivation of $\Gamma \vdash e:t$,
......@@ -1307,18 +1308,129 @@
More precisely:
\begin{align*}
&\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a positive derivation } \Rightarrow \tsrep{\tyof e \Gamma} \leq t \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, e, t, t', \varpi.\ \pvdash \Gamma e t \varpi:t' \text{ has a positive derivation } \Rightarrow \env {\Gamma,e,t} (\varpi) \leq t' \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a positive derivation } \Rightarrow \tsrep{\tyof e \Gamma} \leq t\\
&\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a positive derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for $n_o$ large enough)}
\end{align*}
\end{theorem}
\begin{proof}
We proceed by induction on the declarative derivation.
We proceed by induction on the derivation.
Let's prove the first property. We have a positive derivation of $\Gamma \vdash e:t$.
If $\Gamma = \bot$, we can conclude directly using \Rule{Efq\Aa}. Thus, let's suppose $\Gamma \neq \bot$.
If $e=x$ is a variable, then the derivation only uses \Rule{Env}, \Rule{Inter} and \Rule{Subs}.
We can easily conclude just be using \Rule{Var\Aa}. Thus, let's suppose $e$ is not a variable.
If $e\in\dom\Gamma$, we can have the rule \Rule{Env} in our derivation, but there can only be
\Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation).
Thus, we can build a positive derivation of $\Gamma \vdash e:t'$ that does not use the rule \Rule{Env} on $e$
and such that $t'\land \Gamma(e) \leq t$. Thus we have a positive derivation for $\Gamma\setminus\{e\} \vdash e:t'$.
By using the induction hypothesis we deduce that $\tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t'$.
Thus, by looking at the rule \Rule{Env\Aa},
we deduce $\tsrep{\tyof e \Gamma} \leq \Gamma(e) \land \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t$.
It concludes this case, so let's assume $e\not\in\dom\Gamma$.
Now we analyze the last rule of the derivation:
\begin{description}
\item[\Rule{Env}] Impossible case ($e\not\in\dom\Gamma$).
\item[\Rule{Inter}] By using the induction hypothesis we get $\tsrep{\tyof e \Gamma} \leq t_1$ and $\tsrep{\tyof e \Gamma} \leq t_2$.
Thus, we have $\tsrep{\tyof e \Gamma} \leq t_1 \land t_2$.
\item[\Rule{Subs}] Trivial using the induction hypothesis.
\item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Const\Aa}.
Thus this case is trivial.
\item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{App\Aa}.
Let $\ts_1 = \tyof {e_1} \Gamma$ and $\ts_2 = \tyof {e_2} \Gamma$.
With the induction hypothesis we have $\tsrep {\ts_1} \leq \arrow {t_1} {t_2}$ and $\tsrep {\ts_2} \leq t_1$, with $t_2=t$.
According to the descriptive definition of $\apply{}{}$, we have
$\apply{\tsrep {\ts_1}}{\tsrep {\ts_2}} \leq \apply{\arrow {t_1}{t_2}}{t_1} \leq t_2$.
As we also have $\tsrep{\apply {\ts_1} {\ts_2}} \leq \apply{\tsrep {\ts_1}}{\tsrep {\ts_2}}$,
we can conclude that $\tyof e \Gamma \leq t_2=t$.
\item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Abs\Aa}.
This case is straightforward using the induction hypothesis.
\item[\Rule{Abs-}] This case is impossible (the derivation is positive).
\item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Case\Aa}.
By using the induction hypothesis and the monotonicity lemma, we get $\tsrep{\ts_1}\leq t$ and $\tsrep{\ts_2}\leq t$.
So we have $\tsrep{\ts_1\tsor\ts_2}=\tsrep{\ts1}\vee\tsrep{\ts2}\leq t$.
\item[\Rule{Proj}] Quite similar to the case \Rule{App}.
\item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Pair\Aa}.
We just use the induction hypothesis and the fact that $\tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}$.
\end{description}
\
Now, let's prove the second property. We have a positive derivation of $\Gamma \evdash e t \Gamma'$.
\begin{description}
\item[\Rule{Env}] Trivial.
\item[\Rule{Inter}] TODO%By using the induction hypothesis we get $\tsrep{\tyof e \Gamma}$
\item[\Rule{Base}] Any value of $n_o$ will give $\Refine {e,t} \Gamma \leqA \Gamma$, even $n_o = 0$.
\item[\Rule{Path}] We have $\Gamma' = \Gamma_1,(\occ e \varpi:t')$.
By applying the induction hypothesis on the premise $\Gamma \evdash e t \Gamma_1$, we have
$\RefineStep {e,t}^n (\Gamma) = \Gamma_2$ with $\Gamma_2 \leqA \Gamma_1$ for a certain $n$.
We now proceed by induction on the derivation $\pvdash {\Gamma_1} e t \varpi:t'$
to show that we can obtain $\env {\Gamma'',e,t} (\varpi) \leq t'$ with $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$
for a certain $n'$. It is then easy to conclude by taking $n_o = n+n'$.
\begin{description}
\item[\Rule{PSubs}] Trivial using the induction hypothesis.
\item[\Rule{PInter}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi) \leq t_1$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$ and
$\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$. By taking $n'=\max (n_1,n_2)$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi) \leq t_1 \land t_2 = t'$.
\item[\Rule{PTypeof}] By using the outer induction hypothesis we get
$\tsrep{\tyof {\occ e \varpi} {\Gamma_2}} \leq t'$.
Moreover we have $\env {\Gamma_2,e,t} (\varpi) \leq \tsrep{\tyof {\occ e \varpi} {\Gamma_2}}$
(by definition), thus we can conclude directly.
\item[\Rule{PEps}] Trivial.
\item[\Rule{PAppR}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2'$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$, $\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$
and $t_2\land t_2' \simeq \Empty$.
By taking $n'=\max (n_1,n_2) + 1$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \RefineStep {e,t} (\Gamma_1'')$
and $\Gamma'' \leqA \RefineStep {e,t} (\Gamma_2'')$.
In consequence, we have $\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}} \leq \env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}$
(by definition of $\RefineStep {e,t}$).
We also have, by monotonicity, $\env {\Gamma'',e,t} (\varpi) \leq t_2'$.
As $t_2\land t_2' \simeq \Empty$, we have:
\begin{align*}
&\apply {(\arrow {t_1} {t_2})} {(\dom{\arrow {t_1} {t_2}}\setminus(\neg t_1))}\\
&\simeq \apply {(\arrow {t_1} {t_2})} {t_1} \simeq t_2 \leq \neg t_2'
\end{align*}
Thus, by using the declarative definition of $\worra {} {}$, we know that
$\worra {(\arrow {t_1} {t_2})} {t_2'} \leq \neg t_1$.
According to the properties on $\worra {} {}$ that we have proved in the proof of the monotonicity lemma,
we can deduce:
\begin{align*}
&t_1 \land \worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)}\\
&\leq t_1 \land \worra {(\arrow {t_1} {t_2})} {t_2'} \leq t_1 \land \neg t_1 \simeq \Empty
\end{align*}
And thus $\worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)} \leq \neg t_1$.
It concludes this case.
\item[\Rule{PAppL}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$ and
$\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$. By taking $n'=\max (n_1,n_2)$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi.0) \leq \neg (\arrow {t_1} {\neg t_2}) = t'$.
\item[\Rule{PPairL}] Trivial using the induction hypothesis and the descriptive definition of $\bpi_1$.
\item[\Rule{PPairR}] Trivial using the induction hypothesis and the descriptive definition of $\bpi_2$.
\item[\Rule{PFst}] Trivial using the induction hypothesis.
\item[\Rule{PSnd}] Trivial using the induction hypothesis.
\end{description}
\end{description}
\end{proof}
......@@ -1328,9 +1440,8 @@
More precisely:
\begin{align*}
&\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has an acceptable derivation } \Rightarrow \tyof e \Gamma \leq t \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, e, t, t', \varpi.\ \pvdash \Gamma e t \varpi:t' \text{ has an acceptable derivation } \Rightarrow \env {\Gamma,e,t} (\varpi) \tsand \tyof {\occ e \varpi} \Gamma \leq t' \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has an acceptable derivation } \Rightarrow \tyof e \Gamma \leq t\\
&\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has an acceptable derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for $n_o$ large enough)}
\end{align*}
\end{theorem}
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment