Cobham recursive set functions (Q904151)

Computational complexity keeps being inspired by one of the original definitions of polynomial time computable functions [\textit{A. Cobham}, in: Logic, methodology and philosphy of science. Proceedings of the 1964 international congress. Amsterdam: North-Holland Publishing Company. 24--30 (1965; Zbl 0192.08702)]: instead of defining complexity class in terms of alternation, space or time on an abstract machine, it is possible to define a ``method'' to construct functions that will provably always be computable in polynomial time on an abstract machine. This constitutes an interesting shift from a mere observation to a mathematical proof, and opens the door to a more mathematical way of comparing complexity classes. The original definition, using limited recursion on notation, applies to functions taking as input binary strings. This paper asks (and answers positively) a simple question: is it possible to do the same for sets, i.e., to pinpoint a set of principles that will generate all the functions on set computable on polynomial time, and only those? This question was already asked, and (partially) answered, with the creation of safe recursive set functions (SRSF) [\textit{A. Beckmann} et al., J. Symb. Log. 80, No. 3, 730--762 (2015; Zbl 1357.03075)] and predicatively computable set functions (PCSF) [\textit{T. Arai}, Arch. Math. Logic 54, No. 3--4, 471--485 (2015; Zbl 1371.03094)]. The answer provided in this paper, called ``Cobham recursive set functions'' (CRSF) compares to those approaches as follows: {\parindent=0.7cm \begin{itemize}\item[--] SRSF actually failed to characterize polynomial time functions, but characterized multiple other complexity classes (depending on the restrictions on the sets considered). \item[--] PCSF characterizes polynomial functions on binary strings when restricted to hereditarily finite sets: its exact computational power on non-hereditarily finite sets remains unknown. \item[--] CRSF, when restricted to encoding of finite binary strings, exactly characterizes polynomial-time functions on binary strings (Section 4). \item[--] Additionally, CRSF is proven to be equivalent to PCSF\(^+\) (which varies on PCSF w.r.t. one closure criteria, and is supposed to strictly contain PCSF) over all sets, i.e., including non-hereditarily finite ones (Section 5). \end{itemize}} Their contribution is of importance for other reasons: {\parindent=0.7cm \begin{itemize}\item[--] It introduces and uses cleverly multiple tools of interest (smash function on sets, set composition function, embedding of a set into another) and has an interesting take on \(\in\)-recursion. \item[--] It introduces a nice and efficient way of comparing the ``structural complexity'' of two sets, called single-valued (or multi-valued) embedding \item[--] It is proven to be closed under many interesting schemata (Theorem 13), including ``impredicative'' ones (Section 3.6) \item[--] It can use various encodings of finite strings into sets (Section 4) \item[--] Maybe more importantly, it lays the foundation of further (and ongoing) explorations: alternative characterizations of CRSF in terms of algebra, circuits or extensions of functions [\textit{A. Beckmann} et al., ``Subset-bounded recursion and a circuit model for Cobham recursive set functions'', Preprint], and proof theory for this system [\textit{A. Beckmann} et al., ``Cobham recursive set functions and weak set theories'', Preprint] have been discussed. This illustrates the resilience and solidity of this system. \end{itemize}} Last but not least, their paper is self-contained (it even contains a recalling of the definition of PCSF), extremely well-written and organized. The use of Mostowski graphs of sets to illustrate some ideas (Section 2) and to ease some proofs is an agreeable feature.