Representing Contractive Functions on Streams
Streams, or infinite lists, have many applications in functional programming, and are naturally defined using recursive equations. But how do the user ensure that such equations make sense, i.e., that they actually produce well-defined streams? In this paper, the authors present a new approach to this problem, based upon the topological notion of contractive functions on streams. In particular, they give a sound and complete representation theorem for contractive functions on streams, illustrate the use of this theorem as a practical means to produce well-defined streams, and show how the efficiency of the resulting definitions can be improved using another representation of contractive functions.