| Infinite objects like streams of natural numbers or other data can be specified by a variety of methods. Our framework is that of recursive equations, common in functional languages, based on infinitary term rewriting. For many specifications such as alt = 0 : 1 : alt, defining the stream of alternating bits, well-definedness is evident. For more involved specifications such as fib = 0 : 1 : (fib + tail(fib)) well-definedness is not obvious, and decision methods are needed. This is the issue of productivity, consisting of determining whether a specification yields an infinite normal form composed of constructors. In a slogan: productivity is for infinite objects what termination is for finite data specifications. There are various methods to ensure productivity. For `pure' stream specifications such as above, a powerful automated method has been developed based on a fine-grained pebbleflow network analysis. Pebbles * are abstracted data: 0 = 1 = *. This data-oblivious approach can be extended by taking the identity of data into consideration (data-aware). In this proposal we extend the approach by admitting stream dependent data functions such as head of a stream. This involves dealing with `foresight' as in Y = 0 : head(tail(tail(Y))) : Y. Our primary concern is to treat stream dependent data functions, by explicitation of the input-output behaviour via a dependency analysis of the stream elements. Thus, we can deal also with partially defined stream terms. Second, we aim to generalize the methods to infinite data structures other than streams, such as infinite trees, lambda terms, and proof objects. |
