2026-07-21T19:38:09Z https://drops.dagstuhl.de/oai

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

Proving Productivity in Infinite Data Structures Zantema, Hans Raffelsieper, Matthias Productivity infinite data structures streams For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate the notion of productivity. This generalizes stream productivity. We develop a general technique to prove productivity based on proving context-sensitive termination, by which the power of present termination tools can be exploited. In order to treat cases where the approach does not apply directly, we develop transformations extending the power of the basic approach. We present a tool combining these ingredients that can prove productivity of a wide range of examples fully automatically. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Hans Zantema and Matthias Raffelsieper 2010 Is Part Of LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2010.401 urn:nbn:de:0030-drops-26661 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.401 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode