Commit 6558959c authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 456def46 ca84a67b
......@@ -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}.
\begin{mathpar}
\Infer[Efq\Aa]
\Infer[Efq\Aats]
{ }
{ \Gamma, (e:\Empty) \vdashAts e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\qquad
\Infer[Var\Aa]
\Infer[Var\Aats]
{ }
{ \Gamma \vdashAts x: \Gamma(x) }
{ x\in\dom\Gamma}
\\
\Infer[Env\Aa]
\Infer[Env\Aats]
{ \Gamma\setminus\{e\} \vdashAts e : \ts }
{ \Gamma \vdashAts e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma \text{ and } e \text{ not a variable}}
\qquad
\Infer[Const\Aa]
\Infer[Const\Aats]
{ }
{\Gamma\vdashAts c:\basic{c}}
{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\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}
\\
\Infer[App\Aa]
\Infer[App\Aats]
{
\Gamma \vdashAts e_1: \ts_1\\
\Gamma \vdashAts e_2: \ts_2\\
......@@ -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 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[Case\Aa]
\Infer[Case\Aats]
{\Gamma\vdashAts e:\ts_0\\
\Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashAts e_2 : \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}
\\
\Infer[Proj\Aa]
\Infer[Proj\Aats]
{\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\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,e_2):{\ts_1}\tstimes{\ts_2}}
{(e_1,e_2)\not\in\dom\Gamma}
......@@ -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}.
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}.
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$.
The induction hypothesis gives $\Gamma\setminus\{e\} \vdash e:t'$
(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}.
Now, let's suppose that $e\not\in\dom\Gamma$.
\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=\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$.
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$.
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}.
\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 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}.
$\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}.
\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$).
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}).
\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$).
\end{description}\ \\
......@@ -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}}$
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$
(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
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.
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)$.
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\}$).
\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\}}$.
Together with $\tyof e {\Gamma'} \leq \Gamma(e)$,
......@@ -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}$.
\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$,
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}.
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}
\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=\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)
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.
\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.
\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.
\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$.
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}.
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}.
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
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}.
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'$.
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$.
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}.
\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$ (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.
\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$.
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
......@@ -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}}$,
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.
\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$.
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$ (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}}$.
\end{description}
......@@ -1582,7 +1582,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{lemma}
\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$.
\end{proof}
......@@ -1598,7 +1598,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{theorem}
\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.
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}.
Now we analyze the last rule of the derivation (only the cases that are not similar are shown):
\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$.
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}}}$).
......@@ -1751,7 +1751,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
of the type of $e_1$).
\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
(it makes no difference relatively to the rule \Rule{Efq}).
(it makes no difference relatively to the rule \Rule{Efq\Aats}).
\end{itemize}
\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