Complete and tractable machine-independent characterizations of second-order polytime - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

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

Jean-Yves Marion

Résumé

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 imperative procedures, which are not recursive. 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.
Fichier principal
Vignette du fichier
ctcbff.pdf (437.83 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03722245 , version 1 (13-07-2022)

Identifiants

Citer

Emmanuel Hainry, Bruce M Kapron, Jean-Yves Marion, Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. FoSSaCS 2022 - 25th International Conference on Foundations of Software Science and Computation Structures, Apr 2022, Munich, Germany. pp.368-388, ⟨10.1007/978-3-030-99253-8_19⟩. ⟨hal-03722245⟩
63 Consultations
47 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More