A Coinductive Approach to Computing with Compact Sets

TL;DR

This paper develops a coinductive framework for computing with nonempty compact sets of real numbers, using tree-based representations instead of digit streams, extending previous work on real number representations.

Contribution

It introduces a novel coinductive approach to represent and compute with compact sets using trees, overcoming limitations of digit stream representations.

Findings

Tree-based representations enable exact computation with compact sets.

The approach extends previous digit stream methods from real numbers to sets.

Foundations for certified algorithms on compact sets are established.

Abstract

Exact representations of real numbers such as the signed digit representation or more generally linear fractional representations or the infinite Gray code represent real numbers as infinite streams of digits. In earlier work by the first author it was shown how to extract certified algorithms working with the signed digit representations from constructive proofs. In this paper we lay the foundation for doing a similar thing with nonempty compact sets. It turns out that a representation by streams of finitely many digits is impossible and instead trees are needed.