| |
VOLUME 3, ISSUE 1, PAPER 9
|
Adventures in time and space
|
©Norman Danner, Dept. of Mathematics and Computer Science; Wesleyan University
©James S. Royer, Dept. of Elec. Engrg. and Computer Science; Syracuse University
|
Abstract
This paper investigates what is essentially a call-by-value version of PCF
under a complexity-theoretically motivated type system. The programming
formalism, ATR, has its first-order programs characterize the polynomial-time
computable functions, and its second-order programs characterize the type-2
basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR-types
are confined to levels 0, 1, and 2.) The type system comes in two parts, one
that primarily restricts the sizes of values of expressions and a second that
primarily restricts the time required to evaluate expressions. The
size-restricted part is motivated by Bellantoni and Cook's and Leivant's
implicit characterizations of polynomial-time. The time-restricting part is an
affine version of Barber and Plotkin's DILL. Two semantics are constructed for
ATR. The first is a pruning of the naive denotational semantics for ATR. This
pruning removes certain functions that cause otherwise feasible forms of
recursion to go wrong. The second semantics is a model for ATR's time
complexity relative to a certain abstract machine. This model provides a
setting for complexity recurrences arising from ATR recursions, the solutions
of which yield second-order polynomial time bounds. The time-complexity
semantics is also shown to be sound relative to the costs of interpretation on
the abstract machine.
|
Publication date: March 12, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(1:9)2007
Hit Counts: 3840 |
 Creative Commons | |
