zbMATH — the first resource for mathematics

The computational contents of ramified corecurrence. (English) Zbl 06488007
Pitts, Andrew (ed.), Foundations of software science and computation structures. 18th international conference, FOSSACS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-46677-3/pbk; 978-3-662-46678-0/ebook). Lecture Notes in Computer Science 9034, 422-435 (2015).
Summary: The vast power of iterated recurrence is tamed by data ramification: if a function over words is definable by ramified recurrence and composition, then it is feasible, i.e. computable in polynomial time, i.e. any computation using the first \(n\) input symbols can have at most \(p(n)\) distinct configurations, for some polynomial \(p\). Here, we prove a dual result for coinductive data: if a function over streams is definable by ramified corecurrence, then any computation to obtain the first \(n\) symbols of the output can have at most \(p(n)\) distinct configurations, for some polynomial \(p\). The latter computation is by multi-cursor finite state transducer on streams.
A consequence is that a function over finite streams is definable by ramified corecurrence if it is Turing-computable in logarithmic space. Such corecursive definitions over finite streams are of practical interest, because large finite data is normally used as a knowledge base to be consumed, rather than as recurrence template. Thus, we relate a syntactically restricted computation model, amenable to static analysis, to a major complexity class for streaming algorithms.
For the entire collection see [Zbl 1320.68027].
68Qxx Theory of computing
Full Text: DOI