-
General Ramified Recurrence and Polynomial-time Completeness
Authors:
Norman Danner,
James S. Royer
Abstract:
We exhibit a sound and complete implicit-complexity formalism for functions feasibly computable by structural recursions over inductively defined data structures. Feasibly computable here means that the structural-recursive definition runs in time polynomial in the size of the representation of the inputs where these representations may make use of data sharing. Inductively defined data structures…
▽ More
We exhibit a sound and complete implicit-complexity formalism for functions feasibly computable by structural recursions over inductively defined data structures. Feasibly computable here means that the structural-recursive definition runs in time polynomial in the size of the representation of the inputs where these representations may make use of data sharing. Inductively defined data structures here includes lists and trees. Soundness here means that the programs within the implicit-complexity formalism have feasible run times. Completeness here means that each function computed by a feasible structural recursion has a program in the implicit-complexity formalism. This paper is a follow up on the work of Avanzini, Dal Lago, Martini, and Zorzi who focused on the soundness of such formalisms but did not consider the question of completeness.
△ Less
Submitted 20 May, 2022;
originally announced May 2022.
-
A static cost analysis for a higher-order language
Authors:
N. Danner,
J. Paykin,
J. S. Royer
Abstract:
We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression.…
▽ More
We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression. A translation function tr maps target expressions to complexities. Our main result is the following Soundness Theorem: If t is a term in the target language, then the cost component of tr(t) is an upper bound on the cost of evaluating t. The proof of the Soundness Theorem is formalized in Coq, providing certified upper bounds on the cost of any expression in the target language.
△ Less
Submitted 19 December, 2012; v1 submitted 15 June, 2012;
originally announced June 2012.
-
Ramified Structural Recursion and Corecursion
Authors:
Norman Danner,
James S. Royer
Abstract:
We investigate feasible computation over a fairly general notion of data and codata. Specifically, we present a direct Bellantoni-Cook-style normal/safe typed programming formalism, RS1, that expresses feasible structural recursions and corecursions over data and codata specified by polynomial functors. (Lists, streams, finite trees, infinite trees, etc. are all directly definable.) A novel aspect…
▽ More
We investigate feasible computation over a fairly general notion of data and codata. Specifically, we present a direct Bellantoni-Cook-style normal/safe typed programming formalism, RS1, that expresses feasible structural recursions and corecursions over data and codata specified by polynomial functors. (Lists, streams, finite trees, infinite trees, etc. are all directly definable.) A novel aspect of RS1 is that it embraces structure-sharing as in standard functional-programming implementations. As our data representations use sharing, our implementation of structural recursions are memoized to avoid the possibly exponentially-many repeated subcomputations a naive implementation might perform. We introduce notions of size for representations of data (accounting for sharing) and codata (using ideas from type-2 computational complexity) and establish that type-level 1 RS1-functions have polynomial-bounded runtimes and satisfy a polynomial-time completeness condition. Also, restricting RS1 terms to particular types produces characterizations of some standard complexity classes (e.g., omega-regular languages, linear-space functions) and some less-standard classes (e.g., log-space streams).
△ Less
Submitted 27 January, 2012; v1 submitted 22 January, 2012;
originally announced January 2012.
-
Axiomatizing Resource Bounds for Measure
Authors:
Xiaoyang Gu,
Jack H. Lutz,
Satyadev Nandakumar,
James S. Royer
Abstract:
Resource-bounded measure is a generalization of classical Lebesgue measure that is useful in computational complexity. The central parameter of resource-bounded measure is the {\it resource bound} $Δ$, which is a class of functions. When $Δ$ is unrestricted, i.e., contains all functions with the specified domains and codomains, resource-bounded measure coincides with classical Lebesgue measure. On…
▽ More
Resource-bounded measure is a generalization of classical Lebesgue measure that is useful in computational complexity. The central parameter of resource-bounded measure is the {\it resource bound} $Δ$, which is a class of functions. When $Δ$ is unrestricted, i.e., contains all functions with the specified domains and codomains, resource-bounded measure coincides with classical Lebesgue measure. On the other hand, when $Δ$ contains functions satisfying some complexity constraint, resource-bounded measure imposes internal measure structure on a corresponding complexity class.
Most applications of resource-bounded measure use only the "measure-zero/measure-one fragment" of the theory. For this fragment, $Δ$ can be taken to be a class of type-one functions (e.g., from strings to rationals). However, in the full theory of resource-bounded measurability and measure, the resource bound $Δ$ also contains type-two functionals. To date, both the full theory and its zero-one fragment have been developed in terms of a list of example resource bounds chosen for their apparent utility.
This paper replaces this list-of-examples approach with a careful investigation of the conditions that suffice for a class $Δ$ to be a resource bound. Our main theorem says that every class $Δ$ that has the closure properties of Mehlhorn's basic feasible functionals is a resource bound for measure.
We also prove that the type-2 versions of the time and space hierarchies that have been extensively used in resource-bounded measure have these closure properties. In the course of doing this, we prove theorems establishing that these time and space resource bounds are all robust.
△ Less
Submitted 31 January, 2012; v1 submitted 10 February, 2011;
originally announced February 2011.
-
Two algorithms in search of a type system
Authors:
Norman Danner,
James S. Royer
Abstract:
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursi…
▽ More
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper's main work is in refining the original time-complexity semantics for ATR to show that these new recursion schemes do not lead out of the realm of feasibility.
△ Less
Submitted 18 April, 2008; v1 submitted 3 October, 2007;
originally announced October 2007.
-
Time-complexity semantics for feasible affine recursions (extended abstract)
Authors:
Norman Danner,
James S. Royer
Abstract:
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursi…
▽ More
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper's main work is in extending and simplifying the original time-complexity semantics for ATR to develop a set of tools for extracting and solving the higher-type recurrences arising from feasible affine recursions.
△ Less
Submitted 20 March, 2007; v1 submitted 11 January, 2007;
originally announced January 2007.
-
Adventures in time and space
Authors:
Norman Danner,
James S. Royer
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 l…
▽ More
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.
△ Less
Submitted 12 March, 2007; v1 submitted 21 December, 2006;
originally announced December 2006.
