2 Search Results for "Collins, Pieter"


Document
Formalizing Hyperspaces for Extracting Efficient Exact Real Computation

Authors: Michal Konečný, Sewon Park, and Holger Thies

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
We propose a framework for certified computation on hyperspaces by formalizing various higher-order data types and operations in a constructive dependent type theory. Our approach builds on our previous work on axiomatization of exact real computation where we formalize nondeterministic first-order partial computations over real and complex numbers. Based on the axiomatization, we first define open, closed, compact and overt subsets in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis. From these proofs we extract programs for testing inclusion, overlapping of sets, et cetera. To improve extracted programs, our framework specializes the Euclidean space ℝ^m making use of metric properties. To define interesting operations over hyperspaces of Euclidean space, we introduce a nondeterministic version of a continuity principle valid under the standard type-2 realizability interpretation. Instead of choosing one of the usual formulations, we define it in a way similar to an interval extension operator, which often is already available in exact real computation software. We prove that the operations on subsets preserve the encoding, and thereby define a small calculus to built new subsets from given ones, including limits of converging sequences with regards to the Hausdorff metric. From the proofs, we extract programs that generate drawings of subsets of ℝ^m with any given precision efficiently. As an application we provide a function that constructs fractals, such as the Sierpinski triangle, from iterated function systems using the limit operation, resulting in certified programs that errorlessly draw such fractals up to any desired resolution.

Cite as

Michal Konečný, Sewon Park, and Holger Thies. Formalizing Hyperspaces for Extracting Efficient Exact Real Computation. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 59:1-59:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{konecny_et_al:LIPIcs.MFCS.2023.59,
  author =	{Kone\v{c}n\'{y}, Michal and Park, Sewon and Thies, Holger},
  title =	{{Formalizing Hyperspaces for Extracting Efficient Exact Real Computation}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{59:1--59:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.59},
  URN =		{urn:nbn:de:0030-drops-185935},
  doi =		{10.4230/LIPIcs.MFCS.2023.59},
  annote =	{Keywords: Computable analysis, type theory, program extraction}
}
Document
Computability of Homology for Compact Absolute Neighbourhood Retracts

Authors: Pieter Collins

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
In this note we discuss the information needed to compute the homology groups of a topological space. We argue that the natural class of spaces to consider are the compact absolute neighbourhood retracts, since for these spaces the homology groups are finite. We show that we need to specify both a function which defines a retraction from a neighbourhood of the space in the Hilbert cube to the space itself, and a sufficiently fine over-approximation of the set. However, neither the retraction itself, nor a description of an approximation of the set in the Hausdorff metric, is sufficient to compute the homology groups. We express the conditions in the language of computable analysis, which is a powerful framework for studying computability in topology and geometry, and use cubical homology to perform the computations.

Cite as

Pieter Collins. Computability of Homology for Compact Absolute Neighbourhood Retracts. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 107-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{collins:OASIcs.CCA.2009.2263,
  author =	{Collins, Pieter},
  title =	{{Computability of Homology for Compact Absolute Neighbourhood Retracts}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{107--118},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2263},
  URN =		{urn:nbn:de:0030-drops-22635},
  doi =		{10.4230/OASIcs.CCA.2009.2263},
  annote =	{Keywords: Computability, homology, compact absolute neighbourhood retract}
}
  • Refine by Author
  • 1 Collins, Pieter
  • 1 Konečný, Michal
  • 1 Park, Sewon
  • 1 Thies, Holger

  • Refine by Classification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Computability
  • 1 Computable analysis
  • 1 compact absolute neighbourhood retract
  • 1 homology
  • 1 program extraction
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2009
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail