Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Michal Konečný, Sewon Park, Holger Thies

TL;DR

A framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations and introducing a nondeterministic version of a continuity principle which is natural in this Coq formalization and valid under the standard type-2 realizability interpretation.

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.

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

TL;DR

A framework for certified computation on hyperspaces of subsets by formalizing various higher-order data types and operations and introducing a nondeterministic version of a continuity principle which is natural in this Coq formalization and valid under the standard type-2 realizability interpretation.

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.

Paper Structure

This paper contains 24 sections, 35 theorems, 112 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Overview of the Project
  3. Related Work
  4. Preliminary Version
  5. Preliminaries
  6. Type Theory and Realizability
  7. Kleenean and Sierpinski Types
  8. Nondeterminism
  9. Real Numbers and Euclidean Space
  10. Continuity
  11. Continuity of Continuity
  12. Continuity on Euclidean Spaces
  13. Subsets
  14. Open and Closed Sets
  15. Compact and Overt Subsets
  16. ...and 9 more sections

Key Result

Lemma 3.2

For any types $X, Y$ given that equality for $Y$ is semi-decidable, meaning that the following continuity principle holds:

Figures (2)

  • Figure 1: Approximations of the triangle
  • Figure 2: Approximations of the Sierpinski triangle.

Theorems & Definitions (75)

  • Lemma 3.2: https://github.com/holgerthies/coq-aern/blob/d802e7e03295bfa782dde553ab02a7ab8d336c59/formalization/Hyperspace/Continuity.v#L239
  • proof
  • Lemma 3.3: https://github.com/holgerthies/coq-aern/blob/d802e7e03295bfa782dde553ab02a7ab8d336c59/formalization/Hyperspace/Continuity.v#L15
  • proof
  • Lemma 3.4: https://github.com/holgerthies/coq-aern/blob/d802e7e03295bfa782dde553ab02a7ab8d336c59/formalization/Hyperspace/Continuity.v#L279
  • proof
  • Lemma 3.5: https://github.com/holgerthies/coq-aern/blob/d802e7e03295bfa782dde553ab02a7ab8d336c59/formalization/Hyperspace/Continuity.v#L316
  • proof
  • Theorem 3.6: https://github.com/holgerthies/coq-aern/blob/d802e7e03295bfa782dde553ab02a7ab8d336c59/formalization/Hyperspace/Continuity.v#L417
  • proof
  • ...and 65 more