Elementary explicit types and polynomial time operations |
| |
Authors: | Daria Spescha Thomas Strahm |
| |
Affiliation: | 1. Institut für Informatik und angewandte Mathematik, Universit?t Bern, Neubrückstrasse 10, CH‐3012 Bern;2. http://www.iam.unibe.ch/~spescha |
| |
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] (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) |
| |
Keywords: | theory Feferman's explicit mathematics applicative theories types and names feasible operations |
|
|