Regular Expressions Revisited: A Coinductive Approach to Streams, Automata, and Power Series

Abstract

Regular expressions are a standard means for denoting formal languages that are recognizable by finite automata. Much less familiar is the use of syntactic expressions for (formal) power series. Power series generalize languages by assigning to words multiplicities in any semiring (such as the reals) rather than just Booleans, and include as a special case the set of streams (infinite sequences). Here we shall define an extended set of regular expressions with multiplicities in an arbitrary semiring. The semantics of such expressions will be defined coinductively, allowing for the use of a syntactic coinductive proof principle. To each expression will be assigned a nondeterministic automaton with multiplicities, which usually is a rather efficient representation of the power series denoted by the expression. Much of the above will be illustrated for the special case of streams of real numbers; other examples include automata and languages (sets of words), and task-resource systems (using the max-plus semiring). The coinductive definitions mentioned above take the shape of what we have called behavioural differential equations, on the basis of which we develop, as a motivating example, a theory of streams in a calculus-like fashion.