Commit 31db3325 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

update completeness theorem in the proofs

parent 6237061c
...@@ -954,8 +954,8 @@ can be extended to type schemes (see also~\citep[\S4.4]{Cas15} for a detailed de ...@@ -954,8 +954,8 @@ can be extended to type schemes (see also~\citep[\S4.4]{Cas15} for a detailed de
We present here a refinement of the algorithmic type system presented in \ref{sec:algorules} We present here a refinement of the algorithmic type system presented in \ref{sec:algorules}
that associates to an expression a type scheme instead of a regular type. that associates to an expression a type scheme instead of a regular type.
This allows to type expressions more precisely and thus to have a more powerful completeness theorem in regards to the This allows to type expressions more precisely and thus to have a more powerful
declarative type system. (but still partial) completeness theorem in regards to the declarative type system.
The results about this new type system will be used in \ref{sec:proofs_algorithmic_without_ts} in order to obtain a soundness and completeness The results about this new type system will be used in \ref{sec:proofs_algorithmic_without_ts} in order to obtain a soundness and completeness
theorem for the algorithmic type system presented in \ref{sec:algorules}. theorem for the algorithmic type system presented in \ref{sec:algorules}.
...@@ -1756,11 +1756,9 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1756,11 +1756,9 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{proof} \end{proof}
\begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA} \begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA}
If we restrict the language to positive expressions $e_+$, For every type environment $\Gamma$ and positive expression $e_+$, if
the algorithmic type system without type schemes is complete. $\Gamma\vdash e_+: t$, then there exist $n_o$ and $t'$ such that $\Gamma\vdashA
e_+: t'$.
More precisely:
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \exists t'.\ \Gamma \vdashA e_+ : t'$
\end{theorem} \end{theorem}
\begin{proof} \begin{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