Equality of Streams is a Pi 2^0-Complete Problem

From FSL

Jump to: navigation, search

This work has been published both as a conference paper (ICFP'06) and as a technical report. 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.

[edit] 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


[edit] 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

Views