A coinductive approach to computing with compact sets

DOI10.4115/JLA.2016.8.3MaRDI QIDQ2974666zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Dieter Spreen

Publication date 10 April 2017

Published in Journal of Logic and Analysis (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1510.08498

zbMATH Keywords

compact setscomputing with continuous objectsexact real number computationprogram extraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Computation over the reals, computable analysis (03D78)

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.

Recommendations

• Logical Approaches to Computational Barriers
• An efficient Coq tactic for deciding Kleene algebras
• Soundness and completeness proofs by coinductive methods
• scientific article; zbMATH DE number 1314221
• Coinductive formulas and a many-sorted interpolation theorem
• Techniques of computable set theory with applications to proof verification
• A coinductive approach to proof search
• On Bounded Reachability of Programs with Set Comprehensions
• Exhaustible sets in higher-type computation
• Complete Coinductive Theorems. II

Cited in

(11)

• A bitopological view on cocompact extensions
• Real number computation through Gray code embedding.
• Intuitionistic fixed point logic
• From Sets to Bits in Coq
• Coinductive counting: bisimulation in enumerative combinatorics (extended abstract)
• Representations of stream processors using nested fixed points
• Coinductive formulas and a many-sorted interpolation theorem
• Limits of real numbers in the binary signed digit representation
• Computing with continuous objects: a uniform co-inductive approach
• Logic for Gray-code computation
• scientific article; zbMATH DE number 7731929 (Why is no real title available?)

This page was built for publication: A coinductive approach to computing with compact sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974666)