Mixed Inductive-Coinductive Reasoning Types, Programs and Logic

Induction and coinduction are threads that cross the landscape of Mathematics and Computer Science as methods to define objects and reason about them. Of these two, induction is by far the better known technique, although coinduction has always been around in disguise. It was only in recent years that we began to see through this disguise and developed coinduction as a technique in its own right. This led to some remarkable theory under the umbrella of coalgebra and to striking applications of coinduction.

As it turns out, induction and coinduction are complementary techniques, they are dual in a precise sense. Being complementary, it is often necessary to use both techniques or even intertwine them. In this thesis, we show that combined induction-coinduction is often used implicitly, just like induction and coinduction used to be before they were studied systematically. Thus, the purpose of this thesis is to carefully study the combination of induction and coinduction, which hopefully, if anything, inspires others to work on and use inductive-coinductive techniques.

One example, which pervades the thesis, illustrates the combination particularly well: the so-called substream relation. A stream s, that is an infinite sequence, is a substream of stream t if all the entries of s occur in order in t. Intuitively, one has to find for all entries in s an entry in t with the same value in finitely many steps. The fact that we may only use a finite number of steps to find each entry is an iterative process, while its repetition for all entries is a coiterative process. Since these two processes are interleaved, the substream relation is a mixed inductive-coinductive relation.

To be able to deal with such examples, we aim in this thesis to find and study languages for inductive-coinductive definitions and reasoning, which lend themselves to being automatically verifiable, can be equipped with formal semantics, and allow human-readable specifications and proofs. Put in general terms, the intention of studying languages for inductive-coinductive definitions and reasoning is to provide a framework that is sufficiently rich to accommodate category theory and set theory. Moreover, this framework should allow for semantics that are, in principle, independent of those theories, and for proofs that can be formalised and automatically verified. This is of course an ambitious goal that will not be fully attained in this thesis, but we will nonetheless contribute to it.

Towards these aims, we proceed in several steps. The first step is to have some objects to reason about, which means specifically for this thesis that we provide two programming languages for inductive-coinductive types. In the first language, one can only write terminating programs, while the second allows arbitrary recursive specification. Such recursive specifications ease programming with mixed inductive-coinductive types dramatically over programming with the iteration and coiteration schemes in the first language. However, this increased expressiveness also comes at the price that we give up simple syntactic conditions for well-defined programs (programs that terminate under any observation) and have to characterise such programs in a different way.

To this end, we establish notions of observationally normalising programs, the well-defined programs, and an observational program equivalence in the presence of inductive-coinductive types and arbitrary recursive specifications. As it turns out, the characterisation of observationally normalising programs is itself an inductive-coinductive predicate. In contrast, the program equivalence is introduced through a modal logic and turns out to be purely coinductive. Given such a program equivalence, we have to ask whether it is well-motivated. An important property of the equivalence is that is allows us to construct 2-categories of types and terms, in which equality captures computations, while 2-cells represent program equivalences. In particular, least fixed point types and greatest fixed point types carry, respectively, pseudo-initial algebras and pseudo-final coalgebras in these 2-categories.

Even though the 2-category theoretical results give us some principles to reason about programs, these principles are not always the most convenient ones to work with. For this reason, we develop in the next step more convenient reasoning techniques: a bisimulation proof method, a syntactic first-order logic that is itself recursive, and an algorithm that operates on fragments of the programming languages. The bisimulation proof method can be enhanced by using so-called up-to techniques, which we demonstrate by showing that the substream relation is transitive. In particular, we use an up-to technique that allows us to use induction inside a bisimulation proof.

This setup becomes, unfortunately, rather complex because implementing induction as up-to technique forces a stratification of a mixed inductive-coinductive proof into a coinduction and two inductions. What is worse, the induction proofs must be proven independently of the coinduction, which makes finding the correct induction hypothesis a highly non-trivial task. To overcome such problems, we construe a recursive logic, in which inductive and coinductive proofs are incrementally constructed together. Recursion in proofs of this logic is thereby controlled through the so-called later modality. This modality allows us to ensure the correctness of a proof through each proof rule separately, which makes both proof checking and the soundness proof easy to implement.

Up to this point, the thesis is about programming with simple types, and reasoning about a very specific inductive-coinductive predicate (observational normalisation) and a very specific coinductive relation (observational equivalence). Both are defined in naive set theory, which means that neither are given in a principled manner nor that proofs about them can be directly formally expressed. This clearly violates our aims and is what caused us to invent, for example, a new logic from scratch. The remainder of the thesis deals with this issue in that we develop a category theoretic and a type theoretic approach that allow us to formally express results about simple inductive-coinductive types, and inductive-coinductive predicates and relations. It turns out that inductive-coinductive predicates and relations are best expressed as certain dialgebras in fibrations. This approach subsumes simple types and general dependent types. What is more, we are able to define a class of strictly positive dependent types and reduce them to initial algebras and final coalgebras of polynomial functors. This reduction to minimal requirement allows us to interpret dependent types in well-studied models. The category theoretical approach to dependent types is concluded by an analysis of the logical principles that are available in a fibration that is closed under strictly positive dependent types.

Following the guiding principles of the category theoretical development, we construct also a (syntactic) dependent type theory. This results in a small type theory that is merely based on inductive-coinductive dependent types, yet it admits all basic logical operators like conjunction, implication, quantification etc. Since this type theory is built on iteration and coiteration principles, we are able to show that all terms in that theory are strongly normalising. The thesis is concluded by giving a general induction principle for this type theory and an elaborate example of inductive-coinductive reasoning in Agda.