A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909896969027584 |
|---|---|
| author | Baillot, Patrick Lago, Ugo Dal Kop, Cynthia Vale, Deivid |
| author_facet | Baillot, Patrick Lago, Ugo Dal Kop, Cynthia Vale, Deivid |
| contents | 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$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_12385 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations Baillot, Patrick Lago, Ugo Dal Kop, Cynthia Vale, Deivid Logic in Computer Science Computational Complexity 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$. |
| title | A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations |
| topic | Logic in Computer Science Computational Complexity |
| url | https://arxiv.org/abs/2401.12385 |