Premium
Elementary explicit types and polynomial time operations
Author(s) -
Spescha Daria,
Strahm Thomas
Publication year - 2009
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200810004
Subject(s) - mathematics , polynomial , natural number , comprehension , algebra over a field , type (biology) , order (exchange) , binary number , discrete mathematics , pure mathematics , arithmetic , computer science , programming language , mathematical analysis , ecology , finance , economics , biology
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] (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)