|
Cost Recurrences for DML Programs
Bernd Grobauer June 2001 |
Abstract:
A cost recurrence describes an upper bound for the running time
of a program in terms of the size of its input. Finding cost recurrences is a
frequent intermediate step in complexity analysis, and this step requires an
abstraction from data to data size. In this article, we use information
contained in dependent types to achieve such an abstraction: Dependent ML
(DML), a conservative extension of ML, provides dependent types that can be
used to associate data with size information, thus describing a possible
abstraction. We systematically extract cost recurrences from first-order DML
programs, guiding the abstraction from data to data size with information
contained in DML type derivations
Available as PostScript, PDF, DVI. |