Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale

TL;DR

The paper characterizes the type-2 basic feasible functionals ${\mathtt{BFF}_{2}}$ via higher-order rewriting by introducing cost--size interpretations for simply-typed TRSs and proving a key Innermost Compatibility Theorem. It establishes soundness by showing STRSs with polynomially bounded cost--size interpretations compute only ${\mathtt{BFF}_{2}}$ functionals, and completeness by encoding polynomial-time Oracle Turing Machines into STRSs that admit such interpretations. The work leverages term graphs to bound size growth and implements a robust oracle-simulation framework, yielding a rewriting-based characterization with potential tooling implications. This provides a foundational bridge between implicit complexity and higher-order rewriting, enabling effective analysis of type-2 feasibility through rewriting techniques.

Abstract

The class of type-two basic feasible functionals ($\mathtt{BFF}_2$) is the analogue of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}_2$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing $\mathtt{BFF}_2$ by higher-order term rewriting. Various kinds of interpretations for first-order term rewriting have been introduced in the literature for proving termination and characterizing first-order complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see second order rewriting as ways of computing type-2 functionals. We then prove that the class of functionals represented by higher-order terms admitting polynomially bounded cost-size interpretations exactly corresponds to $\mathtt{BFF}_2$.

A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

TL;DR

The paper characterizes the type-2 basic feasible functionals via higher-order rewriting by introducing cost--size interpretations for simply-typed TRSs and proving a key Innermost Compatibility Theorem. It establishes soundness by showing STRSs with polynomially bounded cost--size interpretations compute only functionals, and completeness by encoding polynomial-time Oracle Turing Machines into STRSs that admit such interpretations. The work leverages term graphs to bound size growth and implements a robust oracle-simulation framework, yielding a rewriting-based characterization with potential tooling implications. This provides a foundational bridge between implicit complexity and higher-order rewriting, enabling effective analysis of type-2 feasibility through rewriting techniques.

Abstract

The class of type-two basic feasible functionals () is the analogue of (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing by higher-order term rewriting. Various kinds of interpretations for first-order term rewriting have been introduced in the literature for proving termination and characterizing first-order complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see second order rewriting as ways of computing type-2 functionals. We then prove that the class of functionals represented by higher-order terms admitting polynomially bounded cost-size interpretations exactly corresponds to .
Paper Structure (27 sections, 22 theorems, 54 equations, 3 figures)

This paper contains 27 sections, 22 theorems, 54 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Publication History
  5. Outline of the Paper
  6. Technical Overview.
  7. Preliminaries
  8. Higher-Order Rewriting
  9. Basic Feasible Functionals
  10. Cost--Size Interpretations
  11. The Interpretation of Types and Terms
  12. Size interpretation
  13. Cost interpretation
  14. Compatibility
  15. The Compatibility Theorem
  16. ...and 12 more sections

Key Result

Theorem 3.0

Suppose ${(\mathbb{F},\mathcal{R})}$ is an STRS compatible with a cost--size interpretation $\mathcal{F}$ (following def:compatible). Then for any valuations $\alpha$ and $\zeta$ we have $\mathsf{cost^{\star}}(s)_{\alpha,\zeta} > \mathsf{cost^{\star}}(t)_{\alpha,\zeta}$ and ${\llbracket{} s \rrbrack

Figures (3)

  • Figure 1: A term graph, its simplified version, and two graphs with sharing
  • Figure 2: Reducing a graph with the rule $\mathsf{add} \, \mathsf{0} \, y \to y$
  • Figure 3: Reducing a term graph with substantial sharing

Theorems & Definitions (57)

  • Example 1
  • Remark 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Example 7
  • Example 8
  • Theorem 3.0: Innermost Compatibility
  • Corollary 10
  • ...and 47 more