Edit abstract data
Abstract
Interesting things tend to happen when successor-like functions and
operations are removed from a standard model of computation, e.g. a
function algebra, a rewriting system or a programming language. Our
investigations of such successor-free models of computation have turned out
to be fruitful and have spawned some surprising theorems, particularly
when the models permit recursion in higher types. Godel's system T and
Plotkin's programming language PCF are prime examples of models of
computation permitting recursion in higher type. We will refer to their
successor-free variants as respectively T- (T minus) and PCF- (PCF minus).
We will study some hierarchies induced by fragments of T- and PCF-.
Many of the well-known deterministic complexity
classes, e.g. LOGSPACE, P, PSAPCE, LINSPACE and EXP, can be found in the
hierarchies. These classes are defined by imposing explicit resource bounds
on Turing machines, but note that the classes are not uniformly defined as
some are defined by imposing time bounds, whereas other are defined by
imposing space bounds. Small subrecursive classes can also be found in our
hierarchies, e.g. the small relational Grzegorczyk classes. In contrast to a
complexity class, a subrecursive class is defined as the least class
containing some initial functions and closed under certain composition and
recursion schemes. Some of the schemes might contain explicit bounds, but
no machine models are involved.
Our hierarchies are induced by neat and natural fragments of T- and PCF-,
and all the classes in the hierarchies are uniformly defined without
referring to explicit bounds. Thus, one would not expect the hierarchies
to capture such a wide variety of classes, that is, both time classes,
space classes and subrecursive classes. This indicates that a further
investigation of the hierarchies might be rewarding, and perhaps shed
light upon some of the notoriously hard open problems involving the classes
captured by the hierarchies, e.g. maybe some of these problems turn out to
be related in some unexpected way.