Commit f1870345 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add \Aats to rules in the proofs

parent c90a109b
...@@ -961,34 +961,34 @@ The results about this new type system will be used in \ref{sec:proofs_algorithm ...@@ -961,34 +961,34 @@ The results about this new type system will be used in \ref{sec:proofs_algorithm
theorem for the algorithmic type system presented in \ref{sec:algorules}. theorem for the algorithmic type system presented in \ref{sec:algorules}.
\begin{mathpar} \begin{mathpar}
\Infer[Efq\Aa] \Infer[Efq\Aats]
{ } { }
{ \Gamma, (e:\Empty) \vdashAts e': \Empty } { \Gamma, (e:\Empty) \vdashAts e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}} { \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\qquad \qquad
\Infer[Var\Aa] \Infer[Var\Aats]
{ } { }
{ \Gamma \vdashAts x: \Gamma(x) } { \Gamma \vdashAts x: \Gamma(x) }
{ x\in\dom\Gamma} { x\in\dom\Gamma}
\\ \\
\Infer[Env\Aa] \Infer[Env\Aats]
{ \Gamma\setminus\{e\} \vdashAts e : \ts } { \Gamma\setminus\{e\} \vdashAts e : \ts }
{ \Gamma \vdashAts e: \Gamma(e) \tsand \ts } { \Gamma \vdashAts e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma \text{ and } e \text{ not a variable}} { e\in\dom\Gamma \text{ and } e \text{ not a variable}}
\qquad \qquad
\Infer[Const\Aa] \Infer[Const\Aats]
{ } { }
{\Gamma\vdashAts c:\basic{c}} {\Gamma\vdashAts c:\basic{c}}
{c\not\in\dom\Gamma} {c\not\in\dom\Gamma}
\\ \\
\Infer[Abs\Aa] \Infer[Abs\Aats]
{\Gamma,x:s_i\vdashAts e:\ts_i'\\ \ts_i'\leq t_i} {\Gamma,x:s_i\vdashAts e:\ts_i'\\ \ts_i'\leq t_i}
{ {
\Gamma\vdashAts\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I} \Gamma\vdashAts\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
} }
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma} {\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\\ \\
\Infer[App\Aa] \Infer[App\Aats]
{ {
\Gamma \vdashAts e_1: \ts_1\\ \Gamma \vdashAts e_1: \ts_1\\
\Gamma \vdashAts e_2: \ts_2\\ \Gamma \vdashAts e_2: \ts_2\\
...@@ -998,19 +998,19 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -998,19 +998,19 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
{ \Gamma \vdashAts {e_1}{e_2}: \ts_1 \circ \ts_2 } { \Gamma \vdashAts {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma} { {e_1}{e_2}\not\in\dom\Gamma}
\\ \\
\Infer[Case\Aa] \Infer[Case\Aats]
{\Gamma\vdashAts e:\ts_0\\ {\Gamma\vdashAts e:\ts_0\\
\Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\ \Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashAts e_2 : \ts_2} \Refine {e,\neg t} \Gamma \vdashAts e_2 : \ts_2}
{\Gamma\vdashAts \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2} {\Gamma\vdashAts \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma} { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
\\ \\
\Infer[Proj\Aa] \Infer[Proj\Aats]
{\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any} {\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)} {\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma} {\pi_i e\not\in\dom\Gamma}
\Infer[Pair\Aa] \Infer[Pair\Aats]
{\Gamma \vdashAts e_1:\ts_1 \and \Gamma \vdashAts e_2:\ts_2} {\Gamma \vdashAts e_1:\ts_1 \and \Gamma \vdashAts e_2:\ts_2}
{\Gamma \vdashAts (e_1,e_2):{\ts_1}\tstimes{\ts_2}} {\Gamma \vdashAts (e_1,e_2):{\ts_1}\tstimes{\ts_2}}
{(e_1,e_2)\not\in\dom\Gamma} {(e_1,e_2)\not\in\dom\Gamma}
...@@ -1092,11 +1092,11 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1092,11 +1092,11 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
If $\Gamma = \bot$, we trivially have $\Gamma \vdash e:t$ with the rule \Rule{Efq}. If $\Gamma = \bot$, we trivially have $\Gamma \vdash e:t$ with the rule \Rule{Efq}.
Let's assume $\Gamma \neq \bot$. Let's assume $\Gamma \neq \bot$.
If $e=x$ is a variable, then the last rule used is \Rule{Var\Aa}. If $e=x$ is a variable, then the last rule used is \Rule{Var\Aats}.
We can derive $\Gamma \vdash x:t$ by using the rule \Rule{Env} and \Rule{Subs}. We can derive $\Gamma \vdash x:t$ by using the rule \Rule{Env} and \Rule{Subs}.
So let's assume that $e$ is not a variable. So let's assume that $e$ is not a variable.
If $e\in\dom\Gamma$, then the last rule used is \Rule{Env\Aa}. If $e\in\dom\Gamma$, then the last rule used is \Rule{Env\Aats}.
Let $t'\in\tsint{\ts}$ such that $t'\land\Gamma(e)\leq t$. Let $t'\in\tsint{\ts}$ such that $t'\land\Gamma(e)\leq t$.
The induction hypothesis gives $\Gamma\setminus\{e\} \vdash e:t'$ The induction hypothesis gives $\Gamma\setminus\{e\} \vdash e:t'$
(the premise uses the same $e$ but the domain of $\Gamma$ is strictly smaller). (the premise uses the same $e$ but the domain of $\Gamma$ is strictly smaller).
...@@ -1106,17 +1106,17 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1106,17 +1106,17 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
Now, let's suppose that $e\not\in\dom\Gamma$. Now, let's suppose that $e\not\in\dom\Gamma$.
\begin{description} \begin{description}
\item[$e=c$] The last rule is \Rule{Const\Aa}. We derive easily $\Gamma \vdash c:t$ with \Rule{Const} and \Rule{Subs}. \item[$e=c$] The last rule is \Rule{Const\Aats}. We derive easily $\Gamma \vdash c:t$ with \Rule{Const} and \Rule{Subs}.
\item[$e=x$] Already treated. \item[$e=x$] Already treated.
\item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$] \item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$]
The last rule is \Rule{Abs\Aa}. The last rule is \Rule{Abs\Aats}.
We have $\bigwedge_{i\in I} \arrow {t_i}{s_i} \leq t$. We have $\bigwedge_{i\in I} \arrow {t_i}{s_i} \leq t$.
Using the definition of type schemes, let $t'=\bigwedge_{i\in I} \arrow {t_i}{s_i} \land \bigwedge_{j\in J} \neg \arrow {t'_j}{s'_j}$ such that $\Empty \neq t' \leq t$. Using the definition of type schemes, let $t'=\bigwedge_{i\in I} \arrow {t_i}{s_i} \land \bigwedge_{j\in J} \neg \arrow {t'_j}{s'_j}$ such that $\Empty \neq t' \leq t$.
The induction hypothesis gives, for all $i\in I$, $\Gamma,x:s_i\vdash e':t_i$. The induction hypothesis gives, for all $i\in I$, $\Gamma,x:s_i\vdash e':t_i$.
Thus, we can derive $\Gamma\vdash e:\bigwedge_{i\in I} \arrow {t_i}{s_i}$ using the rule \Rule{Abs+}, and with \Rule{Inter} and Thus, we can derive $\Gamma\vdash e:\bigwedge_{i\in I} \arrow {t_i}{s_i}$ using the rule \Rule{Abs+}, and with \Rule{Inter} and
\Rule{Abs-} we can derive $\Gamma\vdash e:t'$. We can conclude by applying \Rule{Subs}. \Rule{Abs-} we can derive $\Gamma\vdash e:t'$. We can conclude by applying \Rule{Subs}.
\item[$e=e_1 e_2$] The last rule is \Rule{App\Aa}. \item[$e=e_1 e_2$] The last rule is \Rule{App\Aats}.
We have $\apply {\ts_1} {\ts_2} \leq t$. Thus, let $t_1$ and $t_2$ such that $\ts_1 \leq t_1$, $\ts_2 \leq t_2$ and $\apply {t_1} {t_2} \leq t$. We have $\apply {\ts_1} {\ts_2} \leq t$. Thus, let $t_1$ and $t_2$ such that $\ts_1 \leq t_1$, $\ts_2 \leq t_2$ and $\apply {t_1} {t_2} \leq t$.
We know, according to the descriptive definition of $\apply {} {}$, that there exists $s\leq t$ such that $t_1 \leq \arrow {t_2} s$. We know, according to the descriptive definition of $\apply {} {}$, that there exists $s\leq t$ such that $t_1 \leq \arrow {t_2} s$.
...@@ -1124,15 +1124,15 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1124,15 +1124,15 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
$\Gamma\vdash e_1:\arrow {t_2} s$ using \Rule{Subs}, and together with $\Gamma\vdash e_2:t_2$ it gives $\Gamma\vdash e_1:\arrow {t_2} s$ using \Rule{Subs}, and together with $\Gamma\vdash e_2:t_2$ it gives
$\Gamma\vdash e_1\ e_2:s$ with \Rule{App}. We conclude with \Rule{Subs}. $\Gamma\vdash e_1\ e_2:s$ with \Rule{App}. We conclude with \Rule{Subs}.
\item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aa}. We have $\bpi_i \ts \leq t$. Thus, let $t'$ such that $\ts \leq t'$ and $\bpi_i t' \leq t$. \item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aats}. We have $\bpi_i \ts \leq t$. Thus, let $t'$ such that $\ts \leq t'$ and $\bpi_i t' \leq t$.
We know, according to the descriptive definition of $\bpi_i$, that there exists $t_i\leq t$ such that $t' \leq \pair \Any {t_i}$ (for $i=2$) or $t' \leq \pair {t_i} \Any$ (for $i=1$). We know, according to the descriptive definition of $\bpi_i$, that there exists $t_i\leq t$ such that $t' \leq \pair \Any {t_i}$ (for $i=2$) or $t' \leq \pair {t_i} \Any$ (for $i=1$).
By using the induction hypothesis, we have $\Gamma\vdash e':t'$, and thus we easily conclude using \Rule{Subs} and \Rule{Proj} By using the induction hypothesis, we have $\Gamma\vdash e':t'$, and thus we easily conclude using \Rule{Subs} and \Rule{Proj}
(for instance for the case $i=1$, we can derive $\Gamma\vdash e':\pair {t_i} \Any$ with \Rule{Subs} and then use \Rule{Proj}). (for instance for the case $i=1$, we can derive $\Gamma\vdash e':\pair {t_i} \Any$ with \Rule{Subs} and then use \Rule{Proj}).
\item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aa}. We conclude easily with the induction hypothesis and the rules \Rule{Subs} and \Rule{Pair}. \item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aats}. We conclude easily with the induction hypothesis and the rules \Rule{Subs} and \Rule{Pair}.
\item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aa}. We conclude easily with the induction hypothesis and the rules \item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aats}. We conclude easily with the induction hypothesis and the rules
\Rule{Subs} and \Rule{Case} (for the application of \Rule{Case}, $t'$ must be taken equal to $t_1 \vee t_2$ with $t_1$ and $t_2$ such that $\ts_1\leq t_1$, $\ts_2\leq t_2$ and $t_1 \vee t_2 \leq t$). \Rule{Subs} and \Rule{Case} (for the application of \Rule{Case}, $t'$ must be taken equal to $t_1 \vee t_2$ with $t_1$ and $t_2$ such that $\ts_1\leq t_1$, $\ts_2\leq t_2$ and $t_1 \vee t_2 \leq t$).
\end{description}\ \\ \end{description}\ \\
...@@ -1278,23 +1278,23 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1278,23 +1278,23 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
The property $\tsrep{\tyof e {\Gamma'}} \leq \tsrep{\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 operators on type schemes like $\tsand$ or $\apply {} {}$ are also monotone. 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}.) (Note that the only rule that introduces the type scheme constructor $\tsfun {\_}$ is \Rule{Abs\Aats}.)
If $\Gamma' = \bot$ we can conclude directly with the rule \Rule{Efq}. If $\Gamma' = \bot$ we can conclude directly with the rule \Rule{Efq\Aats}.
So let's assume $\Gamma' \neq \bot$ and $\Gamma \neq \bot$ So let's assume $\Gamma' \neq \bot$ and $\Gamma \neq \bot$
(as $\Gamma = \bot \Rightarrow \Gamma' = \bot$ by definition of $\leqA^e$). (as $\Gamma = \bot \Rightarrow \Gamma' = \bot$ by definition of $\leqA^e$).
If $e=x$ is a variable, then the last rule used in $\tyof e \Gamma$ and $\tyof e {\Gamma'}$ is \Rule{Var\Aa}. If $e=x$ is a variable, then the last rule used in $\tyof e \Gamma$ and $\tyof e {\Gamma'}$ is \Rule{Var\Aats}.
As $\Gamma' \leqA^e \Gamma$, we have $\Gamma'(e) \leq \Gamma(e)$ and thus As $\Gamma' \leqA^e \Gamma$, we have $\Gamma'(e) \leq \Gamma(e)$ and thus
we can conclude with the rule \Rule{Var\Aa}. we can conclude with the rule \Rule{Var\Aats}.
So let's assume that $e$ is not a variable. So let's assume that $e$ is not a variable.
If $e\in\dom\Gamma$, then the last rule used in $\tyof e \Gamma$ is \Rule{Env\Aa}. If $e\in\dom\Gamma$, then the last rule used in $\tyof e \Gamma$ is \Rule{Env\Aats}.
As $\Gamma' \leqA^e \Gamma$, we have $\tyof e {\Gamma'} \leq \Gamma(e)$. As $\Gamma' \leqA^e \Gamma$, we have $\tyof e {\Gamma'} \leq \Gamma(e)$.
Moreover, by applying the induction hypothesis, we get $\tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$ Moreover, by applying the induction hypothesis, we get $\tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$
(we can easily verify that $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\}$). (we can easily verify that $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\}$).
\begin{itemize} \begin{itemize}
\item If we have $e\in\dom{\Gamma'}$, we have according to the rule \Rule{Env\Aa} \item If we have $e\in\dom{\Gamma'}$, we have according to the rule \Rule{Env\Aats}
$\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$. $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$.
Together with $\tyof e {\Gamma'} \leq \Gamma(e)$, Together with $\tyof e {\Gamma'} \leq \Gamma(e)$,
...@@ -1303,7 +1303,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1303,7 +1303,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
$\tyof e {\Gamma'} = \tyof e {\Gamma'\setminus \{e\}} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}}=\tyof e {\Gamma}$. $\tyof e {\Gamma'} = \tyof e {\Gamma'\setminus \{e\}} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}}=\tyof e {\Gamma}$.
\end{itemize} \end{itemize}
If $e\not\in\dom\Gamma$ and $e\in\dom{\Gamma'}$, the last rule is \Rule{Env\Aa} for $\tyof e {\Gamma'}$. If $e\not\in\dom\Gamma$ and $e\in\dom{\Gamma'}$, the last rule is \Rule{Env\Aats} for $\tyof e {\Gamma'}$.
As $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\} = \Gamma$, As $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\} = \Gamma$,
we have $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma}$ by induction hypothesis. we have $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma}$ by induction hypothesis.
...@@ -1311,23 +1311,23 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1311,23 +1311,23 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
From now we know that the last rule in the derivation of $\tyof e {\Gamma}$ and $\tyof e {\Gamma'}$ (if any) is the same. From now we know that the last rule in the derivation of $\tyof e {\Gamma}$ and $\tyof e {\Gamma'}$ (if any) is the same.
\begin{description} \begin{description}
\item[$e=c$] The last rule is \Rule{Const\Aa}. It does not depend on $\Gamma$ so this case is trivial. \item[$e=c$] The last rule is \Rule{Const\Aats}. It does not depend on $\Gamma$ so this case is trivial.
\item[$e=x$] Already treated. \item[$e=x$] Already treated.
\item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$] \item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$]
The last rule is \Rule{Abs\Aa}. The last rule is \Rule{Abs\Aats}.
We have $\forall i\in I.\ \Gamma', (x:s_i) \leqA^{e'} \Gamma, (x:s_i)$ (quite straightforward) We have $\forall i\in I.\ \Gamma', (x:s_i) \leqA^{e'} \Gamma, (x:s_i)$ (quite straightforward)
so by applying the induction hypothesis we have $\forall i\in I.\ \tyof {e'} {\Gamma', (x:s_i)} \leq \tyof {e'} {\Gamma, (x:s_i)}$. so by applying the induction hypothesis we have $\forall i\in I.\ \tyof {e'} {\Gamma', (x:s_i)} \leq \tyof {e'} {\Gamma, (x:s_i)}$.
\item[$e=e_1 e_2$] The last rule is \Rule{App\Aa}. \item[$e=e_1 e_2$] The last rule is \Rule{App\Aats}.
We can conclude immediately by using the induction hypothesis and noticing that $\apply {} {}$ is monotonic for both of its arguments. We can conclude immediately by using the induction hypothesis and noticing that $\apply {} {}$ is monotonic for both of its arguments.
\item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aa}. \item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aats}.
We can conclude immediately by using the induction hypothesis and noticing that $\bpi_i$ is monotonic. We can conclude immediately by using the induction hypothesis and noticing that $\bpi_i$ is monotonic.
\item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aa}. \item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aats}.
We can conclude immediately by using the induction hypothesis. We can conclude immediately by using the induction hypothesis.
\item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aa}. \item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aats}.
By using the induction hypothesis we get $\Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma$. By using the induction hypothesis we get $\Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma$.
We also have $\Gamma' \leqA^{e_1} \Gamma$ (as $e_1$ is a subexpression of $e$). We also have $\Gamma' \leqA^{e_1} \Gamma$ (as $e_1$ is a subexpression of $e$).
...@@ -1428,10 +1428,10 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1428,10 +1428,10 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
Let's prove the first property. We have a positive derivation of $\Gamma \vdash e:t$. 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 $\Gamma = \bot$, we can conclude directly using \Rule{Efq\Aats}. 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}. 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. We can easily conclude just be using \Rule{Var\Aats}. Thus, let's suppose $e$ is not a variable.
If $e\in\dom\Gamma$, we can have the rule \Rule{Env} applied to $e$ in our derivation, but in this case If $e\in\dom\Gamma$, we can have the rule \Rule{Env} applied to $e$ in our derivation, but in this case
there can only be \Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation). there can only be \Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation).
...@@ -1440,7 +1440,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1440,7 +1440,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
in this case we can take $t'=\Any$ and use the fact that $\Gamma$ is well-formed). in this case we can take $t'=\Any$ and use the fact that $\Gamma$ is well-formed).
Hence, we can build a positive derivation for $\Gamma\setminus\{e\} \vdash e:t'$. Hence, we can build 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'$. 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}, Thus, by looking at the rule \Rule{Env\Aats},
we deduce $\tsrep{\tyof e \Gamma} \leq \Gamma(e) \land \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t$. 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$. It concludes this case, so let's assume $e\not\in\dom\Gamma$.
...@@ -1451,9 +1451,9 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1451,9 +1451,9 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\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$. \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$. Thus, we have $\tsrep{\tyof e \Gamma} \leq t_1 \land t_2$.
\item[\Rule{Subs}] Trivial using the induction hypothesis. \item[\Rule{Subs}] Trivial using the induction hypothesis.
\item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Const\Aa}. \item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Const\Aats}.
Thus this case is trivial. Thus this case is trivial.
\item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{App\Aa}. \item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{App\Aats}.
Let $\ts_1 = \tyof {e_1} \Gamma$ and $\ts_2 = \tyof {e_2} \Gamma$. 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$. 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 According to the descriptive definition of $\apply{}{}$, we have
...@@ -1461,14 +1461,14 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1461,14 +1461,14 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
As we also have $\tsrep{\apply {\ts_1} {\ts_2}} \leq \apply{\tsrep {\ts_1}}{\tsrep {\ts_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$. we can conclude that $\tyof e \Gamma \leq t_2=t$.
\item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aa}. \item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aats}.
This case is straightforward using the induction hypothesis. This case is straightforward using the induction hypothesis.
\item[\Rule{Abs-}] This case is impossible (the derivation is positive). \item[\Rule{Abs-}] This case is impossible (the derivation is positive).
\item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Case\Aa}. \item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Case\Aats}.
By using the induction hypothesis and the monotonicity lemma, we get $\tsrep{\ts_1}\leq t$ and $\tsrep{\ts_2}\leq t$. 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$. 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{Proj}] Quite similar to the case \Rule{App}.
\item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Pair\Aa}. \item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Pair\Aats}.
We just use the induction hypothesis and the fact that $\tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}$. We just use the induction hypothesis and the fact that $\tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}$.
\end{description} \end{description}
...@@ -1582,7 +1582,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1582,7 +1582,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
By case analysis: neither \Rule{Efq}, \Rule{Env\Aa} nor \Rule{App\Aa} can produce a type By case analysis: neither \Rule{Efq\Aats}, \Rule{Env\Aats} nor \Rule{App\Aats} can produce a type
containing a constructor $\tsfun \cdots$. containing a constructor $\tsfun \cdots$.
\end{proof} \end{proof}
...@@ -1598,7 +1598,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1598,7 +1598,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{theorem} \end{theorem}
\begin{proof} \begin{proof}
This proof is quite similar to that of the completeness for positive derivations. This proof is done by induction. It is quite similar to that of the completeness for positive derivations.
In consequence, we will only detail cases that are quite different from those of the previous proof. In consequence, we will only detail cases that are quite different from those of the previous proof.
Let's begin with the first property. We have a rank-0 negated derivation of $\Gamma \vdash e:t$. Let's begin with the first property. We have a rank-0 negated derivation of $\Gamma \vdash e:t$.
...@@ -1614,7 +1614,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1614,7 +1614,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
Now we analyze the last rule of the derivation (only the cases that are not similar are shown): Now we analyze the last rule of the derivation (only the cases that are not similar are shown):
\begin{description} \begin{description}
\item[\Rule{Abs-}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aa}. \item[\Rule{Abs-}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aats}.
Moreover, by using the induction hypothesis on the premise, we know that $\tyof e \Gamma \neq \tsempty$. Moreover, by using the induction hypothesis on the premise, we know that $\tyof e \Gamma \neq \tsempty$.
Thus we have $\tyof e \Gamma \leq \neg (\arrow {t_1} {t_2}) = t$ (because every type $\neg (\arrow {s'} {t'})$ Thus we have $\tyof e \Gamma \leq \neg (\arrow {t_1} {t_2}) = t$ (because every type $\neg (\arrow {s'} {t'})$
such that $\neg (\arrow {s'} {t'}) \land \bigwedge_{i\in I} \arrow {s_i} {t_i} \neq \Empty$ is in $\tsint{\tsfun{\arrow {s_i} {t_i}}}$). such that $\neg (\arrow {s'} {t'}) \land \bigwedge_{i\in I} \arrow {s_i} {t_i} \neq \Empty$ is in $\tsint{\tsfun{\arrow {s_i} {t_i}}}$).
...@@ -1751,7 +1751,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1751,7 +1751,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
of the type of $e_1$). of the type of $e_1$).
\item Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type \item Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type
cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part
(it makes no difference relatively to the rule \Rule{Efq}). (it makes no difference relatively to the rule \Rule{Efq\Aats}).
\end{itemize} \end{itemize}
\end{proof} \end{proof}
......
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