Commit 0a76220e authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rank-0

parent 5bc363b0
......@@ -855,25 +855,24 @@ The algorithmic system above is sound with respect to the deductive one of Secti
\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
We were not able to prove full 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
definition of \constrf{} (case~\eqref{due} is the critical
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
left-hand side of negated arrows.
\begin{definition}[Rank-0 negation]
A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if \Rule{Abs--} never occurs in the derivation of a left premise 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.
left-hand side of another negated arrow.
\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$.
For every $\Gamma$, $e$, $t$, if $\Gamma \vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that ${\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
to stress that this systems is defined only to study the declarative
......@@ -883,6 +882,6 @@ practical application type schemes are not needed, since they are
necessary only when type cases may specify types with negative arrows
and this in practice never happens: see Footnote
\ref{foo:typecase}. This is why for our implementation we use the
CDuce library in which type schemes are absent and functiond are typed
CDuce library in which type schemes are absent and functions are typed
only by intersections of positive arrows. We present the implementation in Section~\ref{sec:practical}
but before let us study some extensions.
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