[Prev][Next][Index][Thread]

Minimal Typings in Atomic Subtyping


[------ 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 dag-size 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/research-groups/topps/
                  personal/rehof/publications.html
and also by ftp 
 <ftp://ftp.diku.dk/diku/semantics/papers/D-278.ps.gz>

A summary of the report has been submitted for publication.

The abstract follows:

----------------------------------------------------------
We study the problem of simplifying typings 
and the size-complexity 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 well-known simplification 
techniques. Drawing upon these results, we prove a tight
exponential lower bound for the 
worst case dag-size 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, 
DK-2100 Copenhagen East, Denmark.
Telephone: +45 35 32 14 08
E-mail   : rehof@diku.dk 
-----------------------------------------------------------------------------