Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complete and tractable machine-independent characterizations of second-order polytime

Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, Romain Péchoux

TL;DR

This work addresses the problem of machine-independent, tractable characterization of the second-order polynomial-time class ${\tt BFF}$. It develops a higher-order programming language with a two-layer type system that enforces safe/terminating behavior, and proves that typable and terminating programs characterize ${\tt BFF}$, even without lambda-abstraction. A rank-based variant (rank-0) shows lambda-abstraction is not essential for completeness, and type inference is shown to be polynomial-time in the safe settings. To ensure practical feasibility, the authors introduce ${\rm SCP}_{\rm S}$, a termination criterion computable in quadratic time that preserves completeness, yielding a tractable, complete, and implicit characterization of ${\tt BFF}$ via ${\rm SCP}_{\rm S} \cap SAFE$. The results notably advance automation in verifying second-order time bounds and open pathways for extensions to broader SCT-inspired techniques or purely functional formulations.

Abstract

The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.

Complete and tractable machine-independent characterizations of second-order polytime

TL;DR

This work addresses the problem of machine-independent, tractable characterization of the second-order polynomial-time class . It develops a higher-order programming language with a two-layer type system that enforces safe/terminating behavior, and proves that typable and terminating programs characterize , even without lambda-abstraction. A rank-based variant (rank-0) shows lambda-abstraction is not essential for completeness, and type inference is shown to be polynomial-time in the safe settings. To ensure practical feasibility, the authors introduce , a termination criterion computable in quadratic time that preserves completeness, yielding a tractable, complete, and implicit characterization of via . The results notably advance automation in verifying second-order time bounds and open pathways for extensions to broader SCT-inspired techniques or purely functional formulations.

Abstract

The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.
Paper Structure (22 sections, 15 theorems, 25 equations, 6 figures)

This paper contains 22 sections, 15 theorems, 25 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Motivations
  3. Contributions
  4. Related work
  5. Leading example
  6. A second-order language with imperative procedures
  7. Syntax
  8. Operational semantics
  9. Type system
  10. Tiers and typing environments
  11. Typing judgments and type system
  12. Safe programs
  13. Intuitions
  14. Characterizations of the class of Basic Feasible Functionals
  15. Safe and terminating programs
  16. ...and 7 more sections

Key Result

Lemma 4.1

For any two classes of functionals $\mathcal{X},\mathcal{Y}$, if $\mathcal{X}\subseteq \mathcal{Y}$ then $\lambda(\mathcal{X})_2 \subseteq \lambda(\mathcal{Y})_2$.

Figures (6)

  • Figure 1: Program ce
  • Figure 2: Syntax of type-2 programs
  • Figure 3: Big step operational semantics
  • Figure 4: Tier-based type system
  • Figure :
  • ...and 1 more figures

Theorems & Definitions (43)

  • Definition 1.1: KC91
  • Definition 2.1: Neutral and positive operators
  • Example 2.2
  • Definition 3.1: Safe operator typing environment
  • Example 3.2
  • Example 3.3
  • Lemma 4.1
  • Definition 4.2: Safe and terminating procedures
  • Theorem 4.3: HKMP20
  • Lemma 4.4
  • ...and 33 more