A coinductive approach to exact real number computation

A coinductive approach to exact real number computation

Abstract

Coinduction is a concept of increasing importance in mathematics and computer science, in particular in non-wellfounded set theory, process algebra and database theory. Probably the best-known example of a coinductive relation is bisimilarity of processes. In this talk I present an application of coinduction to exact real number computation. Intuitively, coinduction is about deconstructing, or observing data, or describing how a process evolves. This is in contrast to induction, which is about constructing data. A real number, say pi, is a typical candidate for coinduction. We cannot construct pi (exactly), but we can make observations about it, by, for example, successively computing digits of pi. Similarly, a computable continuous functions on the real numbers can be viewed as a coinductive process: we successively compute digits of the output while reading digits of the input.

In fact, it turns out that the computation of a single correct output digit is an inductive process. Therefore, continuous real functions are described by a combination of induction and coinduction.