Ramified Corecurrence and Logspace

Ramified recurrence over free algebras has been used over the last two decades to provide machine-independent characterizations of major complexity classes. We consider here ramification for the dual setting, referring to coinductive data and corecurrence rather than inductive data and recurrence.Whereas ramified recurrence is related basically to feasible time (PTime) complexity, we show here that ramified corecurrence is related fundamentally to feasible space. Indeed, the 2-tier ramified corecursive functions are precisely the functions over streams computable in logarithmic space. Here we define the complexity of computing over streams in terms of the output rather than the input, i.e. the complexity of computing the n-th entry of the output as a function of n. The class of stream functions computable in logspace seems to be of independent interest, both theoretical and practical.We show that a stream function is definable by ramified corecurrence in two tiers iff it is computable by a transducer on streams that operates in space logarithmic in the position of the output symbol being computed. A consequence is that the two-tier ramified corecursive functions over finite streams are precisely the logspace functions, in the usual sense