Weak theories of operations and typesInstitut für Informatik und angewandte Mathematik, Universität Bern, Neubrückstr. 10, CH-3012 Bern, Switzerland
URL Address: http://www.iam.unibe.ch/~strahm.
The theories of operations and types addressed in this talk are formulated in the spirit of Feferman's explicit mathematics. It has turned out that this framework provides a natural axiomatic basis for studying notions of abstract computability, especially from a proof-theoretic perspective. Our emphasis in this talk is on proof-theoretically weak systems and their relationship to complexity classes and weak arithmetics.
In the first part of our talk, we are concerned with so-called type-free applicative theories, which form the operational core of systems of explicit mathematics. In an applicative universe of discourse, all objects may be thought of as operations or rules, which can freely be applied to each other: self-application is meaningful, though not necessarily total. We survey results on various weak applicative theories whose provably total operations coincide with the functions computable in polynomial time, linear space, and polynomial space. Our systems can be seen as natural applicative analogues of systems of bounded arithmetic.
It is a distinguished advantage of our applicative theories that they allow for a very intrinsic and direct discussion of higher type issues, since higher types arise naturally in our combinatory setting. Moreover, due to the fact that the untyped language does not a priori restrict the class of functionals which can be expressed, it makes perfect sense to consider the class of higher type functionals which are provably total in a given applicative system. We will present some proof-theoretic aspects of higher type complexities in our setting; in particular, we will address the Melhorn-Cook-Urquhart basic feasible functionals.
The second part of the talk will be devoted to extensions of the first-order applicative framework by various means of typing disciplines. We study weak explicit typing and naming in the spirit of explicit mathematics. In particular, we discuss weak type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the polytime functions.
An interesting alternative of extending the applicative core by classes or types is by means of a partial (self-referential) truth predicate. We discuss results of Cantini who has studied substantial extensions of weak first-order applicative theories by partial truth, an axiom of choice and a positive uniformity principle.