Stream Differential Equations: concrete formats for coinductive definitions

Abstract

In this article we give an accessible introduction to stream differential equations, i.e., equations that take the shape of differential equations from analysis and that are used to define infinite streams. Furthermore we discuss a syntactic format for stream differential equations that ensures that any system of equations that fits into the format has a unique solution. It turns out that the stream functions that can be defined using our format are precisely the causal stream functions. Finally, we are going to discuss non-standard stream calculus that uses basic (co-)operations different from the usual head and tail operations in order to define and to reason about streams and stream functions.