On the Complexity of Stream Equality

From FSL
Revision as of 13:47, 1 November 2013 by Grosu (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

This work has been published in complete form as a journal paper (JFP'13), and previous versions as a conference paper (ICFP'06) and as a technical report. The journal paper puts together my previous ICFP'06 paper and an ICFP'12 paper by the JFP coauthors. The technical report has a subtle error in the proof of membership of the stream equality problem in the class \Pi_2^0. Thanks to Andrei Popescu for noticing this error. The ICFP'06 paper fixes this error and adds a discussion on models of streams, and the journal paper adds many more details and consideres several types of stream models.

Journal of Function Programming

On the Complexity of Stream Equality
Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
Journal of Functional Programming, Volume 24(2-3), pp 166-217. 2014
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.
PDF, CIRC, DOI, Journal of Functional Programming, BIB

ICFP'06

Equality of Streams is a Pi_2^0-Complete Problem
Grigore Rosu
ICFP'06, ACM, 2006
Abstract. This paper gives a precise characterization for the complexity of the problem of proving equal two streams defined with a finite number of equations: \Pi_2^0. Since the \Pi_2^0 class includes properly both the recursively enumerable and the co-recursively enumerable classes, this result implies that neither the set of pairs of equal streams nor the set of pairs of unequal streams is recursively enumerable. Consequently, one can find no algorithm for determining equality of streams, as well as no algorithm for determining inequality of streams. In particular, there is no complete proof system for equality of streams and no complete system for inequality of streams.
PDF, ICFP'06 Slides, ACM, ICFP'06, BIB

Technical Report

Equality of Streams is a Pi_2^0-Complete Problem
Grigore Rosu
Technical report UIUCDCS-R-2006-2708, April 2006
Abstract. This paper gives a precise characterization for the complexity of the problem of proving equal two streams defined with a finite number of equations: \Pi_2^0. Since the \Pi_2^0 class includes properly both the recursively enumerable and the co-recursively enumerable classes, this result implies that one can find no mechanical procedure to say when two streams are equal, as well as no procedure to say when two streams are not equal. In particular, there is no complete proof system for equality of streams and no complete system for dis-equality of streams.
PDF, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation