Enhanced coinduction
Jurriaan Rot
promotors: prof.dr. J.J.M.M. Rutten (CWI and RU) and prof.dr. F.S. de Boer (CWI and UL)
copromotor: dr. M.M. Bonsangue (UL)
Universiteit Leiden
Date: 15 October, 2015, 15:00
Thesis: PDF
Summary
Coinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. The most important example of coinduction in computer science is bisimulation, a characterization of behavioural equivalence between objects with infinite or circular behaviour that comes with an associated proof principle. Coinductive techniques provide effective reasoning principles for areas as diverse as concurrency theory, automata theory, the study of infinite and circular data structures and more.
The broad applicability and rapidly increasing interest in coinductive techniques is based on the theory of coalgebras, which allows one to understand and prove properties of state-based models of computation at a high level of abstraction, and instantiate these results to a wide variety of concrete systems. The theory of coalgebras provides a structural and general view of bisimulation and coinduction, yielding canonical notions of behavioural equivalence and associated proof principles for concrete models of interest.
In this thesis we develop methods that simplify and enhance coinductive reasoning, with coalgebra as the framework of choice to obtain generally applicable techniques. Our results are divided into two parts: the first part concerns the coinductive proof method, and the second part concerns coinductive definition techniques.
We introduce a coalgebraic theory of enhanced proof techniques for bisimilarity. This theory generalizes so-called up-to techniques, introduced by Milner and Sangiorgi to simplify reasoning about behavioural equivalence of processes, from processes to a wide range of state-based systems, such as (non)deterministic automata, representations of infinite data structures and quantitative transition systems. As an extended example, we show how to apply these techniques concretely to reason about formal languages.
We further generalize our enhanced proof techniques by using on the abstract perspective on coinductive predicates introduced by Hermida and Jacobs. This allows us to obtain enhanced proof techniques not only for bisimilarity but for arbitrary coinductive predicates, which we apply to obtain proof methods for similarity of processes, language inclusion of weighted automata and divergence of processes.
Coinductive definition techniques are suitable for defining and studying the semantics of languages and calculi. Turi and Plotkin showed that one can obtain a compositional semantics by specifying the interaction between syntax (modelled by algebras) and behaviour (modelled by coalgebras) in terms of so-called distributive laws. We show how such distributive laws can be extended with recursive equations, to simplify language specification. Our main result in this part is that the interpretation of a specification that contains recursive equations of a certain form, is compositional, and that the enhanced proof techniques introduced in previous chapters apply.
Distributive laws can be useful to study coinductively defined languages, but they can be hard to describe. In the final chapter of this thesis we show how distributive laws can be presented as quotients of other distributive laws, which, in turn, can be presented using existing techniques. We apply our technique to derive distributive laws for the semantics of operations on infinite sequences, and the semantics of context-free languages.