{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:16:38Z","timestamp":1742944598439,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572302"},{"type":"electronic","value":"9783031572319"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The class of basic feasible functionals (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{BFF}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>BFF<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) is the analog of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{FP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FP<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{BFF}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>BFF<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> 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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{BFF}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>BFF<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> by higher-order term rewriting. Various kinds of interpretations for <jats:italic>first-order<\/jats:italic> 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\u2013size interpretations for higher-order term rewriting and see definitions as ways of computing functionals. We then prove that the class of functionals represented by higher-order terms admitting a certain kind of cost\u2013size interpretation is exactly <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{BFF}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>BFF<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_4","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"70-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Basic\u00a0Feasible\u00a0Functionals and the Interpretation\u00a0Method"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-9364-1140","authenticated-orcid":false,"given":"Patrick","family":"Baillot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6337-2544","authenticated-orcid":false,"given":"Cynthia","family":"Kop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1350-3478","authenticated-orcid":false,"given":"Deivid","family":"Vale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G.: Polynomial path orders. Log. Methods Comput. Sci. 9(4) (2013). https:\/\/doi.org\/10.2168\/LMCS-9(4:9)2013","DOI":"10.2168\/LMCS-9(4:9)2013"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: Tct: Tyrolean complexity tool. In: Chechik, M., Raskin, J. (eds.) Proceedings of TACAS 2016 conference. Lecture Notes in Computer Science, vol.\u00a09636, pp. 407\u2013423. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_24","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Baillot, P., Dal\u00a0Lago, U.: Higher-order interpretations and program complexity. In: Proceedings of CSL 2012. LIPIcs, vol.\u00a016, pp. 62\u201376. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2012.62, A journal version in Information and Computation (248), 2016","DOI":"10.4230\/LIPICS.CSL.2012.62"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Baillot, P., De\u00a0Benedetti, E., Ronchi Della\u00a0Rocca, S.: Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Inf. Comput. 261, 55\u201377 (2018). https:\/\/doi.org\/10.1016\/J.IC.2018.05.005","DOI":"10.1016\/J.IC.2018.05.005"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Baillot, P., Dal Lago, U., Kop, C., Vale, D.: On basic feasible functionals and the interpretation method (2024), https:\/\/arxiv.org\/abs\/2401.12385","DOI":"10.1007\/978-3-031-57231-9_4"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Beame, P., Cook, S.A., Edmonds, J., Impagliazzo, R., Pitassi, T.: The relative complexity of NP search problems. J. Comput. Syst. Sci. 57(1), 3\u201319 (1998). https:\/\/doi.org\/10.1006\/JCSS.1998.1575","DOI":"10.1006\/JCSS.1998.1575"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Beckmann, A., Weiermann, A.: A term rewriting characterization of the polytime functions and related complexity classes. Arch. Math. Log. 36(1), 11\u201330 (1996). https:\/\/doi.org\/10.1007\/s001530050054","DOI":"10.1007\/s001530050054"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bellantoni, S.J., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Comput. Complex. 2, 97\u2013110 (1992). https:\/\/doi.org\/10.1007\/BF01201998","DOI":"10.1007\/BF01201998"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Program. 11(1), 33\u201353 (2001). https:\/\/doi.org\/10.1017\/S0956796800003877","DOI":"10.1017\/S0956796800003877"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Bonfante, G., Marion, J., Moyen, J.: Quasi-interpretations a way to control resources. Theor. Comput. Sci. 412(25), 2776\u20132796 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.02.007","DOI":"10.1016\/j.tcs.2011.02.007"},{"key":"4_CR11","unstructured":"Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), pp. 24\u201330. North-Holland Publishing (1965)"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Constable, R.L.: Type two computational complexity. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA. pp. 108\u2013121. ACM (1973). https:\/\/doi.org\/10.1145\/800125.804041","DOI":"10.1145\/800125.804041"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Hofmann, M.: Realizability models and implicit complexity. Theor. Comput. Sci. 412(20), 2029\u20132047 (2011). https:\/\/doi.org\/10.1016\/J.TCS.2010.12.025","DOI":"10.1016\/J.TCS.2010.12.025"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Danner, N., Royer, J.S.: Adventures in time and space. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. pp. 168\u2013179. ACM (2006). https:\/\/doi.org\/10.1145\/1111037.1111053","DOI":"10.1145\/1111037.1111053"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279\u2013301 (1982). https:\/\/doi.org\/10.1016\/0304-3975(82)90026-3","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03452, pp. 301\u2013331. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_21","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Hainry, E., Kapron, B.M., Marion, J., P\u00e9choux, R.: A tier-based typed programming language characterizing feasible functionals. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8-11, 2020. pp. 535\u2013549. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394768","DOI":"10.1145\/3373718.3394768"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Hainry, E., Kapron, B.M., Marion, J., P\u00e9choux, R.: Complete and tractable machine-independent characterizations of second-order polytime. In: Bouyer, P., Schr\u00f6der, L. (eds.) Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13242, pp. 368\u2013388. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_19","DOI":"10.1007\/978-3-030-99253-8_19"},{"key":"4_CR19","unstructured":"Hainry, E., P\u00e9choux, R.: Theory of higher order interpretations and application to basic feasible functions. Log. Methods Comput. Sci. 16(4) (2020), https:\/\/lmcs.episciences.org\/6973"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Hartmanis, J., Stearns, R.E.: Automata-based computational complexity. Inf. Sci. 1(2), 173\u2013184 (1969). https:\/\/doi.org\/10.1016\/0020-0255(69)90014-0","DOI":"10.1016\/0020-0255(69)90014-0"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Irwin, R.J., Royer, J.S., Kapron, B.M.: On characterizations of the basic feasible functionals (part i). J. Funct. Program. 11(1), 117\u2013153 (2001). https:\/\/doi.org\/10.1017\/s0956796800003841","DOI":"10.1017\/s0956796800003841"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Kapron, B.M., Cook, S.A.: A new characterization of type-2 feasibility. SIAM J. Comput. 25(1), 117\u2013132 (1996). https:\/\/doi.org\/10.1137\/S0097539794263452","DOI":"10.1137\/S0097539794263452"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Kapron, B.M., Steinberg, F.: Type-two polynomial-time and restricted lookahead. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 579\u2013588. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209124","DOI":"10.1145\/3209108.3209124"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Kawamura, A., Cook, S.A.: Complexity theory for operators in analysis. ACM Trans. Comput. Theory 4(2), 5:1\u20135:24 (2012). https:\/\/doi.org\/10.1145\/2189778.2189780","DOI":"10.1145\/2189778.2189780"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci. 121(1 &2), 279\u2013308 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90091-7","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Kop, C., Vale, D.: Cost-size semantics for call-by-value higher-order rewriting. In: Proc. FSCD. LIPIcs, vol.\u00a0260, pp. 15:1\u201315:19 (2023). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2023.15","DOI":"10.4230\/LIPIcs.FSCD.2023.15"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Kop, C., Vale, D.: Tuple interpretations for higher-order complexity. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs, vol.\u00a0195, pp. 31:1\u201331:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.31","DOI":"10.4230\/LIPIcs.FSCD.2021.31"},{"key":"4_CR28","unstructured":"Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. IPSJ Transactions on Programming 42(SIG 7 (PRO 11)), 35\u201345 (2001), http:\/\/id.nii.ac.jp\/1001\/00016864\/"},{"key":"4_CR29","unstructured":"Lankford, D.S.: On proving term rewriting systems are noetherian. Memo MTP-3 (1979), https:\/\/www.ens-lyon.fr\/LIP\/REWRITING\/TERMINATION\/Lankford_Poly_Term.pdf"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Leivant, D.: A foundational delineation of computational feasiblity. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), Amsterdam, The Netherlands, July 15-18, 1991. pp. 2\u201311. IEEE Computer Society (1991). https:\/\/doi.org\/10.1109\/LICS.1991.151625","DOI":"10.1109\/LICS.1991.151625"},{"key":"4_CR31","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science. pp. 789\u2013792 (1970)"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Mehlhorn, K.: Polynomial and abstract subrecursive classes. J. Comput. Syst. Sci. 12(2), 147\u2013178 (1976). https:\/\/doi.org\/10.1016\/S0022-0000(76)80035-9","DOI":"10.1016\/S0022-0000(76)80035-9"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Oitavem, I.: Implicit characterizations of pspace. In: Kahle, R., Schroeder-Heister, P., St\u00e4rk, R.F. (eds.) Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings. Lecture Notes in Computer Science, vol.\u00a02183, pp. 170\u2013190. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45504-3_11","DOI":"10.1007\/3-540-45504-3_11"},{"key":"4_CR34","unstructured":"Terese: Term rewriting systems, Cambridge tracts in theoretical computer science, vol.\u00a055. Cambridge University Press (2003)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57231-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:02:52Z","timestamp":1714752172000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}