TY - JOUR
T1 - Adventures in time and space
AU - Danner, Norman
AU - Royer, James S.
N1 - Funding Information:
Acknowledgments. Thanks to Susan Older and Bruce Kapron for repeatedly listening to the second author describe this work along its evolution. Thanks to Neil Jones and Luke Ong for inviting the second author to Oxford for a visit and for some extremely helpful comments on an early draft of this paper. Thanks to Syracuse University for hosting the first author during September 2005. Thanks also to the anonymous referees of both the POPL version of this paper [DR06] and the present paper for many extremely helpful comments. Finally many thanks to Peter O’Hearn, Josh Berdine, and the Queen Mary theory group for hosting the second author’s visit in the Autumn of 2005 and for repeatedly raking his poor type-systems over the coals until something reasonably simple and civilized survived the ordeals. This work was partially supported by EPSRC grant GR/T25156/01 and NSF grant CCR-0098198.
Publisher Copyright:
© N. Danner and J. S. Royer.
PY - 2007/3/13
Y1 - 2007/3/13
N2 - 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 na¨ıve 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.
AB - 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 na¨ıve 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.
KW - Basic feasible functional
KW - Compositional semantics
KW - Higher-type computation
KW - Implicit computational complexity
KW - Type systems
UR - http://www.scopus.com/inward/record.url?scp=70349558988&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349558988&partnerID=8YFLogxK
U2 - 10.2168/LMCS-3(1:9)2007
DO - 10.2168/LMCS-3(1:9)2007
M3 - Article
AN - SCOPUS:70349558988
SN - 1860-5974
VL - 3
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 1
M1 - 9
ER -