@@ -851,9 +851,28 @@ an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is a why the algorithm reintroduces the classic rules
for variables.
The system above satisfies the following properties:\beppe{State here
soundness and partial completeness}
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $t$, $n_o$, if $\tyof e \Gamma\leq t$, then $\Gamma\vdash e:t$.
\end{theorem}
We were not able to prove completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
rule \Rule{Path} and $(ii)$ the use of nested \Rule{PAppL} that yield
a precision that the algorithm loses by applying \tsrep{} in the
definition of \constrf{} (case~\eqref{due} is the crical
one). Completeness is recovered by $(i)$ limiting the depth of the
derivations and $(ii)$ forbidding nested negated arrows on the
lefthand side of negated arrows.
\begin{definition}[Rank-1 negation]
A derivation of $\Gamma\vdash e:t$ is \emph{Rank-1 negated} if \Rule{Abs--} never occurs in the derivation of a left premises of a \Rule{PAppL} rule
\end{definition}
The use of this terminology is borrowed from the ranking of higher-order
types, since, intuitively, it corresponds to typing a language in
which in the types used in dynamic tests, a negated arrow never occurs on the
lefthand side of another negated arrows.
\begin{theorem}[Partial Completeness]
For every $\Gamma$, $e$, $t$, if $\Gamma\vdash e:t$ is derivable by a Rank-1 negated derivation, then there exists $n_o$ such that $\tsrep{\tyof e \Gamma}\leq t$.
\end{theorem}
The use of type schemes and the possible non convergence of iterations
yield a system that may seem overly complicated. But it is important
For any $\Gamma$, $e$, $t$ such that$\tyof e \Gamma\leq t$ (for any $n_o$), we can derive $\Gamma\vdash e:t$.
For every $\Gamma$, $e$, $t$, $n_o$, if$\tyof e \Gamma\leq t$, then we can derive $\Gamma\vdash e:t$.
More precisely:
\begin{align*}
...
...
@@ -1444,4 +1444,4 @@
&\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)}
