Norman Danner ; James S. Royer - Adventures in time and space

lmcs:2231 - Logical Methods in Computer Science, March 12, 2007, Volume 3, Issue 1 - https://doi.org/10.2168/LMCS-3(1:9)2007
Adventures in time and spaceArticle

Authors: Norman Danner ; James S. Royer

    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.


    Volume: Volume 3, Issue 1
    Published on: March 12, 2007
    Submitted on: August 7, 2006
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.3,F.1.3,F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Computation and Complexity at Higher-Types; Funder: National Science Foundation; Code: 0098198

    3 Documents citing this article

    Consultation statistics

    This page has been seen 957 times.
    This article's PDF has been downloaded 265 times.