Behavioural differential equations - A coinductive framework for infinite behaviour

Coinduction has come to play an ever more important role in theoretical computer science, for the specification of and reasoning about infinite data structures and, more generally, automata with infinite behaviour.

In this talk, we shall focus on a recently introduced formalism for coinductive definitions: behavioural differential equations, with which one specifies behaviour in terms of initial outputs and behavioural derivatives (next state operators).

Our emphasis will be on the elementary calculus of streams (infinite sequences), of which we shall discuss the basic theory, developed in close analogy to mathematical analysis. As an application area, we will mention a calculus for periodic stream operators. Using this, we will give a new and transparent proof of Moessner's theorem using coinduction. This theorem (from 1951 - 1952) gives a suprising construction for the stream of powers of the natural numbers (such as 1,8,27,64, ... for k=3) out of the stream of natural numbers.