# Stream Differential Equations: Specification Formats and Solution Methods

@article{Hansen2017StreamDE, title={Stream Differential Equations: Specification Formats and Solution Methods}, author={Helle Hvid Hansen and Clemens Kupke and Jan J. M. M. Rutten}, journal={Log. Methods Comput. Sci.}, year={2017}, volume={13} }

Streams, or infinite sequences, are infinite objects of a very simple type, yet they have a rich theory partly due to their ubiquity in mathematics and computer science. Stream differential equations are a coinductive method for specifying streams and stream operations, and their theory has been developed in many papers over the past two decades. In this paper we present a survey of the many results in this area. Our focus is on the classification of different formats of stream differential… Expand

#### Tables and Topics from this paper

#### 24 Citations

Algebra and coalgebra of stream products

- Mathematics, Computer Science
- CONCUR
- 2021

This work introduces the class of (F,G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial of the streams themselves and their derivatives, and shows how to obtain closed forms of algebraic generating functions of combinatorial sequences, as well as solutions of nonlinear ordinary differential equations. Expand

Distributive laws for monotone specifications

- Medicine, Mathematics
- Acta Informatica
- 2019

It is shown that monotone specifications—that disallow negative premises—do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation of coGSOS. Expand

Distributive Laws for Monotone Specifications

- Computer Science, Mathematics
- EXPRESS/SOS
- 2017

It is shown that monotone specifications - that disallow negative premises - do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation of coGSOS. Expand

Bisimilarity of Open Terms in Stream GSOS

- Computer Science
- Sci. Comput. Program.
- 2019

This paper focuses on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables, to capture equivalence of open terms as bisimilarity on certain Mealy machines. Expand

In Praise of Sequence (Co-)Algebra and its implementation in Haskell

- Mathematics, Computer Science
- ArXiv
- 2018

This work sets the stage by bringing together a variety of sequence algebra concepts for the first time in one paper, intended to invite a broad mathematical audience to cast an eye over the subject. Expand

Coinduction Plain and Simple

- Computer Science
- ArXiv
- 2020

Extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle are suggested, which makes the coinductions proof principle more intuitive and stresses its closeness with structural induction. Expand

The differential calculus of causal functions

- Computer Science
- ArXiv
- 2019

This work examines a differential calculus of causal functions which includes many of the familiar properties of standard multivariable differential calculus and shows causal differentiation obeys a unique recurrence rule. Expand

Newton series, coinductively: a comparative study of composition

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2017

It is shown that the Newton transform is an isomorphism of rings that transforms the Hadamard product of two weighted languages into their infiltration product. Expand

Newton Series, Coinductively

- Mathematics, Computer Science
- ICTAC
- 2015

It is shown that the Newton transform is an isomorphism of rings that transforms the Hadamard product of two weighted languages into their infiltration product. Expand

Coinduction in Flow: The Later Modality in Fibrations

- Computer Science
- CALCO
- 2019

This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs, and uses the same construction to obtain a novel language for probabilistic productive coinduction programming. Expand

#### References

SHOWING 1-10 OF 78 REFERENCES

Stream Differential Equations: concrete formats for coinductive definitions

- Computer Science
- 2011

In this article we give an accessible introduction to stream differential equations, ie., equations that take the shape of differential equations from analysis and that are used to define infinite… Expand

Elements of Stream Calculus (An Extensive Exercise in Coinduction)

- Computer Science, Mathematics
- MFPS
- 2001

A number of applications of the calculus are presented, including difference equations, analytical differential equations, continued fractions, and some problems from discrete mathematics and combinatorics. Expand

Concrete stream calculus: An extended study

- Computer Science
- Journal of Functional Programming
- 2010

This paper redevelops the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. Expand

A coinductive calculus of streams

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2005

A coinductive calculus of streams based on the presence of a final coalgebra structure on the set of streams (infinite sequences of real numbers) is developed, which can be used to formulate both coinduction proofs and definitions. Expand

Proving Equality of Streams Automatically

- Computer Science
- RTA
- 2011

This paper presents a tool Streambox, a tool that can prove equality of a wide range of examples fully automatically, and investigates techniques for proving equality of streams suitable for automation. Expand

A tutorial on coinductive stream calculus and signal flow graphs

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 2005

This paper presents an application of coinductive stream calculus to signal flow graphs based on Z-transforms (a discrete version of Laplace transforms) and transfer functions. Expand

Well-definedness of Streams by Transformation and Termination

- Computer Science
- Log. Methods Comput. Sci.
- 2010

This work proposes a transformation from a stream specification to a term rewriting system (TRS) in such a way that termination of the resulting TRS implies that the stream specification is well-defined, that is, admits a unique solution. Expand

Representations of Stream Processors Using Nested Fixed Points

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2009

Representations of continuous functions on infinite streams of dis- crete values are defined, both in the case of discrete-valued functions, and in the cases of stream-valuedfunction representatives, which are non-wellfounded trees pieced together in a coinductive fashion from well-founded trees. Expand

A Sound and Complete Calculus for Finite Stream Circuits

- Mathematics, Computer Science
- 2010 25th Annual IEEE Symposium on Logic in Computer Science
- 2010

It is proved that a final locally finite (dimensional) coalgebra is, equivalently, an initial iterative algebra of the category of real vector spaces and makes the connection to existing work on the semantics of recursive specifications. Expand

On the Final Coalgebra of Automatic Sequences

- Mathematics, Physics
- Logic and Program Semantics
- 2012

This paper shows that the set of automatic sequences carries a final coalgebra structure, consisting of the operations of head, even, and odd, which will allow it to be shown that automatic sequences are to streams what rational languages are to (arbitrary) languages. Expand