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

proofs for the system without type schemes

parent d81024c4
......@@ -1407,7 +1407,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}.
\end{definition}
\begin{theorem}[Completeness for positive derivations]
\begin{theorem}[Completeness for positive derivations]\label{completenessAtsPositive}
For every $\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$.
......@@ -1710,7 +1710,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{theorem}
\begin{proof}
Trivial by using the previous lemma and the theorem \ref{soundnessAts}.
Trivial by using the theorem \ref{soundnessAts} and the previous lemma.
\end{proof}
\subsubsection{Completeness}
......@@ -1723,6 +1723,32 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+}
\end{array}
\]
\begin{lemma}
If we restrict the language to positive expressions $e_+$,
then we have the following property:
$\forall \Gamma, e_+, \ts.\ \Gamma \vdashAts e_+:\ts \Rightarrow \Gamma \vdashA e_+:\tsrep{\ts}$
\end{lemma}
\begin{proof}
We can prove it by induction over the structure of $e_+$.
The main idea of this proof is that, as $e_+$ is a positive expression, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) become useless:
\begin{itemize}
\item When typing an application $e_1 e_2$, the negative part of the type of $e_1$
is ignored by the operator $\apply {} {}$.
\item Moreover, as there is no negated arrows in the domain of lambda-abstractions,
the negative arrows of the type of $e_2$ can also be ignored.
\item Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
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}).
\end{itemize}
\end{proof}
\begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA}
If we restrict the language to positive expressions $e_+$,
......@@ -1732,21 +1758,6 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \exists t'.\ \Gamma \vdashA e_+ : t'$
\end{theorem}
\begin{proof} TODO: ADAPT IT. INDUCTION HYPOTHESIS MUST BE STRONGER.
With such restrictions, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) is useless.
Indeed, when typing an application $e_1 e_2$, the negative part of the type of $e_1$
is ignored by the operator $\apply {} {}$.
Moreover, as there is no negated arrows in the domain of lambda-abstractions,
the negative arrows of the type of $e_2$ can also be ignored.
Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
of the type of $e_1$).
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}).
\begin{proof}
Trivial by using the theorem \ref{completenessAtsPositive} and the previous lemma.
\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