
TL;DR
This paper introduces ATR, a formal system characterizing polynomial-time and type-2 feasible functionals through a complexity-aware type system and semantics, connecting programming formalism with complexity theory.
Contribution
It develops a new formalism, ATR, with a dual restriction type system and semantics that precisely characterize polynomial-time and feasible functionals, advancing the understanding of complexity in higher-order programming.
Findings
ATR's first-order programs characterize polynomial-time functions.
Second-order programs in ATR characterize type-2 basic feasible functionals.
A sound time-complexity semantics for ATR is constructed, linking recursion to polynomial bounds.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
