Search Results

Documents authored by Steinberg, Florian

Document
DOI: 10.4230/LIPIcs.CSL.2021.22
Computing Measure as a Primitive Operation in Real Number Computation

Authors: Christine Gaßner, Arno Pauly, and Florian Steinberg

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
We study the power of BSS-machines enhanced with abilities such as computing the measure of a BSS-decidable set or computing limits of BSS-computable converging sequences. Our variations coalesce into just two equivalence classes, each of which also can be described as a lower cone in the Weihrauch degrees. We then classify computational tasks such as computing the measure of Δ⁰₂-set of reals, integrating piece-wise continuous functions and recovering a continuous function from an L₁([0, 1])-description. All these share the Weihrauch degree lim.
Cite as

Christine Gaßner, Arno Pauly, and Florian Steinberg. Computing Measure as a Primitive Operation in Real Number Computation. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ganer_et_al:LIPIcs.CSL.2021.22,
  author =	{Ga{\ss}ner, Christine and Pauly, Arno and Steinberg, Florian},
  title =	{{Computing Measure as a Primitive Operation in Real Number Computation}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{22:1--22:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.22},
  URN =		{urn:nbn:de:0030-drops-134564},
  doi =		{10.4230/LIPIcs.CSL.2021.22},
  annote =	{Keywords: BSS-machine, Weihrauch reducibility, integrable function, Lebesgue measure, computable analysis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.50
Computable Analysis for Verified Exact Real Computation

Authors: Michal Konečný, Florian Steinberg, and Holger Thies

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We use ideas from computable analysis to formalize exact real number computation in the Coq proof assistant. Our formalization is built on top of the Incone library, a Coq library for computable analysis. We use the theoretical framework that computable analysis provides to systematically generate target specifications for real number algorithms. First we give very simple algorithms that fulfill these specifications based on rational approximations. To provide more efficient algorithms, we develop alternate representations that utilize an existing formalization of floating-point algorithms and interval arithmetic in combination with methods used by software packages for exact real arithmetic that focus on execution speed. We also define a general framework to define real number algorithms independently of their concrete encoding and to prove them correct. Algorithms verified in our framework can be extracted to Haskell programs for efficient computation. The performance of the extracted code is comparable to programs produced using non-verified software packages. This is without the need to optimize the extracted code by hand. As an example, we formalize an algorithm for the square root function based on the Heron method. The algorithm is parametric in the implementation of the real number datatype, not referring to any details of its implementation. Thus the same verified algorithm can be used with different real number representations. Since Boolean valued comparisons of real numbers are not decidable, our algorithms use basic operations that take values in the Kleeneans and Sierpinski space. We develop some of the theory of these spaces. To capture the semantics of non-sequential operations, such as the "parallel or", we use multivalued functions.
Cite as

Michal Konečný, Florian Steinberg, and Holger Thies. Computable Analysis for Verified Exact Real Computation. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{konecny_et_al:LIPIcs.FSTTCS.2020.50,
  author =	{Kone\v{c}n\'{y}, Michal and Steinberg, Florian and Thies, Holger},
  title =	{{Computable Analysis for Verified Exact Real Computation}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{50:1--50:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.50},
  URN =		{urn:nbn:de:0030-drops-132914},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.50},
  annote =	{Keywords: Computable Analysis, exact real computation, formal proofs, proof assistant, Coq}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.56
Continuous and Monotone Machines

Authors: Michal Konečný, Florian Steinberg, and Holger Thies

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional. Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq as part of Incone, a Coq library for computable analysis. The correctness proofs use a classical meta-theory with countable choice. Along the way we formally prove some known results such as the existence of a self-modulating modulus of continuity for partial continuous operators on Baire space. To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics.
Cite as

Michal Konečný, Florian Steinberg, and Holger Thies. Continuous and Monotone Machines. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 56:1-56:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{konecny_et_al:LIPIcs.MFCS.2020.56,
  author =	{Kone\v{c}n\'{y}, Michal and Steinberg, Florian and Thies, Holger},
  title =	{{Continuous and Monotone Machines}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{56:1--56:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.56},
  URN =		{urn:nbn:de:0030-drops-127230},
  doi =		{10.4230/LIPIcs.MFCS.2020.56},
  annote =	{Keywords: Computable Analysis, exact real computation, formal proofs, proof assistant, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.28
Quantitative Continuity and Computable Analysis in Coq

Authors: Florian Steinberg, Laurent Théry, and Holger Thies

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.
Cite as

Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{steinberg_et_al:LIPIcs.ITP.2019.28,
  author =	{Steinberg, Florian and Th\'{e}ry, Laurent and Thies, Holger},
  title =	{{Quantitative Continuity and Computable Analysis in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.28},
  URN =		{urn:nbn:de:0030-drops-110830},
  doi =		{10.4230/LIPIcs.ITP.2019.28},
  annote =	{Keywords: computable analysis, Coq, contionuous functionals, discontinuity, closed choice on the naturals}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.23
Polynomial Running Times for Polynomial-Time Oracle Machines

Authors: Akitoshi Kawamura and Florian Steinberg

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
This paper introduces a more restrictive notion of feasibility of functionals on Baire space than the established one from second-order complexity theory. Thereby making it possible to consider functions on the natural numbers as running times of oracle Turing machines and avoiding second-order polynomials, which are notoriously difficult to handle. Furthermore, all machines that witness this stronger kind of feasibility can be clocked and the different traditions of treating partial functionals from computable analysis and second-order complexity theory are equated in a precise sense. The new notion is named "strong polynomial-time computability", and proven to be a strictly stronger requirement than polynomial-time computability. It is proven that within the framework for complexity of operators from analysis introduced by Kawamura and Cook the classes of strongly polynomial-time computable functionals and polynomial-time computable functionals coincide.
Cite as

Akitoshi Kawamura and Florian Steinberg. Polynomial Running Times for Polynomial-Time Oracle Machines. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kawamura_et_al:LIPIcs.FSCD.2017.23,
  author =	{Kawamura, Akitoshi and Steinberg, Florian},
  title =	{{Polynomial Running Times for Polynomial-Time Oracle Machines}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.23},
  URN =		{urn:nbn:de:0030-drops-77370},
  doi =		{10.4230/LIPIcs.FSCD.2017.23},
  annote =	{Keywords: second-order complexity, oracle Turing machine, computable analysis, second-order polynomial, computational complexity of partial functionals}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact