2026-07-22T13:50:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3138 2024-03-06T10:33:52Z ddc:004 open_access

Proving Equality of Streams Automatically Zantema, Hans Endrullis, Joerg streams Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. In this paper we focus on equality of streams, more precisely, for a given set of equations two stream terms are said to be equal if they are equal in every model satisfying the given equations. We investigate techniques for proving equality of streams suitable for automation. Apart from techniques that were already available in the tool CIRC from Lucanu and Rosu, we also exploit well-definedness of streams, typically proved by proving productivity. Moreover, our approach does not restrict to behavioral input format and does not require termination. We present a tool Streambox that can prove equality of a wide range of examples fully automatically. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Hans Zantema and Joerg Endrullis 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.393 urn:nbn:de:0030-drops-31381 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.393 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode