Publication Types:

Applications of cut-free infinitary derivations to generalized recursion theory

Arnold Beckmann and Wolfram Pohlers
Annals of Pure and Applied Logic, Volume 94, Pages 7-19
Publication year: 1998

In this paper we introduce an infinitary proof system for a language of second order arithmetic which is complete for Pi^1_1 – sentences. The main observation there is the Boundedness Theorem telling that the order-type of a Sigma^1_1 – definable well-ordering < is less than or equal to the truth complexity of TI(<) . The commonly known Boundedness Principle of Generalized Recursion Theory will be obtained as a consequence of our proof theoretical Boundedness Theorem which in turn is a consequence of cut-freeness. This yields a proof of the Boundedness Principle which does not use the Analytical Hierarchy Theorem.

A term rewriting characterization of the polytime functions and related complexity classes

Arnold Beckmann and Andreas Weiermann
Archive for Mathematical Logic, Volume 36, Issue 1, Pages 11-30
Publication year: 1996

A natural term rewriting framework for the Bellantoni Cook schemata of predicative recursion, which yields a canonical definition of the polynomial time computable functions, is introduced. In terms of an exponential function both, an upper bound and a lower bound are proved for the resulting derivation lengths of the functions in question. It is proved that any natural reduction strategy yields an algorithm which runs in exponential time. We give an example in which this estimate is tight. It is proved that the resulting derivation lengths become polynomially bounded in the lengths of the inputs if the rewrite rules are only applied to terms in which the safe arguments – no restrictions are assumed for the normal arguments – consist of values, i.e. numerals, and not of names, i.e. non numeral terms. It is proved that in the latter situation any inside first reduction strategy and any head reduction strategy yield algorithms, for the function under consideration, for which the running time is bounded by an appropriate polynomial in the lengths of the input. A feasible rewrite system for predicative recursion with predicative parameter substitution is defined. It is proved that the derivation lengths of this rewrite system are polynomially bounded in the lengths of the inputs. As a corollary we reobtain Bellantoni´s result stating that predicative recursion is closed under predicative parameter recursion.