Computability in Europe 2008
Logic and Theory of Algorithms

Special Session Talk:
Recursion in Higher Types and Resource Bounded Turing machines

Edit abstract data

Speaker:

Lars Kristiansen

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.