Proving Productivity in Infinite Data Structures

For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate a 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. For cases where the approach does not apply directly, we develop transformations extending the power of the basic approach. We present a tool combining all these ingredients that can prove productivity of a wide range of examples fully automatically.

• Type: Conference
• Year: 2010
• Where: RTA
• Authors: Hans Zantema, Matthias Raffelsieper
• Keywords: Infinite Data Structures, Present Termination Tools, RTA 2010, Stream Productivity, Theoretical Computer Science