A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
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 .
Cite
@article{arxiv.2401.12385,
title = {A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations},
author = {Patrick Baillot and Ugo Dal Lago and Cynthia Kop and Deivid Vale},
journal= {arXiv preprint arXiv:2401.12385},
year = {2025}
}