@article{endrullis-hendriks-bakhshi-rosu-2013-jfp-submission,
author = {J\"{o}rg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Ro\c{s}u},
title = {On the Complexity of Stream Equality},
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.
},
journal = {Journal of Functional Programming},
year = {2013},
author_id = {Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu},
category = {fsl, semantics, logics, programming_languages, behavioral_equivalence, circular_coinduction, automated_reasoning},
project_url = {http://fsl.cs.uiuc.edu/circ},
project_name = {CIRC},
journal_acronym = {JFP},
journal_url = {http://journals.cambridge.org/action/displayJournal?jid=JFP}
}