On the Complexity of Stream Equality

Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
Journal of Functional Programming Volume 24, pp 166-217, May 2014
PDF BIB Journal of Functional Programming CIRC

Abstract. We study the complexity of deciding the equality of streams specified by systems of equations. There are several notions of stream models in the literature, each generating a different semantics of stream equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy. Their complexity ranges from low levels of the arithmetical hierarchy such as $\cpi{0}{2}$ for the most relaxed stream models, to levels of the analytical hierarchy such as $\cpi{1}{1}$ and up to subsuming the entire analytical hierarchy for more restricted but natural stream models. Since all these classes properly include both the semi-decidable and co-semi-decidable classes, it follows that regardless of the stream semantics employed, there is no complete proof system or algorithm for determining equality or inequality of streams. We also discuss several related problems, such as the existence and uniqueness of stream solutions for systems of equations, as well as the equality of such solutions.