Adventures in time and space

Norman Danner, James S. Royer

Research output: Contribution to journalArticle

3 Scopus citations

Abstract

This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR1, has its first-order programs characterize the poly-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATRi-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 poly-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR 1. The first is a pruning of the naïve denotational semantics for ATR1. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR1 's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR1 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.

Original languageEnglish (US)
Pages (from-to)168-179
Number of pages12
JournalACM SIGPLAN Notices
Volume41
Issue number1
DOIs
StatePublished - Jun 26 2006

Keywords

  • Languages
  • Performance
  • Theory

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Adventures in time and space'. Together they form a unique fingerprint.

  • Cite this