Polytime, combinatory logic and positive safe induction (Q1407533)

The author defines a system which characterizes the functions computable in polynomial time. It is based on combinatory logic and uses as main ingredient a ramification [\textit{D. Leivant}, Inf. Comput. 110, No. 2, 391--420 (1994; Zbl 0799.03042); ``Ramified recurrence and computational complexity. I: Word recurrence and poly-time'', in: Feasible mathematics II, 320--343 (1995; Zbl 0844.03024)] of the type of binary words (\(W_0\) and \(W_1\)). The induction principle for elements of \(W_1\) is restricted to {safe} formulae, i.e., positive formulae which do not contain \(W_1\). The lower bound is shown by an embedding of the well-known Bellantoni-Cook characterization of the polytime functions [\textit{S. Bellantoni} and \textit{S. Cook}, Comput. Complexity 2, No. 2, 97--110 (1992; Zbl 0766.68037)]. The upper bound is shown by use of a realizability procedure. In the final section the author addresses the possibility to replace ramification by modality. The work fits perfectly in the framework of Feferman's explicit mathematics. As further references the work of Strahm might be of interest [\textit{T. Strahm}, Inf. Comput. 185, No. 2, 263--297 (2003; Zbl 1057.03051)].