In this paper we use methods of proof theory to assign ordinals to
classes of (terminating) programs, the idea being that the ordinal
assignment provides a uniform way of measuring computational
complexity ``in the large''. We are not concerned with placing prior
(e.g. polynomial) bounds on computation-length, but rather with
general methods of assessing the complexity of natural classes of
programs according to the ways in which they are constructed. We begin
with an overview of the method in section 2, the crucial idea being
supplied by Buchholz's 
-rule. Section 3 introduces a large
class of higher-order programs based on Plotkin's PCF, but with
``bounded'' fixed point operators controlled by given well-orderings.
A Tait-style computability proof then ensures termination. In
section 4 the details of the ordinal assignment method are worked out
for the case where the given well-ordering is just the ordering of
the natural numbers. The complexity bounds thus obtained turn out to
be the slow-growing functions 
with 
below the
Bachmann-Howard ordinal. Thus the functions computed by
PCF
-programs are just the provably recursive functions of
arithmetic.
A semantical method to prove termination of higher order
rewrite systems (HRS) is presented. Its main tool is the notion of a
strict functional, which is a variant of Gandy's notion of a
hereditarily monotonic functional. The main advantage of the method is
that it makes it possible to transfer ones intuitions about why an HRS
should be terminating into a proof: one has to find a ``strict''
interpretation of the constants involved in such a way that the left
hand side of any rewrite rule gets a bigger value than the right hand
side. The applicability of the method is demonstrated in three
examples. (a) An HRS involving map and append. (b) The usual rules for
the higher order primitive recursion operators in Gödel's T. (c)
Derivation terms for natural deduction systems. We prove termination
of the rules for 
-conversion and permutative conversion for
logical rules including introduction and elimination rules for the
existential quantifier. This has already been proved by Prawitz in
1971; however, our proof seems to be more perspicious.
Technically we build on J van de Pol, Termination Proofs for
Higher-Order Rewrite Systems, HOA '93, SLNCS 816, pp. 305 -- 325,
1994. There a notion of a strict functional and simultaneously of a
strict greater-than relation 
between monotonic functionals
is introduced. The main result then is the following. Let M be a
term in 
normal form and 
. Then for any
strict environment U and all monotonic 
and 
, one
has 
. From this van de Pol
derives the technique described above for proving termination of
higher order term rewrite systems, generalizing a similar approach for
first order rewrite systems due to Huet.
Here a slight change in the definition of strictness is exploited (against the original conference paper by van de Pol 1994; cf. the footnote on p. 316). This makes it possible to deal with rewrite rules involving types of level >2 too, and in particular with proof theoretic applications. In order to do this some theory of strict functionals is developed. We also add product types, which are necessary to treat e.g. the existential quantifier.
Different methods for extracting programs from a classical proofs are investigated. A direct method based on normalization and the well known negative translation combined with a realizability interpretation are compared and shown to yield equal results. Furthermore, the translation method is refined in order to obtain optimized programs. An analysis of the proof translation shows that in many cases only small parts of a classical proof need to be translated. Proofs extracted from such refined translations have simpler type and control structure. The effect of the refinements is demonstrated at two examples.