M. Dezani-Ciancaglini, F. Honsell, and F. Alessi
A complete characterization of
complete intersection-type preorders
ACM Transactions on Logic and Computation, 4(1):120-147,
January 2003
We characterize those ``type preorders'' which yield
complete ``intersection-type assignment systems'' for
lambda calculi, with respect to the three canonical set-theoretical
semantics for intersection-types: the inference semantics, the simple
semantics and the F-semantics. These semantics arise
by taking as interpretation of types subsets of applicative structures, as
interpretation of the ``preorder relation'', set-theoretic inclusion, as
interpretation of the ``intersection constructor,
set-theoretic intersection, and by taking the interpretation
of the ``arrow constructor'', a la Scott, with
respect to either ``any possible functionality set'', or the ``largest'' one, or
the ``least'' one.
These results strengthen and generalize significantly all earlier
results in the literature, to our knowledge, in at least three
respects. First of all the inference semantics had not been
considered before. Secondly, the characterizations are all given just
in terms of simple closure conditions on the ``preorder relation''
on the types, rather than on the typing judgments
themselves. The task of checking the condition is made therefore
considerably more tractable. Lastly, we do not restrict attention just
to lambda models, but to arbitrary applicative structures which
admit an interpretation function. Thus we allow also for the treatment of
models of
restricted lambda calculi. Nevertheless the characterizations we give
can
be tailored just to the case of lambda models.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43