Patrick Baillot ; Ugo Dal Lago ; Cynthia Kop ; Deivid Vale - A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

lmcs:14655 - Logical Methods in Computer Science, November 5, 2025, Volume 21, Issue 4 - https://doi.org/10.46298/lmcs-21(4:19)2025
A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple InterpretationsArticle

Authors: Patrick Baillot ; Ugo Dal Lago ; Cynthia Kop ; Deivid Vale

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$.


Volume: Volume 21, Issue 4
Secondary volumes: Selected Papers of the 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024)
Published on: November 5, 2025
Accepted on: August 6, 2025
Submitted on: November 1, 2024
Keywords: Logic in Computer Science, Computational Complexity
Funding:
    Source : OpenAIRE Graph
  • Differential Program Semantics; Funder: European Commission; Code: 818616
  • Implicit Complexity through Higher Order Rewriting; Funder: European Commission; Code: 612.001.803

Consultation statistics

This page has been seen 702 times.
This article's PDF has been downloaded 356 times.