[Prev][Next][Index][Thread]
Minimal Typings in Atomic Subtyping

To: types@dcs.gla.ac.uk

Subject: Minimal Typings in Atomic Subtyping

From: Jakob Rehof <rehof@diku.dk>

Date: Thu, 8 Aug 1996 14:34:13 +0200

Approved: types@dcs.gla.ac.uk
[ The Types Forum  http://www.dcs.gla.ac.uk/~types ]
This is to inform the Types Forum that I have written a
technical report "Minimal Typings in Atomic Subtyping",
which is available from my homepage (and by ftp from DIKU.)
We prove that systems of atomic subtyping have
logically most succinct typings, and we use this result to
prove an exponential lower bound on the dagsize of coercion
sets as well as of types in most general typings, relative to
the notion of "lazy instance" defined by Fuh and Mishra.
The report can be obtained from
http://www.diku.dk/researchgroups/topps/
personal/rehof/publications.html
and also by ftp
<ftp://ftp.diku.dk/diku/semantics/papers/D278.ps.gz>
A summary of the report has been submitted for publication.
The abstract follows:

We study the problem of simplifying typings
and the sizecomplexity of most general typings in
typed programming languages with subtyping. We define a notion
of minimal typings relating all typings which are
equivalent with respect to instantiation.
The notion of instance is that of Fuh and Mishra
\cite{fumi89}, which supports many interesting
simplifications.
We prove that every typable term has a unique
minimal typing, which is the logically most succinct
among all equivalent typings.
The notion of minimality is purely logical, defined
independently of any particular type
simplification technique. We study
completeness properties, with respect to our
notion of minimality, of wellknown simplification
techniques. Drawing upon these results, we prove a tight
exponential lower bound for the
worst case dagsize of coercion sets as well as
of types in most general typings. To the best of
our knowledge, the best previously proven
lower bound was linear.


Jakob Rehof, DIKU, Department of Computer Science,
University of Copenhagen, Universitetsparken 1,
DK2100 Copenhagen East, Denmark.
Telephone: +45 35 32 14 08
Email : rehof@diku.dk
