10.4230/LIPICS.RTA.2010.401
Zantema, Hans
Hans
Zantema
Raffelsieper, Matthias
Matthias
Raffelsieper
Proving Productivity in Infinite Data Structures
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Productivity
infinite data structures
streams
Lynch, Christopher
Christopher
Lynch
2010
2010-07-06
2010-07-06
2010-07-06
en
urn:nbn:de:0030-drops-26661
10.4230/LIPIcs.RTA.2010
978-3-939897-18-7
1868-8969
10.4230/LIPIcs.RTA.2010
LIPIcs, Volume 6, RTA 2010
Proceedings of the 21st International Conference on Rewriting Techniques and Applications
2013
6
29
401
416
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lynch, Christopher
Christopher
Lynch
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
6
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
16 pages
224713 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, pages 401-416