Polytime, combinatory logic and positive safe induction (Q1407533): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s001530100105 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2032152194 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 23:47, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Polytime, combinatory logic and positive safe induction |
scientific article |
Statements
Polytime, combinatory logic and positive safe induction (English)
0 references
16 September 2003
0 references
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)].
0 references
polytime
0 references
restricted induction
0 references
combinatory logic
0 references