Elementary explicit types and polynomial time operations

Mathematical Logic Quarterly 55 (3):245-258 (2009)
  Copy   BIBTEX

Abstract

This paper studies systems of explicit mathematics as introduced by Feferman [9, 11]. In particular, we propose weak explicit type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the functions on binary words that are computable in polynomial time. The systems considered are natural extensions of the first-order applicative theories introduced in Strahm [19, 20]

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,038

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
The provably terminating operations of the subsystem of explicit mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.
Safe recursion with higher types and BCK-algebra.Martin Hofmann - 2000 - Annals of Pure and Applied Logic 104 (1-3):113-166.
Power types in explicit mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
The Analytic Polynomial-Time Hierarchy.Herbert Baier & Klaus W. Wagner - 1998 - Mathematical Logic Quarterly 44 (4):529-544.
Polynomial-time analogues of isolatedness.Leon Harkleroad - 1992 - Annals of Pure and Applied Logic 56 (1-3):173-182.
Feasible Graphs and Colorings.Douglas Cenzer & Jeffrey Remmel - 1995 - Mathematical Logic Quarterly 41 (3):327-352.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
On Nondeterminism, Enumeration Reducibility and Polynomial Bounds.Kate Copestake - 1997 - Mathematical Logic Quarterly 43 (3):287-310.
Machines Over the Reals and Non‐Uniformity.Felipe Cucker - 1997 - Mathematical Logic Quarterly 43 (2):143-157.

Analytics

Added to PP
2013-12-01

Downloads
22 (#710,249)

6 months
5 (#641,756)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The provably terminating operations of the subsystem of explicit mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
A feasible theory of truth over combinatory algebra.Sebastian Eberhard - 2014 - Annals of Pure and Applied Logic 165 (5):1009-1033.
Admissible closures of polynomial time computable arithmetic.Dieter Probst & Thomas Strahm - 2011 - Archive for Mathematical Logic 50 (5):643-660.

Add more citations

References found in this work

Polytime, combinatory logic and positive safe induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Feasible Operations and Applicative Theories Based on λη.Andrea Cantini - 2000 - Mathematical Logic Quarterly 46 (3):291-312.

Add more references