Commit 8e45f539 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

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

parents 039367e0 e1b28f98
......@@ -232,7 +232,6 @@
\label{sec:conclusion}
\input{conclusion}
%% Acknowledgments
\begin{acks} %% acks environment is optional
%% contents suppressed with 'anonymous'
......@@ -248,6 +247,10 @@
conclusions or recommendations expressed in this material are those
of the author and do not necessarily reflect the views of the
National Science Foundation.
This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045-
DIGICOSME) operated by ANR as part of the program «Investissement d'Avenir» Idex
Paris-Saclay (ANR-11-IDEX-0003-02).
\end{acks}
......
......@@ -774,7 +774,7 @@
\begin{lemma}[$\worra {} {}$ alternative definition]
The following algorithmic definition for $\worra {} {}$ is equivalent to the previous one:
\[\forall t, s.\ \worra t s = \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left(
\[\forall t, s.\ \worra t s \simeq \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left(
\dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\]
\end{lemma}
......@@ -1118,7 +1118,6 @@
\qed
\subsubsection{Some definitions}
\begin{definition}[Bottom environment]
......@@ -1144,8 +1143,24 @@
Let $\ts_1$ and $\ts_2$ two type schemes. We write $\ts_2 \leq \ts_1$ iff $\tsint {\ts_1} \subseteq \tsint{\ts_2}$.
\end{definition}
\begin{definition}[Positive derivation]
A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}.
\end{definition}
\begin{definition}[Acceptable derivation]
A derivation of the declarative type system is said acceptable iff any application of \Rule{PAppL}
has a positive derivation as first premise ($\pvdash \Gamma e t \varpi.1:t_1$).
\end{definition}
\subsubsection{Major lemmas and completeness}
\begin{lemma}
Let $t$ a type and $\ts$ a type scheme.
We have $\tsrep{t\tsand\ts} \leq \tsrep{t} \land \tsrep{\ts}$.
\end{lemma}
Proof: straightfoward, by induction on the structure of $\ts$.
\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:
\begin{align*}
&\tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}\\
......@@ -1161,7 +1176,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 noticing that $\tsrep {t \tsand \ts} \leq t \land \tsrep {\ts}$,
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}}$.
(Note that the only rule that introduces the type scheme constructor $\tsfun {\_}$ is \Rule{Abs\Aa}.)
......@@ -1282,14 +1297,38 @@
\qed
\begin{theorem}[Completeness of the algorithm]
For any $\Gamma$, $e$, $t$ such that we can derive $\Gamma \vdash e:t$, there exists a global parameter $n_o$
\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$,
there exists a global parameter $n_o$ with which $\tsrep{\tyof e \Gamma} \leq t$.
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, \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}
Proof:
We proceed by induction on the declarative derivation.
\begin{description}
\item[\Rule{Env}] Trivial.
\item[\Rule{Inter}] TODO%By using the induction hypothesis we get $\tsrep{\tyof e \Gamma}$
\end{description}
\qed
\begin{theorem}[Completeness of the algorithm for acceptable derivations]
For any $\Gamma$, $e$, $t$ such that we have an acceptable derivation of $\Gamma \vdash e:t$, there exists a global parameter $n_o$
with which $\tyof e \Gamma \leq t$.
More precisely:
\begin{align*}
&\forall \Gamma, e, t.\ \Gamma \vdash e:t \Rightarrow \tyof e \Gamma \leq t \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, e, t, t', \varpi.\ \pvdash \Gamma e t \varpi:t' \Rightarrow \env {\Gamma,e,t} (\varpi) \leq t' \text{ (for $n_o$ large enough)}\\
&\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \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 \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, \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