Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers

TL;DR

This paper develops a formal framework in Coq for certified computation on hyperspaces of subsets in topological and Polish spaces, enabling error-free operations and fractal generation.

Contribution

It formalizes higher-order data types and operations on subsets of topological spaces, introduces a nondeterministic continuity principle, and provides certified programs for fractal construction.

Findings

Formalization of open, closed, compact, and overt subsets in an abstract topological setting

Development of efficient encodings for subsets in Polish spaces based on metric properties

Extraction of certified programs for error-free subset operations and fractal generation

Abstract

Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a constructive dependent type theory, we present a framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations. We first define open, closed, compact and overt subsets for generic spaces in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis and constructive mathematics. From these proofs we can extract programs for testing inclusion, overlapping of sets, et cetera. To enhance the efficiency of the extracted programs, we then focus on Polish spaces, where we give more efficient encodings based on metric properties of the space. As various computational properties depend on the continuity of the encoding functions, we introduce a nondeterministic version of a continuity principle which is natural in our formalization and valid under the standard type-2 realizability interpretation. Using this principle we further derive the computational equivalence between the generic and the metric encodings. Our theory is fully implemented in the Coq proof assistant. From proofs in this Coq formalization, we can extract certified programs for error-free operations on subsets. As an application, we provide a function that constructs fractals in Euclidean space, such as the Sierpinski triangle, from iterated function systems using the limit operation. The resulting programs can be used to draw such fractals up to any desired resolution.